FermatProver

Description

FermatProver asks a model to prove one theorem from a machine-checked proof of Fermat's Last Theorem. The prompt gives the statement in Lean and in English, the context the project records for it, the source of the definitions it depends on and, for a theorem the project proved from earlier results, the statements of those results. The model reasons in natural language for as long as it wants, then submits a complete Lean file through a single tool. The environment compiles that file inside a sandbox that already holds Mathlib and the project's definitions, checks that some declaration of the file really has the statement's type, that the proof rests only on the standard axioms and the results 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 ground truth is anthropics/fermats-last-theorem (Apache-2.0), a proof of FLT organised as a directed graph of 29,511 theorem statements ("cards"), each proved in its own module from Mathlib, 1,450 definition modules and the cards it cites. The sibling environment FermatLean asks an agent to formalize a whole sub-graph of that proof from a shell; FermatProver keeps the same ground truth but removes the workspace, so a task is one card and the work is proof search and Lean fluency rather than project navigation. It shares FermatLean's sandbox image and uses the grading protocol of LeanProver.

Capabilities

• Proving research-level theorems in Lean 4 against a fixed Mathlib
• Working inside a large formalization's own definitions and previously proved results
• Translating a natural-language argument into a machine-checked proof
• 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 FermatLean's image (about 22 GB uncompressed), which already contains the Lean 4.33.1 toolchain, the Mathlib v4.33.1 olean cache, and every definition and statement module prebuilt. The environment server itself needs 1 CPU and 4 GB.

License

MIT for this environment's code. The formalization it is built on is Apache-2.0 (anthropics/fermats-last-theorem), as is Mathlib.

Tasks

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

The project routes its cards through numbered stages, and the test split is one whole stage held out, so the test set is a coherent area of the proof rather than lemmas scattered among their own neighbours. FermatLean's split cannot be mirrored: both of its splits contain sub-graph roots that reach every card, so no card is exclusive to either, and a model trained here will have seen cards that appear inside FermatLean's test tasks.

data/drop_cards.txt records every excluded card with its reason: a proof this environment's rules reject outright (69 above the submission cap, 4 using macro_rules, one statement that declares more than its own theorem), and 463 whose re-grade did not credit them. See Environment Difficulty for how much of the corpus that re-grade covered.

Median proof in the corpus is about 15 KB, and a hard task lists 4 usable results at the median and up to 106.

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 results 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. An attempt consumed by a submission the environment rejects before compiling still counts, but an infrastructure failure refunds it, and so does a kernel replay that runs out of time (15 minutes), since it reaches no verdict.

Data

data/statements.jsonl.gz holds one record per card — the Lean statement with its imports and context, the project's English statement and context, and the citation — and data/definitions.jsonl.gz the full source of all 1,450 definition modules. The proofs are not part of this repository and are in no image. data/tasks.json carries the tasks and splits, dag.json.gz the citation graph that decides which results a hard task may use, and drop_cards.txt the excluded cards with reasons.

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 project, or the statement of any result the task allows. Free and unlimited.

There is no shell, no file system and no network.

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. The sandbox starts in the background while the model is still reasoning, so the first submission does not pay the cold start.

Environment Difficulty

High, and higher than the sibling LeanProver: these are research-level lemmas from a current formalization effort, with a median reference proof of 15 KB.

The grader accepts the project's own proofs. Each proof is fed back through the exact submission path a model's answer takes: its wrapper namespace removed, its attribute-removal lines rewritten to the project's own tolerant form, then composed, compiled, type-checked, axiom-checked and kernel-replayed.

Two measurements. A re-grade of 6,057 cards — every easy card and 5,293 of the hard ones — credited 5,594 (92.4%): easy 761/764, hard 4,833/5,293. Every card it did not credit is excluded from the task set, so within that 6,057 the reward is always attainable. Re-grading the rest was not worth the machine time: the hard tier runs at about four cards a minute even on 64 cores, so the remaining 23,000 would have taken more than a day for an expected gain of a few percent. The medium and landmark tiers and 16,411 hard tasks therefore carry only the structural exclusions, and on this evidence about 8% of them have a reference proof this environment would not credit. That is unattainable reward on a minority of tasks, never a source of false credit, and build/verify_prover.py --resume continues the sweep where it stopped.

A separate stratified sample of 798 cards, re-graded with kernel replay included:

Per-stage timings on a 96-core build machine: compile p50 5.7 s / p90 21 s, statement and axiom check p50 4.4 s, kernel replay p50 14 s. The misses are proofs that reference the project's own wrapper namespace explicitly, and a handful whose instance context cannot be reconstructed from the statement stubs alone; every one of them is excluded from the task set.

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

Three of six were solved, against seven of nine on the sibling LeanProver whose tasks are largely competition exercises. Note that models spend many turns on lookup before submitting: a 6-turn budget left three of these rollouts without a single submission, so give a harness at least 15 turns.

The cheat rules hold on the deployment. Five rungs replayed through the session API — sorry, importing the statement's own stub to cite it, a private axiom, native_decide, and a trivial theorem named solution — all score 0 (build/results/cheats_deployed.log).

The grader rejects cheating. The cheat ladder of the sibling LeanProver applies unchanged, because the grading code is shared: 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.

The ladder holds with compile in the loop. LeanProver's 28 rungs were run against FermatProver on real sandboxes through the environment class (build/cheats_compile.py, log in build/results/cheats_compile.log), on AbsoluteValue_Completion_isUltrametricDist_of_isNonarchimedean and the hard card ModularCurve_deg_cuspInftyFull. Each rung was sent to the ungraded compile tool first and then to submit_proof, in sessions of up to three rungs. On every rung compile paid 0, ended nothing and used no attempt, and submit_proof credited exactly the three controls.

Contamination. The formalization is public on GitHub under Apache-2.0, so a model may have seen these proofs during pre-training. That is a real limit on FermatProver as an eval, and the reason the environment is most useful for training.

Other Environment Requirements

None. FermatProver needs no external API keys and no network access.

Safety

The environment only compiles Lean code inside a sandbox with no network. 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 project's proofs are not present in any image, so a task cannot be solved by reading the answer from the sandbox.

Citations

@misc{anthropic2026flt,
  title  = {A Machine-Checked Proof of Fermat's Last Theorem},
  author = {{Anthropic}},
  year   = {2026},
  note   = {https://github.com/anthropics/fermats-last-theorem, Apache-2.0}
}

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

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