FluidLean

Description

FluidLean is an environment for formalizing OpenAI's machine-checked proofs of finite-time blowup for the three-dimensional incompressible Navier–Stokes and Euler equations in Lean 4. The ground truth is the Lean certificate repository openai/NavierStokesAndEuler (Apache-2.0; commit f9e8bc5b, Lean 4.34.0-rc2, Mathlib tag v4.34.0-rc2) accompanying the papers "Finite time blowup for Navier–Stokes" and "Finite time blowup for the Euler equation". The corpus has two libraries, Euler (1,839 modules) and NavierStokes (816 modules), containing 38,531 theorem/lemma declarations ("cards").

The agent works in a prebuilt Lake workspace holding the whole project with every card's proof replaced by an axiom-backed placeholder (:= by nse_card_axiom NSECard.<uid>) and every definition kept verbatim. A task is a set of modules, from one module to a whole library; the agent replaces the placeholders of those modules with proofs in place, using the Lean toolchain, the papers' text, module docstrings and backdated web search (arXiv, news, web as of 2026-09-07). Its score is the fraction of the in-scope cards whose proof is accepted.

FluidLean is the formalize-many sibling of FluidProver (prove one card, no filesystem) and follows the design of FermatLean for Fermat's Last Theorem. Because theorems of this corpus are stated inside ordinary modules (with same-module and private definitions, local notation and section variables), the protocol splices proofs into the original module text rather than restating theorems in separate modules, and statement identity is checked with a per-card type fingerprint.

Capabilities

• Reading a research-level formalization (the blowup constructions, packet estimates, Gevrey and Sobolev bounds) and its papers
• Proving analysis lemmas in Lean 4 against Mathlib, from short leaf facts to the papers' main theorems
• Working inside a large Lake project: compiling single files, reading definitions and statements of imported modules, grepping Mathlib
• Iterating with a grader in the agent's sandbox (check) and banking progress with a telescoping submit (a check that credits new cards submits automatically)
• Backdated literature search on arXiv and the web
• Long-horizon multi-turn execution

Compute Requirements

Agents are given a sandbox with 4 CPUs and 16 GB of RAM running the FluidLean image (Lean 4.34.0-rc2 toolchain, prebuilt Mathlib, the stub workspace, the pristine stub sources and the papers' text; 16.5 GB on disk). Grading runs in a second, pristine sandbox of the same size. Importing Mathlib in the sandbox costs 40–240 seconds per file; on the 96-core build VM the fully proved reference text of a module compiled in a median 5 s (90th percentile 13 s, maximum 386 s for Euler.EulerProof with 997 cards), the check file in a median 3 s and the kernel replay in a median 6 s; a live platform check of a 4-card module task took 24 s of sandbox start, 97 s for check and 2.0 minutes for submit including the second sandbox's start.

License

MIT. The corpus is Apache-2.0 (OpenAI); Mathlib is Apache-2.0.

Tasks

Tasks are scopes of modules; every task lists its modules and cards in SCOPE.md inside the workspace.

Module tasks (2,613 of the 2,655 modules; the rest contain only definitions) cover every module with at least one gradable card, tiered by the number of cards (m1, m2_5, m6_20, m21_100, m100p). Closure tasks cover the import closure of the modules stating the papers' results (Euler.Solution, Euler.EulerSingularity, NavierStokes.ComparatorSolution, NavierStokes.PaperResults). The euler_full and navierstokes_full tasks cover a whole library and are aspirational; their _train twins have the same scope.

The split holds out about 10% of module families (a module and its *NoOptions variant form one family) with a fixed hash; module tasks and the cards of FluidProver inherit it, so a FluidProver test card never appears inside a FluidLean train module task. Statements of test modules remain visible everywhere as imports (statements only); the closure and full tasks in the test split contain train modules, as FermatLean's full task did. Cards whose original proof could not be re-credited by the grader, duplicate cards in the *NoOptions variants, and cards whose stub module compiles too slowly for the sandbox are excluded from grading (see Data).

Reward Structure

submit grades the in-scope modules in a pristine sandbox and pays the change in completion since the previous submit, where completion = credited cards / cards in scope; the total reward of a rollout equals the completion of its final submission, in [0, 1]. Regressions pay negative reward; at most 10 graded submits; the episode ends when every card is credited, when the submit cap is reached, or when the agent calls finish (reward 0; the banked completion stands). check runs the same grader in the agent's sandbox; it pays nothing itself, but a check that credits a card the last submit did not also runs a submit (never the last one before the cap) and pays that submit's reward, so progress is banked even if the agent never calls submit.

A card is credited only if: (1) its file passes hygiene (no sorry, axiom, unsafe, native_decide, implemented_by/extern, set_option, command-level meta-programming, #exit, #print; the placeholder tactic only in untouched placeholders), keeps the module's original imports (Mathlib-family imports and modules already in its import closure may be added), and compiles; a declaration whose proof fails is put back to its placeholder before grading so one broken proof does not sink a file; (2) the theorem exists with the elaborated type recorded at build time (a structural fingerprint of the type after normalising private names, so helper lemmas above the card are fine but shadowing a name or adding an instance that changes the statement is not), and every pre-existing non-card constant of the file (definitions, abbrevs, instances, structures; read from the pristine stub's .olean) keeps its kind, type and, for definitions, value, so the names a statement mentions keep their meaning (otherwise no card of the file is credited); (3) its axioms are only propext, Classical.choice, Quot.sound and card axioms NSECard.<uid> of theorems visible from that point of the original project: theorems of imported modules (the axiom must be declared by that module and carry the recorded fingerprint) and earlier theorems of the same file (later cards, the card itself and forged look-alikes are rejected); (4) leanchecker replays the file through Lean's kernel. There are no LLM graders.

Data

Every module of the corpus is shipped as a stub (proof bodies replaced by placeholders); the original proofs are in no image and never leave the build machine. The data files (data/cards.json.gz, data/modules.json.gz, data/tasks.json, data/split.json, data/drop_cards.txt) hold the card table (names, signatures, docstrings, context, fingerprints, citation heights), the stub sources and import closures, and the tasks; they are hosted on the OpenReward platform. The papers are shipped as plain text extracted from OpenAI's PDFs.

Exclusions: none. Every one of the 38,531 original proofs was re-credited by the grader (three of them only with the doubled heartbeat budget the grader uses, maxHeartbeats 400000), so the drop list is empty and there are no given cards. The Euler.EulerProof module task (997 cards; its fully proved text takes 386 s to compile on the build VM) is train-only.

Tools

Environment tools: check(modules=None), submit(), finish(), progress(). Backdated web tools: web_search, web_fetch (as of 2026-09-07, the eve of the announcement of the papers and the Lean repository: none of the coverage or the Lean sources are visible, the earlier blowup literature is). CLI tools: bash, read, write, edit, multi_edit, glob, grep, ls, todo_write. The sandbox itself has no network.

Time Horizon

Long-horizon: a module task takes tens to hundreds of tool calls (each compile of a file that imports Mathlib costs minutes), the closure and full tasks are open-ended. Tool-call statistics for models have not been measured yet.

Environment Difficulty

Verification so far is grader-side: the reference re-grade credited 38,531/38,531 cards over all 2,613 module tasks; the cheat ladder (build/results/cheat_ladder.txt) scores 0 on every rung except the gold and harmless controls; live platform checks reproduce the reward mechanics: on the deployed environment (verify_deployed.py, build/results/verify_deployed.log) the 4-card module task Euler.ClassicalBridge gave check 4/4 in 119 s, submit reward 1.0 in 2.1 minutes (pristine sandbox start included), a second session paid 0.75 with one card back at its placeholder, 0 for an edit of an out-of-scope module, and 0.25 after restoring the proof. One gpt-5.2 rollout on the 3-card module task Euler.CompactSmoothBounds (30 turns, 12 minutes) read SCOPE.md and the stubs, grepped Mathlib, wrote proofs for all three cards, ran check twice (0/3 credited, 63 s each) and submit once (0/3, 94 s), and ended at reward 0 (build/results/smoke_gpt-5.2_Euler.CompactSmoothBounds.log); success rates have not been measured beyond that. The card heights (0 = the original proof cites no other card of the project) range from 0 to 90; 8,408 cards have height 0 and 11,736 have height 10 or more, and the original proofs are 5 lines long at the median (90th percentile 17, maximum 149).

Contamination: the corpus and its proofs have been public on GitHub since 2026-09-08, so models trained on data after that date may have seen them; the backdated search cutoff removes the in-episode leak, not the pretraining one.

Other Environment Requirements

None beyond the OpenReward platform.

Safety

Agents prove mathematical statements in a sandbox without network access. The environment presents no direct safety risk. The grader is adversarially hardened (hygiene rules, statement fingerprints, axiom whitelist, pristine grading sandbox, kernel replay); a cheat ladder of 28 rungs scores 0 on every rung but the controls.

Citations

@misc{openai2026navierstokes,
  author = {OpenAI},
  title  = {Finite time blowup for Navier--Stokes},
  year   = {2026},
  url    = {https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf}
}
@misc{openai2026euler,
  author = {OpenAI},
  title  = {Finite time blowup for the Euler equation},
  year   = {2026},
  url    = {https://cdn.openai.com/pdf/315b36cd-ec98-4023-8342-93345194ece1/euler.pdf}
}
@misc{openai2026nselean,
  author = {OpenAI},
  title  = {NavierStokesAndEuler: Lean certificates accompanying Navier-Stokes and Euler results},
  year   = {2026},
  url    = {https://github.com/openai/NavierStokesAndEuler}
}
@inproceedings{mathlib2020,
  author    = {The mathlib Community},
  title     = {The Lean Mathematical Library},
  booktitle = {CPP 2020},
  year      = {2020},
  doi       = {10.1145/3372885.3373824}
}
@dataset{GRFluidLean,
  author    = {General Reasoning Inc. Team},
  title     = {FluidLean},
  year      = {2026},
  publisher = {OpenReward},
  url       = {https://openreward.ai/GeneralReasoning/FluidLean}
}