MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

• URL: http://arxiv.org/abs/2605.26959v2
• Date: Wed, 27 May 2026 04:48:39 GMT
• Title: MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
• Abstract summary: MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs.<n>On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23.<n>The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.

Related papers

• Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study [0.20415910628419062]
  Large language models (LLMs) can generate text that resembles a mathematical proof, but resemblance does not establish correctness.<n>Coq bases its rules on the Calculus of Inductive Constructions, a logical framework that defines which proof steps the system may accept.<n>This pilot study evaluated six open-weight LLMs on the same 100 theorems from CoqStoq, a benchmark derived from real Coq projects.
  arXiv  Detail & Related papers  (2026-08-05T21:29:12Z)
• Harnessing Code Agents for Automatic Software Verification [0.47154736035631406]
  Large language models (LLMs) promise to generate proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system.<n>We show that imposing such a strategy is unnecessary and limiting.<n>Handing the whole lemma to a general code agent, free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective.
  arXiv  Detail & Related papers  (2026-07-07T14:39:59Z)
• Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement [69.77146194380488]
  We introduce Goedel-Architect, a framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement.<n>Goedel-Architect attains 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench.<n>This represents state-of-the-art performance for an open-source pipeline at a price point up to 500x less than comparable open-source pipelines.
  arXiv  Detail & Related papers  (2026-06-04T17:54:44Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization.<n>Four contract-scoped agents construct, audit, prove, and repair this blueprint.<n>We evaluate LeanMarathon on two recent research papers spanning four Erds problems.
  arXiv  Detail & Related papers  (2026-06-03T20:09:39Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4 [1.2816802110958607]
  We introduce proof-state snapshotting, which captures the elaborated proof state once and reuses it across branches via a small extension to the Lean 4 language server.<n>Across 48 miniF2F-v2 problems, our approach achieves a 5.6-50x wall-time speedup over the standard fallback.
  arXiv  Detail & Related papers  (2026-05-25T08:12:26Z)
• OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
  OProver is a unified framework for agentic formal iteration theorem proving in Lean 4.<n>It runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL.<n>OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.
  arXiv  Detail & Related papers  (2026-05-17T06:39:05Z)
• Hilbert: Recursively Building Formal Proofs with Informal Reasoning [38.36481253622752]
  Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions often contain errors that cannot be automatically verified.<n>We introduce Hilbert, an agentic framework that combines the complementary strengths of informal reasoning and formal verification.<n>Our system orchestrates four components: an informal LLM that excels at mathematical reasoning, a specialized prover LLM optimized for Lean 4 tactics, a formal verifier, and a semantic theorem retriever.
  arXiv  Detail & Related papers  (2025-09-26T18:24:23Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  We introduce LeanProgress, a method that predicts the progress in the proof.<n>Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.1%.
  arXiv  Detail & Related papers  (2025-02-25T07:46:36Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  This paper focuses on improving LLMs' ability to write proofs in formal languages that permit automated proof verification/evaluation. We work in a more natural setup where the lemmas that are directly relevant to the theorem are not given to the theorem prover at test time. We design an RL-based training algorithm that encourages the model to decompose a theorem into lemmas, prove the lemmas, and then prove the theorem by using the lemmas.
  arXiv  Detail & Related papers  (2024-11-04T05:57:40Z)
• Theorem-Validated Reverse Chain-of-Thought Problem Generation for Geometric Reasoning [53.13514542825493]
  We introduce a two-stage Theorem-d Reverse Chain-of-Thought Reasoning Synthesis (TRCoT) framework.<n>The first stage, TR-Engine, synthesizes theorem-grounded geometric diagrams with structured descriptions and properties.<n>The second stage, TR-Reasoner, employs reverse reasoning to iteratively refine question-answer pairs by cross-validating geometric properties and description fragments.
  arXiv  Detail & Related papers  (2024-10-23T13:58:39Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  We introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. We fine-tune the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs. Our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any.
  arXiv  Detail & Related papers  (2024-05-23T09:03:42Z)
• REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
  We show that REFACTOR can extract 19.6% of the theorems that humans would use to write the proofs. With newly extracted theorems, we show that the existing MetaMath database can beed. We also demonstrate that the prover trained on the new-theoremed dataset proves more test theorems and outperforms state-of-the-art baselines.
  arXiv  Detail & Related papers  (2024-02-26T21:21:30Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.