MerLean-Prover: A Recursive Looping Harness for End-to-End Lean 4 Theorem Proving 事件

MerLean-Prover: A Recursive Looping Harness for End-to-End Lean 4 Theorem Proving arXiv:2605.26959v1 Announce Type: cross 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