MerLeanProver/MerLean
11 stars · Last commit 2026-09-29
An autonomous Lean 4 + Mathlib theorem-proving system, built as Claude Code skills and subagents over a plan graph.
README preview
# MerLean Three mathematics agents, available in **Claude Code and Codex**: six entrypoints in total. | Agent | When to use it | Verification target | | --- | --- | --- | | **MerLean -lite** | Explore a question, develop a natural-language proof, debate it, and Lean-check its weakest links | **SILVER** | | **MerLean -heavy** | Fully prove a result, formalize an existing proof or paper, or complete Lean proofs | **GOLD** | | **Paper-writing** | Compose, refine, resume, or audit a mathematics paper | Preserve the recorded research grade | **Lite is on by default.** Bare MerLean selects Lite; `-heavy` is the explicit name for the former “Lite off” state. The flags are mutually exclusive. Silver and Gold are evidence thresholds, not labels awarded automatically: unfinished Lite work may remain Bronze, and Heavy cannot report Gold until its full audit passes. Lite does not silently escalate to Heavy. ## Choose a workflow - “MerLean: investigate this question” → Lite. - “MerLean -lite: check this proposed proof” → Lite, even though a proof is attached. - “MerLean -heavy: finish this result to Gold” → Heavy.