Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

1 Introduction

• The work targets data sparsity: MiniF2F is limited by the labor required for formalization, while Mathlib emphasizes fundamental rather than contest-level problems.The introduction identifies creating enough high-quality formalized statements as an initial step toward better automatic theorem proving.Source: §1 · p. 1
• 57K math problems were autoformalized, with 93.5% accuracy in a random manual sample, and the filtering process produced 21 new IMO statements absent from Compfiles.The authors describe the pipeline as translating between natural-language questions and Lean 4 statements, with compiler and NLI checks and human revision of invalid samples.Source: §1 · p. 2
• The authors present an active-learning pipeline for autoformalizing natural-language questions and open-source a translation model and pipeline for diverse mathematical topics.They also describe an open dataset of 57K formalized problems, 5K with formal solutions, for autoformalization and automated theorem proving.Source: §1 · pp. 1–2
• The contribution also includes 21 newly formalized IMO questions that have not appeared in Compfiles.The questions are produced through the same filtering process described for the larger dataset.Source: §1 · p. 2

2 Preliminaries

• Lean 4 supports formal verification, and a completed proof returns a “No goals” signal; users can also leave a proof incomplete with “sorry.”The paper says its focus is statement translation, so it uses “sorry” for proofs.Source: §2 · p. 2
• Mathlib is a user-maintained Lean 4 library whose existing theorems and functions can be used when stating and proving results.The paper defaults to Mathlib in the following discussion, as in MiniF2F environments.Source: §2 · p. 2
• A typical Lean statement lists variables and their types, gives conditions in brackets, and places the conclusion after a colon before `:= by sorry`.The example uses a theorem declaration with assumptions and a set-valued conclusion.Source: §2 · p. 3

3.1 Autoformalization

• For high-school contest problems, Lean Workbook differs from DeepSeek-prover [31] by using active learning to reduce incorrect formalizations and manually evaluating dataset accuracy.Prior autoformalization spans grade-school, high-school contest, and undergraduate mathematics, using in-context learning or fine-tuned LLMs.Source: §3.1 · p. 3

3.2 Automatic Theorem Proving

• Theorem-proving approaches either search proof states with best-first or tree search [7] [23] [29], or generate whole proofs from models or human proofs [31] [12, 27].Search can reject invalid tactics through the compiler, but the paper says it does not let the model predict tactics from an overall perspective.Source: §3.2 · p. 3

3.3 Data curation

• Formal-language datasets draw on runtime information, human annotations, and human interaction, while benchmarks provide high-accuracy formal verification; this work combines expert and LLM contributions to autoformalization data.The cited examples include LeanDojo and CoqGym for extracting runtime information [32? ].Source: §3.3 · p. 3

4.1 First-round pipeline

• For round one, MiniF2F and ProofNet supplied paired data; solution questions were rewritten as proof goals, and both translation directions entered training.Source: §4.1 · pp. 3–4
• The well-defined subset had 6,652 tags; more than three-fourths of samples had algebra-related tags, geometry tags were rare, and number-theory tags were often assigned to inequalities.Source: §4.1 · p. 5

4.2 Data Diagnostic and Iteration pipeline

• Lean compilation checks statement validity, then back-translation and NLI compare the original question with its formalization’s natural-language rendering.Samples without positive NLI feedback are marked for human revision.Source: §4.2 · p. 5
• Experts diagnosed samples that failed compilation or NLI, added manual corrections to training, and later switched to random tag-based sampling as patterns became harder to identify.Early iterations added about 30 human-labeled samples each.Source: §4.2 · p. 5
• After six rounds, sampled-data correct rate almost reached 95%, and iterations added 341 problems to training.Source: §4.2 · p. 6

5.1 Evaluation setting

• Evaluation uses compile pass number, NLI pass number, and sampled human-judged correct translation rate to assess generated statements.NLI pass requires compilation and a back-translation judged equivalent to the original question; human review is sampled by question type.Source: §5.1 · p. 6

5.2 Dataset Statistics and Evaluation Results

• After six iterations, 205,079 questions pass compilation and 57,231 pass NLI; sampled accuracy exceeds 90% for the three most common tags.For other tags, almost all have at most one wrong translation; Table 1 samples 10 problems for each of the three most common tags and five for others.Source: §5.2 · p. 6, Table 1 · p. 7
• InternLM-Math-Plus solves 4,898 Lean Workbook problems from 1,024 proof samples per problem, a Pass@1024 of 8.6%.The paper describes these problems as significantly harder than MiniF2F and says the solutions will be open-sourced to support theorem proving.Source: §5.2 · p. 6
• Manual diagnostics find that iterative examples help correct compilation patterns, but are less effective for contest-problem interpretation errors.Reported examples include integer division type ambiguity and omitted minimality or existence; some errors can be partly fixed by post-processing.Source: §5.2 · p. 6

5.3 Effectiveness and discussion

• The pipeline and dataset add over 20,000 correct samples for both compile and NLI tests, while MiniF2F accuracy increases with the extended dataset.The comparison covers models across iterations and MiniF2F fine-tuning with and without Lean Workbook.Source: §5.3 · p. 8, Table 3 · p. 8, Table 4 · p. 8

5.4 Formalizing IMO problems

• The model yields 21 manually evaluated IMO formalizations: 14 algebra, five number theory, and two combinatorics problems.The team translated each problem 100 times, filtered with compile and NLI tests, and manually checked and slightly modified some conclusions.Source: §5.4 · p. 8

6 Conclusion

• The authors conclude that active learning is effective in this data-sparse setting and release Lean Workbook to support work on autoformalization and automatic theorem proving.Source: §6 · p. 9

Limitations

• Similar problems are difficult to deduplicate, and contest-focused active learning may not suit formalizing other levels of mathematics.Source: Limitations · p. 9

Checklist

• The checklist says the main claims and scope are described and that work limitations are discussed in Section 6.Source: Checklist · p. 12
• The authors report no apparent negative societal impacts, stating that proving mathematical theorems has none.Source: Checklist · p. 12
• The checklist reports that code, data, and training details are provided; error bars are marked not applicable because each iteration was fine-tuned once.Source: Checklist · p. 12

• The examples pair natural-language problems with Lean statements across common mathematical tags.Source: A Case study · p. 13
• A four-variable inequality assumes positive variables with product 1 and gives an upper bound of 4/5.Source: A Case study · p. 13
• Number-theory examples formalize a prime-divisibility claim and classify integer cubes modulo 9.Source: A Case study · pp. 13–14
• A trigonometric system is stated in Lean with an equivalent characterization of its solutions using integer multiples of π.Source: A Case study · p. 13
• A triangle-side inequality is formalized under positivity and triangle-inequality hypotheses.Source: A Case study · p. 13
• A complex-set example states that containing two specified lines and being closed under addition implies M = C.Source: A Case study · p. 14
• The case study also includes a normalized sum estimate approaching 1 and the theorem that a continuous image of a compact set is compact.Source: A Case study · pp. 14–15
• Other examples formalize a real-valued functional equation and a sequence recurrence whose reciprocal terms have partial sums below 2.Source: A Case study · p. 14

• The formalized IMO questions focus on algebra, number theory, and combinatorics.Source: B IMO example · p. 15
• The IMO 1975 sequence example formalizes infinitely many representations of later sequence terms as positive-integer combinations involving an earlier term.Source: B IMO example · p. 15
• The IMO 1977 trigonometric example states bounds on two pairs of coefficients when a specified trigonometric expression is nonnegative for all real inputs.Source: B IMO example · p. 15
• The IMO 1978 number-theory example encodes finding the least-sum positive exponents whose powers of 1978 have matching last three digits.Source: B IMO example · p. 15
• The IMO 1982 number-theory example states that a positive integer represented by x^3 − 3xy^2 + y^3 has at least three representations, while 2891 has none.Source: B IMO example · p. 16
• The IMO 1978 combinatorics example encodes a six-country, 1978-member society problem as a same-country sum condition on member numbers.Source: B IMO example · p. 16

• Lean Workbook contains 57,231 problems and Lean Workbook Plus contains 82,893, with natural-language statements, answers, formal statements, and proofs when available.Source: C Dataset card · p. 16
• The code and data are open-sourced under an Apache 2.0 dataset license, with plans to maintain and improve the dataset.Source: C Dataset card · p. 16