Hugging Face FineEnvs turns OpenAI math proofs into 369 Harbor RL environments

What did FineEnvs publish from OpenAI’s math release?

On 6 October 2026 OpenAI published a large formal-math drop that we covered as OpenAI’s 722 AI math manuscripts with Lean artifacts: manuscripts plus Lean proof artifacts. FineEnvs’ follow-up is not another paper. It is a runnable dataset: the math problems become Harbor reinforcement-learning environments that an agent can attempt and that a separate checker can score without a human grader.

The Hub page FineEnvs/openai-math describes the port from OpenAI’s openai/math repository at commit adc7f12. OpenAI formalized 405 results as Lean statements. FineEnvs generated a Harbor task for each statement except one left out by design, then ran Harbor’s oracle—which submits OpenAI’s own proof—through the same verifier an agent would face. Only the 369 tasks whose official proofs were accepted are included.

Clement Delangue’s 11 October 2026 post framed the release as turning a research drop into “executable training infrastructure for everyone,” while warning that the verifier only accepts the exact original formalization. Hugging Face’s Hub API shows the dataset created on 8 October and last modified on 9 October 2026; Delangue’s post is what put the packaging in the wider AI-news stream this week. We treat 11 October as the public spotlight date and the Hub card as the technical primary.

How does a Harbor math task actually work?

Inside a task the agent receives a sandbox with Lean 4 and a prebuilt Mathlib, no internet, and one of OpenAI’s theorems written with `sorry` where the proof should be. In Lean, `sorry` is a compile-time placeholder that pretends a step is proven; the agent’s job is to replace every `sorry` with a real proof of the statement exactly as OpenAI formalized it.

When the agent finishes, a separate fresh sandbox grades the submission with Comparator, the Lean FRO’s proof checker. Reward is 1 only if three conditions hold: the theorem statement is exactly the original, the proof uses only Lean’s standard axioms (`propext`, `Quot.sound`, `Classical.choice`—so no leftover `sorry` and no new axioms), and the Lean kernel accepts it. Otherwise the reward is 0.

OpenAI’s own proofs are the reference solutions. Harbor’s oracle fetches them from GitHub at run time; they are not shipped inside the dataset, and the agent never sees them. That keeps the training set from trivially containing the answers while still letting maintainers verify that the environment can accept a known-good proof.

Why is the reward so strict, and what does that cost?

The dataset card is unusually blunt about the training-signal trade-off. A correct proof of an equivalent statement that uses different definitions scores 0. Useful lemmas, a proof of a special case, or a strategy with one gap also score 0. Nothing rewards creative reformulation unless it ends in a complete proof of this exact statement.

FineEnvs says that for open research problems a more general reward—one that recognizes any valid solution to the underlying problem, including partial progress—would be a better training signal. They kept the strict check because it is precise and hard to game. They also report testing cheating attempts (`sorry` disguises, fake axioms, `native_decide`, weakened statements, redefined definitions, planted reward files, code that runs during grading, disk-filling builds). All scored 0. A no-op agent scores 0.

Eight of openai/math’s Comparator configs had listed some inlined definitions as unchecked “holes,” which would have let a solution redefine them. FineEnvs requires those definitions to match exactly and lists them under `fixed_definitions` in `task.toml`. Contamination is acknowledged up front: statements and proofs have been public since 6 October 2026. Difficulty is also acknowledged: these are open research problems; expect reward 0 on almost every task.

What made it into the dataset, and what was left out?

The card’s validation table is the most concrete quality statement in the release. Of the statements FineEnvs tried to turn into tasks, 369 were accepted end to end. Twenty-one failed because OpenAI’s proof needs a Lean library beyond Mathlib that the sandbox does not include. Ten needed more than the sandbox’s 8 GB of memory to build. Two hit definition-mismatch failures where OpenAI’s proof text compiles differently under exact-match checking. Two grading runs did not complete. One statement (`DefocusingNLS`) was left out by design because a definition the theorems depend on still contains `sorry`.

Median time to grade an accepted proof was about eight minutes in FineEnvs’ run. Each task records its oracle result in `task.toml` and in `manifest.parquet`. The dataset also ships `tasks/`, a Harbor registry entry (`openai-math@1.0`), a generator that rebuilds sandbox images from openai/math, and licensing files that separate OpenAI’s Lean statements from FineEnvs’ packaging.

How do you run it, and what does it cost to try?

The documented install path is straightforward on paper and heavy in practice. You need Harbor 0.24 or newer with the Daytona backend (`DAYTONA_API_KEY`, `DAYTONA_API_URL`) plus credentials for whatever agent you want to run. After `hf download FineEnvs/openai-math`, you build a shared sandbox snapshot once—Lean 4, Mathlib, Comparator—about 9 GB and roughly an hour, then point `harbor run` at individual tasks under `tasks/`.

Each task asks for 4 CPUs, 8 GB of memory, 10 GB of disk, and gives the agent four hours. That is closer to a research cluster budget than a laptop afternoon. The card also documents an oracle mode that fetches OpenAI’s proof from GitHub to confirm the grader accepts a known solution—useful as a smoke test before you burn agent hours on reward-zero research problems.

If you already follow agent-evaluation harnesses such as Kiln’s Seahaven synthetic agent worlds, Reason Agent 1.1’s coding-agent index results, or Microsoft’s ThinkingBox stateful agent benchmark, treat openai-math as a different slice of the same trend: graded environments instead of static question banks. The difference is domain difficulty. Coding-agent benches often have dense partial credit; this math set is deliberately almost all-or-nothing.

Why does packaging proofs as RL environments matter?

Static proof corpora are easy to download and hard to train against. Without a verifier that can score an attempt automatically, reinforcement learning and agent loops stall on human review. Packaging openai/math as Harbor tasks is a concrete answer: same statements, same kernel, machine-checkable reward.

The limit is the reward shape. Exact-match Comparator scoring protects against reward hacking and weakens credit for genuine mathematical progress that does not match OpenAI’s formalization. Labs that care about open-ended theorem proving will likely want a second grader—or a curriculum of easier lemmas—before this set becomes a productive RL target rather than a stress test.

Licensing is clearer than many model cards. OpenAI’s Lean statements remain Apache-2.0 and are copied unchanged; OpenAI’s proofs are not redistributed; FineEnvs’ packaging, verifier and generator are Apache-2.0; the sandbox stacks Lean 4, Mathlib, Comparator and lean4export (Apache-2.0) plus landrun (MIT). The card asks users who publish results to cite the openai/math manuscripts as that repository requests.

We inspected the Hub dataset card and README on 12 October 2026, checked the Hub API timestamps, and cross-read OpenAI’s openai/math repository page. We did not build the 9 GB snapshot, run Harbor, or attempt any proof. Until independent groups publish agent scores on the held-out task names, treat “executable infrastructure” as an accurate packaging claim and “better open models” as an aspiration still waiting for public training curves.