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

Jinzheng Li, Zeru Zhu, Yuanjie Ren

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) c…