FluidProver

Description

FluidProver is an environment for proving one theorem of OpenAI's machine-checked Lean 4 proofs of finite-time blowup for the three-dimensional incompressible Navier–Stokes and Euler equations. 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": 38,531 theorem/lemma declarations ("cards") in 2,655 modules of the Euler and NavierStokes libraries.

A task is one card. The prompt shows the theorem exactly as it stands in its module, the commands in effect at that point (namespaces, opens, variables, local notation), the earlier declarations of the module with proofs elided, the module's imports and docstring, and for the harder tiers the statements of the cards the original proof cited. The model reasons in natural language, may look up any visible declaration or module and search the pre-announcement web, then calls submit_proof with the theorem restated verbatim and proved (helper lemmas above it are allowed). The environment splices that code into the stub module at the card's position, compiles it in a Lean sandbox, checks the theorem's type fingerprint and axioms with a per-session command, and replays the module through leanchecker. Reward 1.0 when credited, up to 3 attempts with compiler feedback.

FluidProver is the prove-one sibling of FluidLean (formalize whole modules from a shell) and follows the design of FermatProver for Fermat's Last Theorem; it shares FluidLean's sandbox image and grader.

Capabilities

• Formal proof search in Lean 4 over Mathlib for research-level analysis (packet constructions, Gevrey and Sobolev estimates, transport and heat equations, the blowup arguments themselves)
• Reading a large formalization through its statements, docstrings and definitions rather than its proofs
• Natural-language mathematical reasoning before committing to a formal proof
• Repairing a proof from compiler feedback (3 attempts)
• Backdated literature search on arXiv and the web

Compute Requirements

Each task runs one sandbox with 4 CPUs and 16 GB of RAM (the FluidLean image, 16.5 GB on disk), started in the background while the model reads the prompt. A graded submission compiles the module prefix plus the proof, then the check file and the kernel replay; in a live platform check of an easy card the sandbox started in 43 s, a wrong proof came back in 43 s and the reference proof was credited in 79 s (compile 11 s, check 10 s, kernel replay 56 s). The stub prefixes compile in at most 29 s on the build VM (median 3 s), so no card is excluded for size.

License

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

Tasks

One task per card, excluding given cards (statements the placeholder tactic cannot stub), duplicate cards in the *NoOptions module variants, cards of modules whose stub compiles too slowly for the sandbox, and cards whose original proof the grader could not re-credit.

Tiers: landmark = cards of the four modules that state the papers' results (Euler.Solution, Euler.EulerSingularity, NavierStokes.ComparatorSolution, NavierStokes.PaperResults); easy = original proof of at most 12 lines citing at most 2 other cards; medium = at most 25 lines citing at most 8 cards; hard = the rest. The split holds out about 10% of module families (a module and its *NoOptions variant) with a fixed hash, shared with FluidLean; test cards remain visible everywhere as statements.

Reward Structure

Reward 1.0 when the proof is credited, 0 otherwise; the task ends on a credited proof or after 3 attempts. A submission is rejected before compilation (consuming an attempt) if it is too large, trips a hygiene rule (sorry, axiom, unsafe, native_decide, implemented_by/extern, set_option, command-level meta-programming, #exit, #print, the placeholder tactic), imports a module outside the module's import closure, or does not restate the theorem with a whitespace-equivalent signature. It is credited only if the spliced module compiles, the theorem has the elaborated type recorded at build time (a structural fingerprint, so a preamble that shadows a name or adds an instance fails), its axioms are only propext, Classical.choice, Quot.sound and card axioms of theorems visible from that point (imported modules and earlier theorems of the same module, each with its recorded fingerprint and declaring module), and leanchecker accepts the module. Infrastructure failures refund the attempt; identical resubmissions return the cached verdict. There are no LLM graders.

Data

data/cards.json.gz (the card table: names, signatures, docstrings, context commands, fingerprints, citations and heights), data/modules.json.gz (imports, import closures, docstrings and the stub source of every module) and data/tasks.json are hosted on the OpenReward platform; the original proofs are in no data file and no image. The papers are OpenAI's PDFs linked from the repository.

Tools

submit_proof(lean_code, informal_proof=""), compile(lean_code) (splices and compiles a draft and returns Lean's messages without grading it: sorry allowed, never credited, no attempt used, statement and axioms not checked; at most 8 per task, identical drafts and drafts rejected before compiling are not counted), lookup(names=[], modules=[]) (free; declarations visible from the card, module statements with proofs elided, "*" lists the visible modules), and the backdated web tools web_search / web_fetch (as of 2026-09-07, the eve of the announcement of the papers and the Lean repository). The Lean sandbox has no network.

Time Horizon

Short-horizon: a few lookup and web_search calls, up to 8 compile calls, then up to 3 submit_proof calls; each graded submission takes several minutes of sandbox time. Give at least 15 turns: models spend many turns reading before submitting.

Environment Difficulty

Every task has a proof the grader accepts: the whole-corpus reference re-grade credited 38,531/38,531 cards (three only with the doubled heartbeat budget the grader uses, maxHeartbeats 400000), the drop list is empty and there are no given cards. The cheat ladder (../fluidlean/build/results/cheat_ladder.txt, 28 rungs) scores 0 on every rung except the controls. On the deployed environment, verify_deployed.py reproduced the gold path (a wrong proof returns the mapped Lean error in 154 s including the sandbox start, the reference proof is credited in 94 s: compile 13 s, check 12 s, kernel replay 66 s) and build/cheats_deployed.py scored 0 on all 7 cheat rungs with the gold control credited (build/results/cheats_deployed.log). The 19 single-card rungs of that ladder (S01–S19) were also re-run on real sandboxes through the environment class with the ungraded compile tool available, on Euler.LpBochnerRealization.c4 (build/cheats_compile.py, log in build/results/cheats_compile.log): each rung went to compile first and then to submit_proof, and on every rung compile paid 0, ended nothing and used no attempt, while submit_proof credited only the controls and S09 (a rung whose outcome the ladder leaves open, credited as in the original run). S16, citing a later card of the module, was skipped in the original run and is refused here. One gpt-5.2 rollout on the easy card Euler.BaseWordMetric.c1 used two lookup calls and three submit_proof attempts, all failing to compile (reward 0 after 199 s; build/results/smoke_gpt-5.2_Euler.BaseWordMetric.c1.log), so even the easy tier is not trivial for a general model. Success rates by tier have not been measured beyond that. Original proofs are 5 lines long at the median (90th percentile 17, maximum 149); heights range from 0 to 90.

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, per-session check command, 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{GRFluidProver,
  author    = {General Reasoning Inc. Team},
  title     = {FluidProver},
  year      = {2026},
  publisher = {OpenReward},
  url       = {https://openreward.ai/GeneralReasoning/FluidProver}
}