{"id":"bf4b5c2b-732f-4c77-ac09-e28d8ce0d37f","arxiv_id":"2507.06804","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"A decoupled reasoning-and-proving framework generated machine-verified Lean proofs for five post-2000 IMO problems.","lead":"This paper describes an automated theorem proving system that separates strategic mathematical reasoning from step-by-step proof generation, using different AI models for each stage. The system produced machine-checked Lean proofs for five International Mathematical Olympiad problems from 2000 to 2020, including problems not previously solved by open-source provers.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The five reported solutions are completed by closed frontier models (OpenAI-o3/Gemini 2.5 Pro) in the final assembly stage, and the paper reports no direct-proving baseline for these models; without that control, the successes cannot be attributed to the decoupled architecture.","rationale":"I read the paper's central claim as the architectural one: separating a general-purpose Reasoner from a specialized Prover enables solving five previously unsolved post-2000 IMO problems. The strongest available evidence is the five Appendix B proofs, which are substantial and would be valuable if they compile; they should be checked in a pinned Lean environment. However, the load-bearing link in the argument is causal: the reported winners are not produced by the open-source Prover but by the closed models used in Stage 3 (Section 3.3). The paper gives examples of DeepSeek-Prover-v2's degenerate behavior (Section 4.1) and of its 'contextual blindness' to lemmas (Section 4.3), and then switches final assembly to OpenAI-o3 and Gemini 2.5 Pro. The reader's weakest assumption correctly flags the closed-API dependence and the missing denominator; my concern is sharper: without a same-model direct-proving baseline, the five successes may be entirely due to the frontier closed models, making the decoupling architecture unnecessary to explain them. The oracle experiment in the Limitations section (manual proofs or sorry for bottleneck lemmas allow a significantly larger number of problems to be solved) reinforces that the open-source Prover is the bottleneck and that the final proof completion is done elsewhere. I therefore recommend keeping the CONDITIONAL verdict, with the explicit condition that the authors run and report the direct-proving baseline and the attempted-problem denominator. If the baseline shows the closed models cannot prove the five theorems directly, the central claim would be substantially supported. If not, the paper should be reframed as an evaluation of closed reasoners with auxiliary lemma filtering.","tokens_in":34172,"tokens_out":7400,"duration_ms":77232,"concrete_test":"Run a direct-proving baseline: for each of the five theorems (IMO 2000 P2, 2005 P3, 2011 P3, 2019 P1, 2020 P2), prompt OpenAI-o3 and Gemini 2.5 Pro with only the Lean theorem statement (no Reasoner-generated subgoal lemmas), using the same proof-search protocol and budget (e.g., k=128 attempts per theorem), and record whether a Lean proof compiles. Also report the full denominator: the complete list of non-geometry IMO 2000–2024 problems attempted and the per-problem outcome. If any baseline proof compiles, the decoupled framework's contribution on that problem is not established.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central claim is that the decoupled Reasoner–Prover framework solves five post-2000 IMO problems. Section 3.3 states that the open-source Prover (DeepSeek-Prover-v2) ignores provided lemmas, so the final proof assembly is instead performed by OpenAI-o3 and Gemini 2.5 Pro. Consequently, the five Appendix B proofs are outputs of closed frontier models, not of the open-source pipeline that the paper's title and abstract foreground. The paper never reports whether these same closed models, given only the Lean theorem statements and the same compute budget (k=128 candidate proofs), can prove any of the five theorems directly. Without this ablation, the successes may be due to the raw capability of the closed reasoners rather than to the decoupling of reasoning and proving; the architecture's claimed benefit—that strategic subgoal lemmas are necessary to reduce the proof search—is unsupported. The missing denominator (how many non-geometry post-2000 IMO problems were attempted) compounds this, and the paper's own oracle experiment (replacing bottleneck lemmas with sorry) shows that the open-source Prover is the limiting component, further separating the final closed-model assembly from the named Prover. The claim as stated is therefore not established by the reported evidence.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes DRP-IMO, a three-stage pipeline for Lean 4 theorem proving in which a general-purpose LLM Reasoner generates formal subgoal lemma statements, an open-source Prover (DeepSeek-Prover-v2, 7B CoT) attempts to verify those lemmas, and a final assembly stage uses OpenAI-o3 or Gemini 2.5 Pro to combine the verified lemmas into a proof of the main IMO problem. The authors report success on five post-2000 non-geometry IMO problems: IMO 2000 P2, IMO 2005 P3, IMO 2011 P3, IMO 2019 P1, and IMO 2020 P2. They also present a qualitative case study on IMO 2019 P1, a small quantitative experiment on reasoning degradation in Kimina-Prover, an oracle experiment suggesting that the Prover is the main bottleneck, and a release of verified lemmas for a broader set of IMO problems. The central claim is that decoupling reasoning from proving enables machine-verified solutions on problems where prior open-source provers have reported no success.","tokens_in":34377,"tokens_out":3251,"duration_ms":41404,"significance":"If the five proofs are correct and the attribution to the decoupled architecture is valid, this is a meaningful advance: it would provide the first open-source-adjacent pipeline that machine-verifies several difficult post-2000 IMO problems, and the released lemma dataset could be a useful resource. The paper also makes a falsifiable architectural claim about the benefit of separating strategic reasoning from tactical proof search. However, the significance is conditional on reproducibility and on controls that the current manuscript does not provide; the final proofs are generated by closed commercial models, and no direct-proving baseline is reported for those models.","major_comments":[{"comment":"The final proofs of all five solved problems are produced by OpenAI-o3 or Gemini 2.5 Pro, not by the open-source Prover (DeepSeek-Prover-v2) that is the named Prover component in the paper's framing. The manuscript reports that DeepSeek-Prover-v2 ignores provided lemmas, but it does not report any direct-proving baseline in which OpenAI-o3 or Gemini 2.5 Pro attempt the same five Lean statements without the decoupled subgoal pipeline and with the same compute budget (k=128). Without this ablation, the observed successes cannot be attributed to the decoupled architecture; they may reflect the raw proving capability of the closed models. This is the load-bearing control for the paper's central claim and must be added.","section":"Section 3.3 and Appendix B"},{"comment":"The evaluation reports only the five successes and never states the total number of non-geometry post-2000 IMO problems that were attempted, nor a per-problem breakdown of lemma-generation and verification outcomes. The abstract's phrase 'solves 5 of these problems' is therefore compatible with a much larger attempted set, and the claim that this problem set is one 'on which no prior open-source prover has reported success' is likewise asserted without a citation or a systematic comparison. The paper should report the full attempted set, the success/failure status of every problem, and the basis for the no-prior-success claim.","section":"Section 4"},{"comment":"The paper's main evidence consists of five Lean proof scripts, but no build environment, Mathlib version, Lean toolchain version, commit hash, or exact inference prompts and hyperparameters are provided. Several proof scripts use very heavy tactic combinations (e.g., `maxHeartbeats 0`, repeated `nlinarith`, `ring_nf`, `aesop`, `omega`) and contain notation that is not obviously standard Lean 4; as a referee I cannot determine from the text alone whether the Appendix B files compile as printed. The authors should ship a reproducible artifact with exact versions and commands, and confirm that each listed proof compiles in that environment.","section":"Sections 3.2, 3.3, and Appendix B"},{"comment":"The qualitative comparison in Section 4.1 is based on three sampled, partially quoted attempts from DeepSeek-Prover-v2 and is not a controlled experiment; it cannot support the claim that the decoupled framework's reasoning path is the cause of success. Similarly, the RLVR-degradation experiment in Section 4.2 uses one base model and one prover derived from it, with no error bars or repetition across models; the reported drops, especially at pass@1, are suggestive but not strong enough to carry the paper's motivational thesis. These sections should be reframed as illustrative or supplemented with a systematic comparison on the solved problem set.","section":"Section 4.1 and Section 4.2"}],"minor_comments":[{"comment":"There are typographical errors such as 'experiemnts' in Section 4; the paper should be copy-edited.","section":"Section 4"},{"comment":"The text describing the final proof construction appears twice with slightly different wording; one of the duplicated paragraphs should be removed.","section":"Section 3.3"},{"comment":"Figure 1 is difficult to read at the resolution provided; the subgoal statements and the correspondence between reasoning steps and formal lemmas should be presented more legibly.","section":"Figure 1"},{"comment":"Table 1 reports pass@k only for AIME24 and only pass@1 for MATH; the sampling setup, the number of samples, and whether pass@k is unbiased are not specified, so the numerical comparisons should be interpreted cautiously.","section":"Table 1"},{"comment":"The paper refers to PutnamBench and to the claim that informal accuracy exceeds 80% while formal success is below 8%, but the precise source of these numbers should be cited directly rather than cited only through a general reference.","section":"Abstract and Section 1"},{"comment":"The theorem names are inconsistent across the appendix (e.g., `imo2019_p1` in some places and `imo2020_q2` in others); uniform naming would improve readability.","section":"Appendix B"}],"recommendation":"major_revision","confidential_remarks":"The central claim is potentially significant but is currently not established because the decisive final-proving step is performed by closed API models without a direct-proving control, and because the success denominator is omitted. Before this paper can be accepted, the authors need to supply the missing ablation, the full attempted set, and a reproducible artifact. I would also ask the editor to consider whether the heavy reliance on commercial models (OpenAI-o3, Gemini 2.5 Pro) with undisclosed prompts and budgets is acceptable for the journal's reproducibility standards; at minimum it must be disclosed prominently in the abstract and conclusions."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Five Lean proofs and a cleaner decoupling story than most ATP papers. If those appendix proofs compile, they are real artifacts, and the division of labor—one model proposes formal lemma statements, another verifies them, a third assembles the final proof—is a sensible way to separate strategy from tactic execution. The dataset of verified lemmas across a range of IMO problems is a genuine resource, and the IMO 2019 case study gives a concrete picture of what the authors mean by strategic decomposition.\n\nThe soft spots are the two that the stress-test flags, and they are real. First, no denominator: the paper never reports how many non-geometry post-2000 IMO problems were attempted, so five successes from an unknown pool cannot be evaluated. Second, the final assembly is done by OpenAI-o3 and Gemini 2.5 Pro, not the open-source Prover, because DeepSeek-Prover-v2 ignored the provided lemmas. The paper never shows whether those same closed models, given only the theorem statement and the same candidate budget, can prove any of the five directly. Without that control, the headline claim that decoupling is what earns the five solutions is not established; the raw capability of the closed reasoners could be doing the work. The paper is transparent about the prover switch and the limitations section admits the Prover is the bottleneck, which is honest but further separates the named pipeline from the final results.\n\nSmaller issues: no build environment, commit hash, or exact prompt set, which makes independent replication harder. The proofs lean heavily on tactics like nlinarith and omega, fine if they compile, but a compiler log would help. The RLVR degradation experiment (Kimina vs its base model on MATH/AIME) is suggestive but not load-bearing for the main claim.\n\nThe core idea is credible and the artifacts are worth serious referee time. A referee should ask for the attempted set size, a direct-proving baseline for the closed final-stage models, and a reproducibility appendix. If those come back clean, this is a meaningful capability result. Send it to review.","headline":"Five Lean proofs and a clean decoupling story, but the missing direct-proving control and unreported attempt pool keep the central claim from being fully established.","tokens_in":34957,"tokens_out":3207,"would_cite":true,"duration_ms":37048,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","68V05"],"pacs":[],"model":"deepseek-v4-flash","headline":"A two-model pipeline—one model proposing lemma statements, another verifying them—produces machine-verified Lean proofs for five post-2000 IMO problems.","keywords":["automated theorem proving","Lean formal proofs","IMO problems","decoupled reasoning and proving","subgoal lemmas","large language models","reinforcement learning with verifiable rewards","reasoning-proving gap"],"falsifier":"Publishing the complete list of attempted post-2000 IMO problems with per-problem outcomes, or re-running the pipeline with open-weights models and fully specified prompts, would settle the claim. Concretely: if the attempted set is shown to include many more than the five reported problems, or if an independent run with the same prompts on the stated API models fails to reproduce even one of the five verified proofs, the central claim would be refuted.","tokens_in":33943,"feed_emoji":"🏆","tokens_out":6114,"duration_ms":64398,"temperature":0.7,"pith_summary":"Large language models can reason about hard mathematics informally—over 80% accuracy on PutnamBench—but their formally verified proofs lag far behind, below 8%. This paper argues that the gap is self-inflicted: state-of-the-art provers couple planning and proof generation inside one model trained to maximize the binary reward of a completed proof, which pushes them toward shallow tactic-bashing instead of deep strategy. The proposed fix is a decoupled pipeline in which a general-purpose Reasoner emits only formal lemma statements, a specialized Prover checks each lemma, and a final model assembles the proof from the verified lemmas. On a set of post-2000 non-geometry IMO problems where the authors state no open-source prover had previously reported a success, the pipeline produces machine-verified Lean proofs for five: IMO 2000 P2, 2005 P3, 2011 P3, 2019 P1, and 2020 P2. A sympathetic reader should take the paper as evidence that the bottleneck in formal proving is not raw reasoning power but the architecture that couples reasoning to tactic-level proof search.","feed_headline":"Two-model pipeline solves five IMO problems in Lean","feed_subtitle":"Separating strategic lemma generation from formal proof checking beats monolithic provers on post-2000 competition problems.","key_machinery":"The load-bearing mechanism is the subgoal-lemma bridge. The Reasoner (the authors use Gemini 2.5 Pro) is prompted to think through a proof strategy and output only the formal Lean statements of intermediate theorems, terminated by 'by sorry'; a regular expression extracts the declarations. The Prover (DeepSeek-Prover-v2 7B, CoT variant) then attempts each lemma with up to $k=128$ proof candidates, retaining only lemmas for which at least one attempt succeeds. Finally, a model adept at proof continuation (OpenAI-o3 or Gemini 2.5 Pro) receives the verified lemmas in context and assembles the main proof. The framework also documents a phenomenon the authors call 'contextual blindness': many provers ignore pre-proven standalone lemmas and try to reprove the theorem from scratch, which is why the final stage uses reasoner models rather than the specialized prover.","core_discovery":"The paper's central claim is that high-level mathematical reasoning and low-level formal proof generation should be performed by distinct, specialized models: a Reasoner that proposes strategic subgoal lemmas as formal statements, and a Prover that verifies them. The authors identify the prevailing training paradigm—reinforcement learning with verifiable rewards, which rewards only final proof success—as the root cause of the reasoning-proving gap, arguing that it degrades the latent reasoning of prover models and encourages brute-force tactic application. As evidence, they report that a specialized prover (Kimina-Prover) scores lower than its general-purpose base model (Qwen2.5-Math-7B-Instruct) on MATH and AIME24, and they present a case study on IMO 2019 P1 in which a monolithic prover's attempts reduce to flat instantiations and tactic calls, while the decoupled Reasoner recovers the shifted-Cauchy structure of the solution. The paper's headline result is that the decoupled framework produces verified Lean proofs for five post-2000 IMO problems that, on the paper's problem set, no prior open-source prover had solved.","pith_inferences":["The paper never states how many post-2000 non-geometry IMO problems were attempted, so the five successes cannot yet be converted into a success rate; if the intended denominator is roughly the one hundred non-geometry problems from 2000 to 2024, the correct headline would be 'five of about one hundred,' not simply 'five solved.'","If the diagnosis generalizes, the same decoupled design should transfer to other proof assistants and to non-competition mathematics: any domain where a strong informal reasoner can name the right intermediate statements while a weaker tactic engine verifies them.","A testable extension would be to run the full pipeline with an open-weights Reasoner and fully public prompts; if the same five problems still verify, the result would no longer depend on closed API models.","The Kimina/Qwen degradation comparison is a single model pair, so the claimed RLVR-induced degeneration would be stronger if replicated across other prover/base-model pairs."],"forward_implications":["If the decoupling principle is correct, the poor formal-proving performance of LLMs is not a reasoning deficit but a training and architecture artifact, so the same general-purpose reasoning models that score high on informal benchmarks can be redirected into formal proof search.","The five verified Lean proofs become concrete baselines: any future open-source prover can be checked against them, and the released verified-lemma dataset gives the community intermediate milestones for problems that remain unsolved.","The pipeline's bottleneck analysis implies that improving the Prover—either by stronger proof search or by fine-tuning provers to use given lemmas—should directly increase the number of solvable IMO problems, since an oracle experiment with human-proved lemmas solved significantly more.","The RLVR degradation result suggests that training signals for provers should reward strategic structure or lemma use, not only final proof success, if the community wants provers that scale to olympiad-level problems."],"supporting_citations":[{"why":"Supplies the PutnamBench evidence of the informal/formal accuracy gap (over 80% informal versus under 8% formal) that motivates the paper.","marker":"(Dekoninck et al., 2025)"},{"why":"DeepSeek-Prover-V2 is both the state-of-the-art monolithic baseline the paper critiques and the Prover model used in the decoupled pipeline.","marker":"(Ren et al., 2025)"},{"why":"Kimina-Prover is the specialized prover whose MATH and AIME24 degradation relative to its base model is used to support the RLVR-degradation hypothesis.","marker":"(Wang et al., 2025)"},{"why":"Draft, Sketch, Prove is the closest multi-stage pipeline the paper distinguishes itself from by generating formal lemma statements rather than autoformalizing an informal proof.","marker":"(Jiang et al., 2023)"},{"why":"Lean 4 is the proof assistant in which all subgoals and final proofs are formally verified.","marker":"(Moura & Ullrich, 2021)"},{"why":"Introduces the expert-iteration and verifiable-reward training paradigm whose binary reward signal the paper diagnoses as the cause of reasoning degradation in provers.","marker":"(Polu & Sutskever, 2020)"}],"fun_headline_variants":["Decoupled reasoner and prover crack five IMO problems in Lean","Five post-2000 IMO problems solved in Lean via decoupled reasoning","Open-source first: decoupled reasoning solves five IMO problems in Lean","Decoupling reasoning and proving yields five IMO proofs in Lean"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole result rests on the unstated size of the attempted IMO problem set and on the closed API models used for the final proof assembly: if the five solved problems were selected from a much larger pool, or if the commercial reasoners needed human-tuned prompts or oracle hints, the claim of first success on this problem set loses its force.","fun_headline_variants_meta":{"raw":{"variants":["Decoupled reasoner and prover crack five IMO problems in Lean","Five post-2000 IMO problems solved in Lean via decoupled reasoning","Open-source first: decoupled reasoning solves five IMO problems in Lean","Decoupling reasoning and proving yields five IMO proofs in Lean"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00187,"raw_usage":{"total_tokens":7385,"prompt_tokens":1037,"completion_tokens":6348,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":653,"completion_tokens_details":{"reasoning_tokens":6270}},"tokens_in":653,"tokens_out":6348,"duration_ms":49283,"temperature":1.0,"reasoning_tokens":6270,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T19:24:22.979059+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Publishing the complete list of attempted post-2000 IMO problems with per-problem outcomes, or re-running the pipeline with open-weights models and fully specified prompts, would settle the claim. Concretely: if the attempted set is shown to include many more than the five reported problems, or if an independent run with the same prompts on the stated API models fails to reproduce even one of the five verified proofs, the central claim would be refuted.","supporting_citations":[{"cited_title":"The lean 4 theorem prover and programming language","cited_arxiv_id":null,"evidence_quote":"Lean 4 is the proof assistant in which all subgoals and final proofs are formally verified."}],"review_version":1}