Prove2Me

Description

Prove2Me is a long-horizon Lean 4 formalization environment built on the public library of Prove2Me, an open collaborative platform where humans and AI agents formalize papers, textbooks and open problems as "missions" of small Lean statements ("cards") whose proofs are checked by Lean's kernel (Chen et al., 2026). Every machine-checked, non-deprecated theorem of the platform outside the Fermat's Last Theorem mission (which has its own environment, FermatLean) is turned into a blueprint task: the agent gets the platform's definition modules and the statements of every card below a target theorem as axiom-backed stubs, and has to write the proofs. Its score is the fraction of those cards whose proof the grader accepts, so the environment measures how much of a verified formalization an agent can reproduce, from a single competition exercise up to a whole research-paper mission. To give the difficulty curve a well-populated easy end, the environment also contains competition problems with verified proofs from NuminaMath-LEAN (re-verified on this toolchain) and the Lean Workbook problems that were proved on the platform.

Capabilities

• Formal theorem proving in Lean 4 against Mathlib and project-specific definition modules
• Reading a blueprint of interdependent theorem statements, choosing which cards to attack and citing proved cards
• Decomposing research-level results into lemmas and tracking which statements are still open
• Long-horizon multi-turn execution in a sandboxed Lake project (build, iterate, check, submit)

Compute Requirements

Agents are given a sandbox with 4 CPUs and 16 GB of RAM. Grading runs in a second, pristine sandbox of the same size. Each corpus has its own sandbox image (14 GB and 16.6 GB uncompressed for the Lean 4.29 and 4.33 corpora) shipping the Lean toolchain, the Mathlib olean cache for the corpus's pinned revision and every definition and statement module prebuilt, so no Lean file outside the agent's own modules is compiled inside the sandbox. Importing all of Mathlib in the sandbox costs one to two minutes per module (the platform sandboxes run under gVisor with a fixed address-space limit of about 15 GB; the image wraps lean with a 256 MB thread stack so a full Mathlib import fits); the card preambles list the targeted imports that are much cheaper, and the grader caches the compile and kernel-replay results of modules whose sources have not changed between submits.

License

MIT. The theorem statements, definitions and natural-language summaries are redistributed from the Prove2Me platform, whose FAQ states that every public theorem, definition and proof is open for anyone to read, reuse and import; the NuminaMath-LEAN and Lean Workbook problems are Apache-2.0. Mathlib is Apache-2.0.

Tasks

A task is one card and its downward closure in the citation DAG of its corpus (the edges are the import Theorems.Thm_* lines of the accepted proofs, augmented with the cards that definition modules import). The agent sees exactly the statements in that closure. Task ids are <corpus>/<card module>.

There are two corpora, one per platform Lean environment (a third platform environment, Lean v4.30.0, is not included: 3,651 of its 3,861 theorems exist with identical statements in the default environment):

Every task carries a tier measured from the reference proofs, never guessed:

• exercise: a single competition problem (NuminaMath-LEAN or Lean Workbook), Mathlib-only statement, height 0.
• easy: a single platform card of height 0 whose accepted proof is at most 30 lines and whose statement imports at most two definition modules.
• medium: any other single card, or a sub-DAG of 2–20 cards.
• hard: a sub-DAG of 21–500 cards.
• mission: the goal theorem of a platform mission with its whole verified tree (from a few cards to several hundred).

There are 28,971 train tasks and 1,495 test tasks in total (30,466); about 82% of the train tasks are exercises, so curricula that want fewer of them should sample by tier. Mission tasks in p2m4331 range from 2 to 462 cards (63 multi-card missions; 18 of the corpus's 96 missions are test, with their whole trees).

The train/test split is by mission: about 20% of the missions (chosen by a hash of the mission id, so the same mission lands in the same split in both corpora) are test tasks together with every card in their trees, which never appear as train roots, and a 5% sample of the single cards of each tier is test; the remaining missions, single cards and stratified sub-DAG roots are train. Because sub-DAGs overlap, the split separates roots rather than knowledge. Cards present in both corpora are task roots only in p2m4331.

Reward Structure

This is a dense, verifiable reward environment with no LLM grader. A card is credited when all of the following hold for its module P2M/Sol/S_<M>.lean:

1. the module and every agent module it imports compile within the per-module time limit and contain no forbidden constructs (sorry, axiom, unsafe, native_decide, implemented_by, extern, set_option debug.*, or command-level meta-programming);
2. #p2m_card_type_eq accepts that P2MW.S_<M>.solution has the card's statement (definitionally equal, universes not specialised);
3. the axioms of the solution, collected transitively, are only propext, Classical.choice, Quot.sound and card axioms P2MCard.<M'> declared by the statement stub of a card M' in scope with strictly smaller height than M;
4. lake env leanchecker replays the agent's modules through the Lean kernel.

Completion is the number of credited cards divided by the number of gradable cards in the task. submit grades the agent's P2M/Sol/ tree in a pristine sandbox and returns the change in completion since the previous submit, so the total reward of a rollout equals the completion of its final submission, in $[0, 1]$; regressions cost reward. The height rule makes the credit well founded: citing a card of equal or greater height, a card outside the blueprint or the card being proved is rejected, so credit can only flow from lower cards to higher ones, exactly as in the platform's DAG.

Data

Statements, preambles, definition modules, natural-language statements, tags, sources, contributors, missions and human audit flags were harvested from the Prove2Me API on 2026-09-05 (all theorems with status Proved or Definition in each Lean environment, and the first accepted submission of each proved theorem as the reference proof). The statement stubs are the platform statements with the := by sorry hole replaced by a command that declares the card axiom with the theorem's exact type. Reference proofs are used only to build the citation DAG and to verify the grader; no proof text is present in the sandbox images, and the sandboxes have no network access.

The exercise tier of p2m4331 comes from AI-MO/NuminaMath-LEAN (Apache-2.0): its model-generated proofs were re-run under this environment's toolchain (Lean v4.33.1, Mathlib 0df444a, autoImplicit false) and only problems whose proof still compiles without sorry were kept (22,924 of 31,634 tried); 21,148 remain after dropping statements without the expected := by hole, proofs that use constructs the grader forbids (native_decide and friends) and three statements that only elaborate with autoImplicit. The Lean Workbook problems in p2m4290 were proved on the platform itself and are harvested like every other card.

Tools

Agents get the CLI toolset (bash, read, write, edit, multi_edit, glob, grep, ls, todo_write) rooted at the Lake workspace, plus three environment tools: check runs the grader on the agent's own tree and reports every card's verdict with categorical failure tags (free, unlimited), submit grades in a pristine sandbox and pays the telescoping reward (at most 10 graded submits per rollout), and progress shows the banked completion.

Time Horizon

Open-ended and long-horizon. A rollout is bounded only by the harness turn budget and the submit cap; single exercises take a handful of turns, the largest mission tasks contain several hundred cards.

Environment Difficulty

The accepted platform proofs are the yardstick. Dropping a reference proof in as the agent's solution and grading it with the environment's grader credits 382 of 410 sampled p2m4331 cards (300 random cards with an accepted proof, every card of the five smallest multi-card missions, and 100 NuminaMath exercises, measured on the 4,000-exercise build of the corpus) and 699 of 720 sampled p2m4290 cards (300 random cards plus every card of the five smallest multi-card missions, which include the 334-card matrix-multiplication mission mme_omega_lt). The misses are not grader rejections of valid proofs: they are references whose platform-convention source (top-level theorem solution in arbitrary namespaces) does not survive being re-namespaced for batch grading (19 in p2m4331, 18 in p2m4290), nine p2m4331 references that declare their solution inside a namespace block, two p2m4290 references that cite a card of equal or greater height, one that uses a construct the environment forbids, and one that imports a card outside its own closure (a deprecated platform theorem). Reference proofs compile in a median of 3.7 s (p90 9.2 s, maximum 126 s) on the build machine for p2m4290 and 3.8 s (p90 10 s, maximum 68 s) for p2m4331; peak memory stays under 8 GB, which fits the 16 GB sandbox.

The grader's cheat ladder (sorry, self-citation, a weakened statement, set_option debug.skipKernelTC, a private axiom, a macro-hidden axiom, native_decide, misuse of the stub-building tactic, citing a higher card, importing an out-of-scope card) scores 0 on every rung in both corpora.

The pushed images were checked on the platform sandboxes themselves: verify_local.py (driving the environment class directly) and verify_deployed.py (through the deployed environment) write the three reference proofs of p2m4290/Cardinality_of_Set_of_Subsets and score 1.0 with the episode finishing (cold sandbox start 141 s, advisory check 106 s to 3.7 min, pristine-sandbox grade 4.0 to 5.2 min); deleting one proof and resubmitting pays 2/3, restoring it pays the remaining 1/3.

Live rollouts (OpenAI Responses API through test_agent.py, gpt-5.6-sol, a reminder to submit when 10 turns remain; trajectories in build/results/):

The exercise and easy tiers are within reach of current frontier models in a handful of turns, and a small textbook mission took a 44-turn rollout; the medium, hard and larger mission tiers (up to 462 cards of research-level mathematics) remain open-ended. Per-tier solve rates over larger samples are left to users of the environment. Two earlier attempts at the mission task on a memory-starved laptop were killed by the harness mid-rollout (the partial log is kept in build/results/); the reported run was driven from the build machine.

A rollout that never submits earns nothing, so harnesses should remind the model to submit before its turn budget ends.

Other Environment Requirements

Prove2Me needs no external API keys; the sandbox images contain everything.

Safety

The agent works inside an offline Lake project and can only write Lean code and run its own build. Grading is deterministic and never trusts the agent's sandbox. The environment presents no direct safety risk; the only sensitive material is the reference proof text, which is kept out of the sandbox images.

Citations

@misc{chen2026prove2me,
  title         = {Prove2Me: An Open Collaborative Platform for Scaling Math Formalization},
  author        = {Shuze Chen and Kunal Marwaha and Xiaoyang Lu and Henry Yuen and Tianyi Peng},
  year          = {2026},
  eprint        = {2608.28433},
  archivePrefix = {arXiv},
  url           = {https://prove2.me}
}

@article{kimina_prover_2025,
  title  = {Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning},
  author = {Wang, Haiming and others},
  year   = {2025},
  url    = {http://arxiv.org/abs/2504.11354},
  note   = {NuminaMath-LEAN dataset, \url{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        = {Huaiyuan Ying and Zijian Wu and Yihan Geng and Jiayu Wang and Dahua Lin and Kai Chen},
  year          = {2024},
  eprint        = {2406.03847},
  archivePrefix = {arXiv}
}

@dataset{GRProve2Me,
  author    = {General Reasoning Inc. Team},
  title     = {Prove2Me},
  year      = {2026},
  publisher = {OpenReward},
  url       = {https://openreward.ai/GeneralReasoning/Prove2Me}
}