FermatLean

Description

FermatLean is a long-horizon Lean 4 formalization environment built on Anthropic's machine-checked proof of Fermat's Last Theorem (anthropics/fermats-last-theorem, Lean 4.33.1, Mathlib v4.33). That proof was produced by the Prove2Me pipeline as a directed acyclic graph of 29,511 theorem statements ("cards"), each proved in its own module from Mathlib, 1,450 definition modules and the cards it cites. FermatLean turns that DAG into a blueprint task: the agent is given the definitions 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 the reference formalization an agent can reproduce, from a single lemma up to the whole of Fermat's Last Theorem.

Capabilities

• Formal theorem proving in Lean 4 against Mathlib and a large project-specific library of definitions
• Reading and navigating a blueprint of thousands of interdependent theorem statements
• Decomposing deep results into cited 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. The sandbox image (about 22 GB uncompressed) ships the Lean 4.33.1 toolchain, the Mathlib v4.33.1 olean cache and every definition and statement module prebuilt, so no Lean file outside the agent's own modules is ever compiled inside the sandbox. Importing 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), and the grader caches the compile and kernel-replay results of modules whose sources have not changed between submits.

License

MIT. The reference formalization, whose statements and definitions are redistributed here, is released by Anthropic under the Apache License 2.0 with material from the Imperial College London FLT project, flt-regular and Mathlib (see its ATTRIBUTION.md).

Tasks

A task is one card and its downward closure in the citation DAG (augmented with the edges from definition modules to the cards they import). The agent sees exactly the statements in that closure.

• train (1,027 tasks): 1,000 roots sampled from the DAG, stratified by closure size (150 single-card tasks, 150 of 2–5 cards, 200 of 6–20, 200 of 21–100, 150 of 101–500, 100 of 501–3,000 and 50 larger), 26 of the landmark theorems named in the reference's PROOF-PATH.md, and the full theorem fermat_last_theorem (all 29,511 cards).
• test (28 tasks): the other 27 landmark theorems and the full theorem.

The landmark theorems are the named steps of the proof route (the Frey package, irreducibility of the Frey representation, Kummer's theorem for regular primes, Langlands–Tunnell, the modularity lifting theorems, level lowering, the vanishing of weight-2 cusp forms of level 2, ...). They range from one card to 29,511 cards and are split between train and test alternately by size. Because sub-DAGs overlap heavily, the split separates roots rather than knowledge.

One of the 29,511 cards (LanglandsTunnell.RankinSelberg.integral_matrixTwo_eq_setIntegral_iwasawaInv_unconditional) has a statement that only elaborates together with its own proof module; that card is shipped proved (P2M/Given/), is marked "given" in the blueprint and is never graded. Every other card is a gradable statement stub.

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 meta-programming);
2. the reference project's own #p2m_type_eq command 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 reference DAG.

Data

The statements, definitions and English summaries come from the reference repository (its Theorems/, Definitions/ and html/ data). The statement stubs are the reference statement files with the proof import removed and the proof term replaced by a command that declares the card axiom with the theorem's exact type. No proof text from the reference is present in the sandbox image, apart from the given cards described above, and the sandbox has no network access.

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 (unlimited; a check that credits a card the last submit did not also runs a submit and pays its reward), submit grades in a pristine sandbox and pays the telescoping reward (at most 10 graded submits per rollout, automatic ones included), 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; the full-theorem task contains 29,511 cards.

Environment Difficulty

The reference proofs are the yardstick. On a sample of 666 cards (the complete closures of the small landmark tasks — FreyPackage.frey_no_cofixed_small, WeierstrassCurve.modThreeOrFiveIrreducible, FreyPackage.frey_reducible_hasCofixedLine, FreyPackage.Mazur_Frey_of_a_mod_eight, WeierstrassCurve.threeFiveSwitchCurve, WeierstrassCurve.fifteenIsogenyClassification, GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum and the single-card landmarks — plus 400 random cards), dropping the reference proof module in as the agent's solution is credited for 665 of 666 cards; the one exception uses a helper lemma that lives inside another card's proof module, which the blueprint does not expose. 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.

Reference proof compile cost on the build machine (per module, lake env lean with the project's options):

No sampled module needed more than 16 GB or more than 15 minutes on that machine; the sandbox (4 CPUs, 16 GB, 25-minute per-module compile budget) is several times slower per module, mostly in the Mathlib import. On the deployed environment, writing the seven reference proofs of the landmark task FreyPackage.frey_no_cofixed_small through the CLI tools and submitting scores 1.0 and finishes the episode (the advisory check took 6.4 minutes and the pristine-sandbox grade 6.3 minutes); deleting one proof and resubmitting pays 6/7, restoring it pays the remaining 1/7 (verify_deployed.py). Cards get harder with height: the 7,691 height-0 cards need Mathlib and the Definitions only, while the target fermat_last_theorem sits at height 117 above 29,510 other cards.

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

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

Other Environment Requirements

FermatLean needs no external API keys; the sandbox image contains 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 image.

Citations

@misc{anthropic2026flt,
  author    = {Anthropic},
  title     = {Fermat's Last Theorem in Lean 4},
  year      = {2026},
  howpublished = {\url{https://github.com/anthropics/fermats-last-theorem}},
  note      = {Research artifact; see also \url{https://www.anthropic.com/research/formalizing-fermats-last-theorem}}
}

@misc{ImperialFLT,
  author    = {Kevin Buzzard and others},
  title     = {Fermat's Last Theorem (Imperial College London formalization project)},
  howpublished = {\url{https://github.com/ImperialCollegeLondon/FLT}}
}

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