MerLeanProver/MerLean

README preview

# MerLean

**Autonomous mathematics agents over a plan graph** — from an informal question to a
machine-checked Lean 4 + Mathlib result, and from a finished campaign to a publishable paper.

Give the research agent a paper, a stubbed `sorry`, or an informal open question. It decomposes
the goal into a dependency graph of lemmas, proves each node in its own file with a dedicated
`compile-fix` subagent, and drives the whole plan to a **sorry-free, axiom-clean** proof — one
whose `#print axioms` output is exactly `[propext, Classical.choice, Quot.sound]`, with no
`sorry` in the dependency cone. When speed matters more than certification, its **lite mode**
works NL-first — adversarial skeptic debate plus Python experiments — and fires Lean only at
the weakest links. When the mathematics is done, the paper-writing agent turns the campaign
into a paper through a gated 8-step protocol.

## Two agents × N runtimes

|  | **Claude Code** | **Codex** | *(future: opencode, …)* |
|---|---|---|---|
| **Research agent** — formalize / prove / auto-research / lite-research | [`.claude/`](.claude) (live at the repo root — the repo *is* the Claude Code install) *or* installable as a plugin ([`.claude-plugin/`](.claude-plugin) + [`skills/`](skills) + [`agents/`](agents)) | [`research-agent/codex/`](research-agent/codex) | one folder per runtime |
| **Paper-writing agent** — campaign → gated 8-step paper | [`paper-writing-agent/claude/`](paper-writing-agent/claude) (invoked via `/write-paper`) | [`paper-writing-agent/codex/`](paper-writing-agent/codex) | one folder per runtime |

View full repository on GitHub →