{"id":"6eaaa329-b937-4ab7-afec-7f4e8a2fc434","arxiv_id":"2411.18872","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A new Lean dataset contains 1,329 verified lemmas decomposed from IMO proofs, on which current LLMs prove only about a quarter to two-fifths of the lemmas.","lead":"The authors wrote complete Lean formal proofs for 14 International Math Olympiad problems in the miniF2F benchmark that previously had no public proofs, plus three newer problems. They then broke these proofs into 1,329 smaller lemmas, creating a dataset for evaluating how well AI models write formal proofs, and tested several large language models on it.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma dataset likely mixes standalone steps with hypothesis-granting variants; aggregate counts and LLM accuracies may overstate the benchmark's diagnostic value.","rationale":"The core contribution—17 machine-checked Lean proofs and a 1,329-lemma dataset with formally verified proofs—is supported by the nature of Lean itself: every listed lemma and proof compiles in Lean 4.17, so the existence claims are strong. The reader's weakest assumption about the meaningfulness of the decomposition is reasonable, and my concern is a concrete version of it: Section 4.1 explicitly generates lemmas by granting arbitrary subsets of previously proved hypotheses to the original problem, which can produce many context-specific variants of the same target. The paper does not report how many of the 1,329 entries are such variants, nor whether the reported model accuracies are stable if only distinct conclusions are counted. This is a genuine gap in the benchmark's validation, but it is not fatal: the paper frames the dataset as a diagnostic stepping stone, acknowledges the planning/execution separation in Section 6, and the formal artifacts exist regardless. Minor numerical inconsistencies between Tables 5 and E4 (one DeepSeek count difference) also do not change the verdict. I therefore keep the reader's ACCEPT unchanged while recommending the dataset-level redundancy check as a worthwhile verification step.","tokens_in":19990,"tokens_out":13053,"duration_ms":122634,"concrete_test":"In the released repository, group the 1,329 lemmas by their conclusion (after normalizing variable names), treating two lemmas as the same mathematical target if their goals match and they differ only in granted hypotheses. Recompute the number of distinct conclusions and recompute Table 5 accuracies on that subset. If the count falls by more than ~30% or the model ranking changes, the aggregate 1,329-lemma and percentage claims are an artifact of the hypothesis-granting construction and should be qualified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 4.1's decomposition procedure creates, for each intermediate hypothesis, both a standalone lemma and additional lemmas that grant some of those hypotheses back to the original theorem (e.g., 'grant lemmas 1,2,3,4 to the original problem and prove ...'). Such variants are proof-state snapshots rather than independent mathematical building blocks. The paper reports 1,329 lemmas and per-model accuracies as a single aggregate. If a substantial fraction of the 1,329 entries are these granted-variant lemmas, the headline numbers conflate performance on genuinely new facts with performance on context-specific goals, weakening the central claim that the dataset is a 'stepping stone' diagnostic for proving IMO problems. The paper does not disclose the fraction of such variants or show that the aggregate results are robust when only distinct target statements are counted. This is a real validation gap in the benchmark contribution, though it does not affect the machine-checked existence of the proofs.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper contributes original Lean 4 formal proofs for 17 IMO problems that previously lacked public Lean proofs, of which 14 are from the miniF2F test set and 3 are from IMO 2022 and 2023. From 13 of these proofs the authors extract a dataset of 1,329 lemmas (about 40k lines of Lean code) and evaluate six LLM-based provers on it, reporting accuracies between 0% and 39.3%. The paper also provides a detailed manual error taxonomy for o3-mini's failed proofs, including hallucination, wrong approach, wrong implementation, incomplete proof, and minor errors. All formal proofs and lemmas are machine-checked in Lean 4.17, and the dataset and code are released on GitHub.","tokens_in":20104,"tokens_out":5583,"duration_ms":51736,"significance":"If the claims hold, this is a valuable community resource: it supplies verified Lean proofs for hard IMO problems that were missing from the public domain, and it provides a sizable, machine-checked lemma set for evaluating and diagnosing automated theorem provers. The evaluation is informative because it covers multiple models, includes open and closed training-set regimes, and reports human-reviewed error categories. The paper's central limitation is the unclear composition of the 1,329 lemmas: Section 4.1 explicitly creates both standalone lemmas and hypothesis-granting variants, but the paper never reports how many of the 1,329 are of each type, which affects the interpretation of the headline accuracies as a measure of performance on the 'building blocks' of IMO proofs. The machine-checked existence of the proofs is not in question.","major_comments":[{"comment":"The decomposition procedure creates two structurally different kinds of lemmas: standalone intermediate facts (Lemmas 1–4 in the example) and variants that grant some of those facts back to the original problem (Lemmas 5–8). The paper says the examples lead to 2*k lemmas per proof, meaning a large share of the dataset could consist of hypothesis-granting, context-specific proof-state snapshots rather than independent mathematical building blocks. The paper never reports the fraction of such variants in the 1,329 lemmas, nor does it report accuracies separately for the standalone subset. This is load-bearing for the benchmark claim: aggregate accuracies in Tables 2, 3, and 5 conflate the ability to discover a fact with the ability to use a granted hypothesis. Please add a breakdown by lemma type and show that the main conclusions (low absolute accuracy, length-based failure patterns, and problem-level rankings) are robust when only distinct standalone target statements are counted.","section":"§4.1, Lemmas 5–8"},{"comment":"The paper describes the decomposition as a 'method' and derives formal bounds, but the actual selection of which intermediate hypotheses to turn into lemmas, and which granted variants to include, is made by human judgment and is not specified algorithmically. The datasheet in Appendix H also states that lemmas provable by certain automatic solvers were excluded. As a result, the 1,329 lemmas are not a reproducible, exhaustive decomposition of the 13 proofs, and the dataset's coverage of the proof space is unclear. The authors should state explicitly which choices were made, provide the code or criteria used to identify intermediate hypotheses, and discuss how the exclusion of solver-provable lemmas affects the dataset's claim to represent the 'building blocks' of these IMO problems.","section":"§4.1 and §4.2"}],"minor_comments":[{"comment":"The number of lines of Lean proof is given as 5,880 in the abstract, 5,790 in Section 1.4, and 5,884 in Table C2; these should be reconciled.","section":"Abstract; §1.4; Table C2"},{"comment":"The introduction states the dataset has 1,330 lemmas, while the abstract, Table 1, and Table D3 all report 1,329; please correct the inconsistency.","section":"Introduction; Table 1; Table D3"},{"comment":"The DeepSeek-Prover total differs between Table 5 (522, 39.3%) and Table E4 (523, 39.4%); the same evaluation should yield a single count.","section":"Table 5; Table E4"},{"comment":"There is a typo in 'stat-of-the-art'; it should read 'state-of-the-art'.","section":"§1.4"},{"comment":"The phrase 'derive an upper bound' is imprecise because the expressions (n−2)+(n−2)+(n−3) are exact counts for the described forward/backward procedures, not an upper bound over all possible decompositions.","section":"§4.2"},{"comment":"The datasheet's categorical 'No' regarding errors and redundancies is stronger than what machine-checking establishes: Lean verifies the formal statements and proofs as written, but it does not verify that the lemmas are the intended cognitive 'building blocks' or that they are non-redundant in the proof's reasoning.","section":"Appendix H, 'Are there any errors...'"}],"recommendation":"major_revision","confidential_remarks":"The core artifact—machine-checked Lean proofs and a released dataset—is real and valuable. My main concern is the lack of a breakdown between standalone lemmas and hypothesis-granting variants, which affects the benchmark's interpretability. If this review is for the archival record given that the paper is already published in TMLR, I would encourage the authors to issue a corrected version or addendum with the requested breakdown and count reconciliation."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First, this paper delivers a real, verified artifact: 17 new Lean proofs for IMO problems that lacked them (14 in miniF2F), plus 1,329 machine-checked lemmas with over 40k lines of Lean code. That part is solid; the proofs are checked by Lean 4.17. Second, the headline LLM accuracies are harder to interpret than they look, because the lemma set mixes two kinds of tasks. Section 4.1 explicitly says that for each intermediate hypothesis they create both a standalone lemma and additional lemmas that grant some hypotheses back to the original theorem—for example, 'grant lemmas 1,2,3,4 to the original problem and prove ...'. Those granted-variant lemmas are proof-state snapshots, not independent building blocks. The paper never reports what fraction of the 1,329 lemmas are these variants, so the per-model percentages (23.8% to 39.3%) conflate proving a fact from scratch with finishing a goal given intermediate results. That is a real validation gap in the benchmark's diagnostic value, though it does not affect the existence or correctness of the proofs.\n\nWhat is genuinely new: the missing miniF2F proofs, the scale of the lemma dataset, and the multi-model evaluation with a careful error taxonomy. The discussion of training-set contamination and the choice of models with different training data is thoughtful. The citation picture looks solid; the relevant prior work is covered. The paper is also honest in its limitations appendix about focusing on building blocks rather than planning.\n\nSoft spots, in proportion: the granted-variant issue is the biggest and is fixable by reporting standalone and variant accuracies separately. The manual decomposition and the exclusion of solver-provable lemmas are disclosed in the datasheet, so they are selection properties rather than hidden flaws. There are minor numerical inconsistencies (DeepSeek totals 522 in Table 5 but 523 in Table E4), and the o3-mini feedback evaluation appears to be a single run without reported variance. None of these are load-bearing.\n\nWho this is for: anyone building or evaluating LLM-based theorem provers, plus the ATP community broadly. It deserves serious peer review. My recommendation: send it to review, and in review ask the authors to split the lemma counts by type and re-run the headline numbers. Even without that split, the verified proofs alone justify publication.","headline":"A valuable, machine-checked dataset of IMO proofs and lemmas, but the headline LLM accuracies mix two task types the paper never separates.","tokens_in":20639,"tokens_out":4600,"would_cite":true,"duration_ms":36686,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper provides public Lean proofs for 17 IMO problems that lacked them, decomposes 13 of those proofs into 1,329 machine-checked lemmas, and reports that state-of-the-art LLMs prove at most 39.3% of those lemmas.","keywords":["Lean","formal proof","interactive theorem proving","International Math Olympiad","miniF2F","lemma decomposition","LLM evaluation","automated theorem proving"],"falsifier":"Give a strong automated prover, or a human expert, access to all 1,329 verified lemmas as an allowed library and ask it to prove the 13 full IMO statements. If a system that proves essentially all the lemmas still cannot assemble any full proof, the decomposition is not capturing the reasoning needed. A narrower check is to hide the final step of each proof and see whether models can use the granted lemma to finish, which the chained lemmas in the dataset already make possible.","tokens_in":19773,"feed_emoji":"🧮","tokens_out":12183,"duration_ms":96276,"temperature":0.7,"pith_summary":"This paper tries to remove a basic obstacle for AI systems that prove hard mathematics: for almost half of the IMO problems in the standard miniF2F benchmark, no correct formal proof was publicly available, so failures could not be diagnosed. The authors write complete Lean proofs for the 14 missing miniF2F IMO problems plus three from IMO 2022 and 2023, then break 13 of those proofs into 1,329 smaller verified lemmas that form a stepping-stone dataset. They evaluate several state-of-the-art LLMs on these lemmas and report that the best model, DeepSeek-Prover-V1.5-RL, proves only 39.3% of them, while o3-mini reaches 23.8% after ten rounds of automated feedback and general-purpose math models prove 1 or 0 lemmas. If these lemmas really are the building blocks of IMO proofs, the dataset lets the community locate exactly where automated provers break down and measure progress well before full olympiad problems are solved.","feed_headline":"AI theorem provers solve under 40% of new IMO lemma set","feed_subtitle":"Paper decomposes 13 IMO proofs into 1,329 verified lemmas; best model proves 39%.","key_machinery":"The central object is a proof-decomposition procedure that turns one long formal proof into a dataset of approachable building-block lemmas. The procedure finds intermediate hypotheses inside a proof, states each hypothesis as a standalone lemma, and also creates new lemmas by granting some of those hypotheses back to the original statement so that each extracted lemma has a proof that is a segment of the full proof. Lean's type checker is the machine that certifies every lemma, and lemmas that existing automatic solvers can already prove were excluded so the benchmark focuses on reasoning that current automation does not handle.","core_discovery":"The central claim is that a hard IMO proof can be rewritten as a graded collection of small, individually checkable lemmas, and that current AI systems still fail on most of these small pieces. The paper contributes complete Lean 4 proofs for 17 IMO problems that previously had no public Lean proof, and for 13 of those problems it extracts 1,329 lemmas, each with a proof verified by Lean, totaling more than 40,000 lines of formal code. On this lemma dataset the best evaluated model proves 522 of 1,329 lemmas (39.3%), o3-mini after feedback proves 316 (23.8%), and the successful proofs produced by specialized provers are almost all short (at most 15 lines), although many human-written lemma proofs are considerably longer. The paper interprets this as evidence that the current bottleneck is less about executing individual proof steps and more about planning and sustaining long proof chains.","pith_inferences":["A natural extension, not run in the paper, is to fine-tune an open model on the 1,329 lemmas while withholding the 13 full proofs, then measure transfer to the full IMO statements; success would confirm the building-block hypothesis, and failure would localize the bottleneck as assembly rather than execution.","The same decomposition recipe could be applied to other long formal proofs to generate curricula for any proof library, and the paper's bounds on how many lemmas can be extracted from n lines of proof give a rough cost model for doing so.","The large gap between general-purpose math models (1 lemma proved) and Lean-specialized provers (roughly 30-40%) suggests that formal-language competence is a distinct skill from informal mathematical reasoning, so hybrid systems pairing a general reasoner with a specialized proof search may be a faster route than one model doing everything.","The benchmark's difficulty will erode as automatic solvers improve, since lemmas solvable by linarith, omega, ring, and similar tactics were deliberately excluded; re-running the decomposition on newer IMO problems would keep the benchmark meaningful."],"forward_implications":["Every IMO problem in the miniF2F test set now has a public Lean proof, so future evaluations can be checked against ground truth instead of missing or altered formalizations.","The 1,329 lemmas give a graded benchmark: a model that cannot prove the small pieces has no credible claim to solving the full problems, while a model that proves the pieces but not the whole proof exhibits a specific planning deficit.","The near-zero accuracy of specialized provers on lemmas whose proofs exceed 10-15 lines identifies long proof chains, not single-tactic steps, as the main thing to improve.","The paper's error labels (hallucination, wrong approach, wrong implementation, incomplete proof, minor error) give a repeatable vocabulary for diagnosing why a generated Lean proof fails.","Because the dataset is public and machine-checked, model developers can use it as a shared benchmark while keeping the full IMO proofs out of training to avoid contamination."],"supporting_citations":[{"why":"Defines the miniF2F benchmark and its 20 IMO test problems, the target set that the paper completes with formal proofs.","marker":"(Zheng et al., 2021)"},{"why":"Introduces the Lean theorem prover, the system used to write and machine-check every proof and lemma.","marker":"(de Moura et al., 2015)"},{"why":"LEGO-Prover, the prior peer-reviewed state of the art on miniF2F, which proved only one IMO problem and is the baseline the paper's dataset and evaluation build on.","marker":"(Wang et al., 2024)"},{"why":"HTPS, a neural prover whose claimed IMO proofs relied on simplified or erroneous problem statements, motivating the paper's insistence on original statements.","marker":"(Lample et al., 2022)"},{"why":"DeepSeek-Prover-V1.5-RL, the model that reaches the best accuracy (39.3%) on the paper's lemma dataset.","marker":"(Xin et al., 2024b)"},{"why":"Goedel-Prover, the strongest model on miniF2F, which proves fewer lemmas than DeepSeek on the new dataset despite its higher miniF2F accuracy.","marker":"(Lin et al., 2025)"},{"why":"LeanDojo and the ReProver model, evaluated both with and without retrieval, supplying the open-source retrieval-augmented prover comparison.","marker":"(Yang et al., 2023)"},{"why":"o3-mini, the general-purpose model whose zero-shot and feedback-augmented attempts receive the paper's detailed human error analysis.","marker":"(OpenAI, 2025)"}],"fun_headline_variants":["AI proves just 39% of new IMO lemma benchmark","Deconstructing IMO proofs into 1,329 testable lemmas","Lean proofs for 17 IMO problems released as AI benchmark","Small lemmas, big failures: AI stumbles on IMO subgoals","New dataset breaks IMO proofs into small steps for AI"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The central claim depends on the assumption that the manually chosen 1,329 lemmas genuinely are the building blocks of the IMO proofs, so a model's success on them measures its ability to prove the full problems.","fun_headline_variants_meta":{"raw":{"variants":["AI proves just 39% of new IMO lemma benchmark","Deconstructing IMO proofs into 1,329 testable lemmas","Lean proofs for 17 IMO problems released as AI benchmark","Small lemmas, big failures: AI stumbles on IMO subgoals","New dataset breaks IMO proofs into small steps for AI"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000524,"raw_usage":{"total_tokens":2589,"prompt_tokens":1058,"completion_tokens":1531,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":674,"completion_tokens_details":{"reasoning_tokens":1439}},"tokens_in":674,"tokens_out":1531,"duration_ms":11234,"temperature":1.0,"reasoning_tokens":1439,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T10:47:33.578656+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Give a strong automated prover, or a human expert, access to all 1,329 verified lemmas as an allowed library and ask it to prove the 13 full IMO statements. If a system that proves essentially all the lemmas still cannot assemble any full proof, the decomposition is not capturing the reasoning needed. A narrower check is to hide the final step of each proof and see whether models can use the granted lemma to finish, which the chained lemmas in the dataset already make possible.","supporting_citations":[{"cited_title":"The Lean theorem prover (system description)","cited_arxiv_id":null,"evidence_quote":"Introduces the Lean theorem prover, the system used to write and machine-check every proof and lemma."},{"cited_title":"OpenAI o3-mini, January 2025","cited_arxiv_id":null,"evidence_quote":"o3-mini, the general-purpose model whose zero-shot and feedback-augmented attempts receive the paper's detailed human error analysis."}],"review_version":1}