Lean Environment Agentic Prover

An open, trackable prover that works alongside mathematicians

LEAP turns a mathematical argument into a Lean proof that the kernel checks. Every lemma it proposes, every failed attempt and every repair is kept in a proof DAG you can inspect, resume and steer.

OpenThe agent and CLI are open source, and every proof here can be downloaded and re-checked.
TrackableEach run records its whole search: lemmas, dead ends and the Lean code for every step.
Built to assistStart from your own informal proof or blueprint and let LEAP do the formal work.

See the problems Paper LEAP-CLI

Mathematicians

Hyunsik Chae³, Xinjie He³, Raghu Meka³, Amit Sahai³, Zhi Zhang³, Vigyan Sahai³, Carlo Pagano², Moritz Firsching²

LEAP team

Po-Nien Kung^1,3, Linfeng Song¹, Zheng Tan^1,3, Dawsen Hwang², Jinsung Yoon¹, Chun-Liang Li¹, Simone Severini¹, Song Zuo¹, Yuan Deng¹, Jieming Mao¹, Jin Zhou², Qijun Tan², Mirek Olšák², Edward Lockhart², Quoc V Le², Burak Gokturk¹, Thang Luong², Tomas Pfister¹, Vahab Mirrokni¹, Nanyun Peng¹

¹Google
²Google DeepMind
³UCLA

01 · Problems

Featured results

All problems →

02 · How it works

One orchestrator, parallel subagents, and a proof DAG behind a compiler gate

LEAP-CLI keeps the proof DAG. An orchestrator claims the next open work from it and launches subagents in parallel. Each subagent submits its result back to the CLI, and only what the Lean compiler accepts enters the graph.

Trackable

A DAG with backtracking

Every goal, attempt and dead end stays in the proof DAG, so a failed branch can be retried and any run can be inspected or resumed.

Fast

Subagents run in parallel

The orchestrator claims every lemma that is ready and launches a subagent for each, so a wide proof is worked on everywhere at once.

Local

Compiled per lemma

Each submission is compiled on its own against a local Lean server, so even very large graphs never wait on a full rebuild.

03 · Run it

Point LEAP-CLI at a Lean statement and let it work

You need Python, a model endpoint and a Lean server. Give it a theorem whose proof is sorry, optionally with your own informal proof, and it builds the proof DAG until everything compiles.

1
Install
LEAP-CLI is a Python package. Installing it adds the leap-* commands.
```
pip install git+https://github.com/billkunghappy/LEAP-CLI.git
```
2
Start a Lean server
Every submission is compiled here before it can enter the graph. Docker builds the server straight from the repository.
```
docker build -t leap-lean https://github.com/billkunghappy/LEAP-CLI.git#main:src/leap/interfaces
docker run -p 8000:8000 leap-lean
```
3
Prove a theorem
Check that the model and the Lean server respond, then start a run on your statement.
```
leap-check
leap-run-agent --file Problem.lean
```

what a run leaves behind

runs/my_problem/
problem.leanthe statement you gave it
reference/your informal proof or blueprint, if any
proof_graph.jsonthe proof DAG, and the point a run resumes from
nodes/<lemma>/context, findings and logs for each lemma
orchestrator_log.mdwhat was claimed and launched, step by step
solution/answer.leanthe verified proof, written once nothing is left as sorry

The problem pages on this site are built from three of these files: problem.lean, proof_graph.json and solution/answer.lean.

Paper

LEAP: Supercharging LLMs for Formal Mathematics

The agentic framework and its ablations. arXiv 2606.03303.

Tool

LEAP-CLI

Run LEAP on your own Lean statements from the command line.

Cite

BibTeX

@article{kung2026leap,
  title   = {LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks},
  author  = {Kung, Po-Nien and Song, Linfeng and Hwang, Dawsen and Yoon, Jinsung and
             Li, Chun-Liang and Severini, Simone and Ol{\v{s}}{\'a}k, Mirek and
             Lockhart, Edward and Le, Quoc V and Gokturk, Burak and Luong, Thang and
             Pfister, Tomas and Peng, Nanyun},
  journal = {arXiv preprint arXiv:2606.03303},
  year    = {2026}
}