LeanProver

Description

LeanProver asks a model to prove one theorem in Lean 4. The prompt gives the statement in Lean and in natural language, the source of the definitions it depends on and, for theorems that were originally proved from earlier results, the statements of those results. The model reasons in natural language for as long as it wants and then submits a complete Lean file through a single tool. The environment compiles that file inside a sandbox that already holds Mathlib, checks that some declaration of the file really has the statement's type, that the proof rests only on the standard axioms and the lemmas the task allows, and replays the module through Lean's independent kernel checker. A credited proof pays reward 1; a failed attempt returns Lean's own diagnostics, with line numbers pointing into the submitted code, and the model may try again.

The statements come from the corpora of the sibling environment Prove2Me: the machine-checked theorem library of the Prove2Me platform, plus the competition exercises of NuminaMath-LEAN and Lean Workbook re-verified against the same toolchains. Prove2Me asks an agent to formalize a blueprint from a shell; LeanProver keeps the same ground truth but removes the workspace, so the task is proof search and Lean fluency rather than project navigation.

Capabilities

• Proving theorems in Lean 4 against a fixed Mathlib
• Translating a natural-language argument into a machine-checked proof
• Working from a library's own definitions and previously proved results
• Reading Lean's error messages and repairing a proof across attempts
• Single-turn reasoning at length before committing to an answer

Compute Requirements

Each rollout gets one sandbox with 4 CPUs and 16 GB of RAM, started from the corpus image (about 17 GB) that already contains the Lean toolchain, the pinned Mathlib build and the corpus definitions. The environment server itself needs 1 CPU and 4 GB.

License

MIT for this environment's code. The Prove2Me platform's theorems, definitions and proofs are open for anyone to read and reuse per its FAQ; NuminaMath-LEAN, Lean Workbook and Mathlib are Apache-2.0.

Tasks

A task is one theorem. Every task carries a tier measured from the corpus, not guessed:

Two corpora, one per Lean environment of the platform, each with its own sandbox image:

Task counts after dropping every card whose own accepted proof this environment's rules would reject:

The test split is the one Prove2Me holds out: every theorem reachable from about 20% of the platform's missions (chosen by a hash of the mission id), plus a 5% sample of the single-theorem tasks. Theorems present in both corpora are tasks only in p2m4331. About 79% of the training tasks are exercises, so a curriculum that wants fewer should sample by tier.

A theorem becomes a task only if its own accepted proof is credited by this environment, so the reward is always attainable. data/<corpus>/drop_cards.txt records every excluded theorem with its reason:

Reward Structure

Binary and verifiable, with no model grader anywhere. A submission is credited, and pays reward 1.0, only if all of the following hold:

1. the file compiles within ten minutes with no error and none of the forbidden constructs (sorry/admit, axiom, unsafe, native_decide, implemented_by/extern, set_option debug.*, command-level meta-programming, #exit, #help);
2. some declaration of the file has a type definitionally equal to the statement's, with no universe parameter of the statement specialised;
3. the axioms that declaration transitively depends on are only propext, Classical.choice and Quot.sound, plus the card axioms of the lemmas the task lists (each of strictly smaller height, and each declared by its own stub module) — so a proof may not cite the theorem it is proving;
4. lake env leanchecker replays the module through Lean's independent kernel checker.

Anything else pays 0. The model has 3 attempts; a failed attempt returns Lean's messages and the number of attempts left, a credited one ends the episode. Attempts consumed by a submission the environment rejects before compiling (a forbidden construct, a disallowed import, an oversized file) still count, but an infrastructure failure refunds the attempt.

Data

data/<corpus>/statements.jsonl.gz holds one record per theorem — the Lean statement with its imports and preamble, the platform's natural-language statement, the source citation and contributor — and data/<corpus>/definitions.jsonl.gz the full source of every definition module. Both are extracted from the Prove2Me build outputs; the accepted proofs are not part of this repository and are in no image. data/<corpus>/tasks.json carries the tasks and splits, dag.json.gz the citation graph that decides which lemmas a hard task may use, and drop_cards.txt the theorems excluded with the reason.

Statement provenance: 21,148 exercises from NuminaMath-LEAN and 4,141 from Lean Workbook, both re-verified against the corpus toolchain; the rest are Prove2Me platform cards. Every task but six carries a natural-language statement. The images are the Prove2Me corpus images, hosted on the OpenReward platform.

Tools

• submit_proof(lean_code, informal_proof="") — the complete Lean file. Graded as described above; at most 3 calls.
• compile(lean_code) — compiles a draft with Lean and returns its messages without grading it: sorry is allowed, nothing is credited, no attempt is used, and the statement and axioms are not checked. At most 8 compiles per task (a draft identical to an earlier one returns the cached result without being counted); a draft rejected before compiling is not counted either.
• lookup(modules) — the source of any definition module of the corpus, or the statement of any lemma the task allows. Free and unlimited.

There is no shell, no file system and no network: the model writes the proof from what it knows, what the prompt and lookup give it, and what compile reports.

Time Horizon

Short. A rollout is one to three submit_proof calls, up to eight optional compile calls, a few optional lookup calls, and whatever reasoning the model does in between. Grading one submission took 53 to 90 seconds against a sandbox driven directly, and 160 to 166 seconds through the deployed environment (compile about 34 s, statement check about 32 s, kernel replay about 99 s). The sandbox starts in the background while the model is still reasoning, so the first submission does not pay the cold start.

Environment Difficulty

The grader accepts the known-good proofs. All 31,816 accepted proofs of both corpora were fed back through the exact submission path a model's answer takes: un-wrapped to a top-level file, composed, compiled, type-checked and axiom-checked.

By tier on p2m4331: easy 590/590, hard 2,684/2,742, exercise 20,836/21,148, medium 1,586/1,645. Every theorem that was not credited is excluded from the task set, so each shipped task has a proof this grader accepts. The failures were inspected and none is a grader disagreement with a valid proof: the largest class is 122 proofs whose declarations collide with the module that states the goal, and every one of those theorems was already excluded by the structural rules above, so that trap never reaches a model. A separate 1,200-theorem sample re-graded with kernel replay included scored 1,182.

Per-stage timings, on a 96-core build machine (the sandbox is slower, see Time Horizon):

The grader rejects cheating. A ladder of 28 attacks — sorry, citing the theorem being proved through its stub, weakening the statement, #exit, forging the check's own success marker (with the token handed to the attacker), hijacking the check command with macro_rules or a command macro, debug.skipKernelTC, native_decide, a private axiom, an unterminated comment, warningAsError, an empty file, a look-alike card axiom, importing the statement's own stub, importing a card outside the allowed set, and citing a card of equal height — scores 0 on every rung, while the two control rungs (a real reference proof, and one preceded by set_option warningAsError true) are credited. See build/results/cheats_p2m4331.txt.

Five of those rungs were replayed against the deployed environment through the session API (build/cheats_deployed.py, log in build/results/cheats_deployed.log) to confirm the shipped path enforces the same rules: sorry, importing the statement's own stub to cite it, a private axiom, native_decide and a trivial theorem named solution all score 0.

With compile in the loop. The same 28 rungs were re-run against real sandboxes through the environment class with the ungraded compile tool available (build/cheats_compile.py, log in build/results/cheats_compile.log). Each rung was sent to compile first and then to submit_proof, in sessions of up to three rungs, so later rungs meet whatever earlier compiles left in the sandbox. On every rung compile paid 0, ended nothing and used no attempt; submit_proof credited exactly the three controls, and every other rung scored 0 at the same stage as in the original ladder, except declares_card_name_and_solution, which now fails at compile time instead of being rejected upfront because the composer leaves name clashes to Lean.

The per-session design is what makes the marker rungs fail: the check command is compiled before any model code exists, is named with a random per-session token the model never sees, runs in a separate file that imports the model's module, and its markers are trusted only as a whole message of that file.

Live rollouts. gpt-5.6-sol through the deployed environment, one rollout per task, at most six turns each:

Seven of the nine were solved, four of them only after reading Lean's error and repairing the proof, which is the behaviour the three-attempt budget is there to train. Trajectories and logs are in build/results/live_*.json.

Other Environment Requirements

None. LeanProver needs no external API keys and no network access; everything it compiles against is inside the sandbox image.

Safety

The environment only compiles Lean code inside a sandbox with no network. The submitted code is elaborated by Lean, which can run arbitrary meta-programs, so the environment forbids command-level meta-programming, environment manipulation and @[init] code, and never lets model-supplied code influence the check: the checking elaborator is compiled first, invoked from a separate file, and its verdict is confirmed by an independent kernel replay. The accepted proofs are not present in any image, so a task cannot be solved by reading the answer.

Reward hacking is the natural risk of a proof-checking environment, and the cheat ladder above is the standing test that it does not pay.

Citations

@misc{chen2026prove2me,
  title  = {Prove2Me: A Platform for Collaborative Machine-Checked Mathematics},
  author = {Chen, Marwaha, Lu, Yuen, Peng},
  year   = {2026},
  eprint = {2608.28433},
  archivePrefix = {arXiv},
  url    = {https://prove2.me}
}

@misc{kimina_prover_2025,
  title  = {Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models},
  author = {Wang, Haiming and Unsal, Mert and Lin, Xiaohan and others},
  year   = {2025},
  eprint = {2504.11354},
  archivePrefix = {arXiv},
  note   = {NuminaMath-LEAN, https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN}
}

@misc{ying2024lean,
  title  = {Lean Workbook: A large-scale Lean problem set formalized from natural language math problems},
  author = {Ying, Huaiyuan and Wu, Zijian and Geng, Yihan and Wang, Jiayu and Lin, Dahua and Chen, Kai},
  year   = {2024},
  eprint = {2406.03847},
  archivePrefix = {arXiv}
}

@misc{mathlib2020,
  title  = {The Lean Mathematical Library},
  author = {{The mathlib Community}},
  year   = {2020},
  doi    = {10.1145/3372885.3373824}
}

@dataset{GRLeanProver,
  title     = {LeanProver},
  author    = {{General Reasoning}},
  year      = {2026},
  publisher = {OpenReward},
  url       = {https://openreward.ai/GeneralReasoning/LeanProver}
}