Cover Image

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

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Li, Jinzheng, Zhu, Zeru, Ren, Yuanjie
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Computation and Language
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

MerLean: An Agentic Framework for Autoformalization in Quantum Computation
by: Ren, Yuanjie, et al.
Published: (2026)

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
by: Tang, Xichen
Published: (2025)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
by: Liu, Chengwu, et al.
Published: (2026)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
Published: (2025)

Formalizing Automated Market Makers in the Lean 4 Theorem Prover
by: Pusceddu, Daniele, et al.
Published: (2024)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
by: Song, Peiyang, et al.
Published: (2024)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
by: Zhang, Terry Jingchen, et al.
Published: (2025)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
by: Aniva, Leni, et al.
Published: (2026)

LeanAgent: Lifelong Learning for Formal Theorem Proving
by: Kumarappan, Adarsh, et al.
Published: (2024)

Process-Driven Autoformalization in Lean 4
by: Lu, Jianqiao, et al.
Published: (2024)

Theorem Provers: One Size Fits All?
by: Oates, Harrison, et al.
Published: (2025)

CSLib: The Lean Computer Science Library
by: Barrett, Clark, et al.
Published: (2026)

Small Scale Reflection for the Working Lean User
by: Gladshtein, Vladimir, et al.
Published: (2024)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
by: Rajaee, Sara, et al.
Published: (2025)

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
by: Lamont, Sean, et al.
Published: (2024)

A complete formalization of Fermat's Last Theorem for regular primes in Lean
by: Best, Alex, et al.
Published: (2024)

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
by: Montesi, Fabrizio, et al.
Published: (2026)

Herald: A Natural Language Annotated Lean 4 Dataset
by: Gao, Guoxiong, et al.
Published: (2024)

Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
by: Henson, Christopher, et al.
Published: (2026)

Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
by: Bourigault, Pauline, et al.
Published: (2026)

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
by: Baek, Jineon, et al.
Published: (2024)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
by: Dong, Kefan, et al.
Published: (2025)

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
by: Santos, Marco Dos, et al.
Published: (2025)

Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
by: Yang, Bowen, et al.
Published: (2026)

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
by: Liu, Qi, et al.
Published: (2025)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
by: Tsoukalas, George, et al.
Published: (2024)

Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving
by: Cao, Chuxue, et al.
Published: (2025)

Combining Textual and Structural Information for Premise Selection in Lean
by: Petrovčič, Job, et al.
Published: (2025)

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4
by: Guan, Naillin, et al.
Published: (2025)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
by: Li, Guchan, et al.
Published: (2026)

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
by: Ji, Junye
Published: (2026)

Intuitionistic Propositional Logic in Lean
by: Trufaş, Dafina
Published: (2024)

Formalizing zeta and L-functions in Lean
by: Loeffler, David, et al.
Published: (2025)

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
by: Xin, Huajian, et al.
Published: (2024)

LeanArchitect: Automating Blueprint Generation for Humans and AI
by: Zhu, Thomas, et al.
Published: (2026)

Lean on Vampire Proofs (Short Paper)
by: Bodingbauer, Jonas, et al.
Published: (2026)