OpenAI Math Becomes RL Environments: 369 Lean Proof Tasks on Hugging Face

Short answer: a Hugging Face dataset now turns the formalized results from OpenAI's new math release into 369 reinforcement learning environments that anyone can run. Hugging Face CEO Clement Delangue announced it on X on October 11, 2026 ("We turned @OpenAI's math problems into open-source RL environments on @huggingface"). The dataset page, FineEnvs/openai-math, describes each task as a Lean 4 theorem the agent must prove, graded by a separate proof checker.

The catch is stated plainly on the dataset card: "These are open research problems; expect reward 0 on almost every task." This is training infrastructure, not a leaderboard you can climb this week. Below is what it is, how the grading works, and what it means for open models. For the release it builds on, see our coverage of OpenAI's 722 math manuscripts.

TL;DR: what the dataset is

Two attribution notes. The Delangue post is a primary source as the Hugging Face CEO's own announcement, but I could only read its text through a feed summary. The dataset itself is hosted under the FineEnvs namespace, so confirm its relationship to Hugging Face on the Hub if that matters for your use.

What are RL environments, and why math?

An RL environment is a task a model can attempt, a way to run its actions, and a reward that scores the attempt. We explained the pattern in our guide to Hugging Face's push to host RL environments on the Hub. Math with a proof checker is attractive because the reward can be computed by machine with no human grader and no model judge.

This dataset uses Harbor, a framework for packaging agent tasks as folders containing an instruction, a sandbox recipe, a verifier and a reference solution. Each of the 369 tasks has that shape. The agent receives one of OpenAI's theorems written in Lean with sorry where the proof should be. In Lean, sorry is a placeholder that lets a file compile as if a step were proven; the agent has to replace every one.

How the grading works

According to the dataset card, when the agent finishes, its Submission files are copied to a fresh machine and checked with Comparator. Reward is 1 only if three things hold:

1. The theorem has exactly the original statement.
2. The proof uses only Lean's standard axioms: propext, Quot.sound and Classical.choice. Leftover sorry, new axioms and native_decide are rejected.
3. The Lean kernel accepts the proof.

Otherwise the reward is 0. OpenAI's own proofs act as reference solutions, which Harbor's oracle fetches from GitHub at run time; the agent never sees them. The card also says the verifier was tested against cheating attempts such as disguised sorry, fake axioms, weakened statements, redefined definitions, planted reward files and code that runs during grading, and all scored 0.

I looked at two task pages. abhyankar-sathaye is tagged difficulty research, has a reference proof of 15 modules, and its oracle grading took 47 seconds. affine-bernstein has a reference of 322 modules and about 2 MB of Lean source, and grading took 1,429 seconds. That spread shows how uneven these tasks are, and why a median grading time of 8 minutes, as the card reports, hides a long tail.

The reward is strict, and the authors say so

The most useful part of the card is its own critique of its reward:

• A correct proof of an equivalent statement with different definitions scores 0.
• Partial progress, such as useful lemmas or a special case, scores 0.
• Nothing rewards a creative approach unless it ends in a complete proof of the exact statement.

The authors write that for open research problems "a more general reward function that recognizes any valid solution to the underlying problem" would be a better training signal, and that they use the strict check because it is precise and cannot be fooled. In RL terms, this is a sparse, binary, hard-to-hack reward on tasks where a current model almost never succeeds.

Green ball slipping through a shortcut under an arch, a picture of reward hacking that a strict proof checker is built to block

That has a practical consequence. With success rates near zero, there is little gradient to learn from unless you pair these environments with easier tasks, curriculum, or supervised proof data. The environments are better read as an evaluation and a research testbed than as a ready training recipe.

Which problems are left out

Only environments whose official proof was verified end to end inside the sandbox made the cut. The 36 excluded statements break down per the card:

One technical note from the card matters for trust: in eight of openai/math's Comparator configs, definitions written out in the statement were listed as "holes" that Comparator does not check, so a solution could redefine them. In this dataset they must match exactly, and affected tasks list them under fixed_definitions.

Why this matters beyond math

Three threads meet here.

Open reproduction of lab research. OpenAI released the math statements and manuscripts; the community converted them into runnable infrastructure within days. That is the same pattern as open-source evaluation harnesses, and it fits the Hugging Face push for shared environments.

Verifiable rewards. Lean is among the few domains where "correct" is checked by a small trusted kernel. That makes it a clean test of whether open models can do research-grade reasoning, in the spirit of the Opus 5.5 science experiments we covered in agents finding room-temperature magnetic semiconductor candidates.

Contamination. The card warns the statements and proofs have been public since October 6, 2026, so any model trained on web data after that date may have seen them. Treat future benchmark claims on this set with that in mind.

The surrounding controversy

The underlying OpenAI release is contested. Our post on what to check in the 722 manuscripts and the roundup of expert reactions to the math results cover why mathematicians want independent review, and the Association for Human Mathematics statement shows how heated it is. Lean checks that a proof follows from the stated formal statement. It does not check that the formal statement says what a mathematician means, and the dataset authors themselves warn to read any proof that scores 1.

What people are asking

Small shape reaching for a green token at the end of a path, the sparse reward signal of a Lean proof environment

Can a current model actually solve one? The card does not report agent results, and it says to expect zero on almost every task. Some tasks are far smaller than others: the Abhyankar-Sathaye reference proof is 15 modules, versus 322 for affine Bernstein rigidity, so the shortest tasks are the realistic place to look for a first nonzero score. No independent solve has been reported that I could find.

Is it safe to run untrusted agent output? The design is cautious. The agent sandbox has no network access, the verifier runs in a separate environment, and the card describes tests against reward-file planting and code that executes during grading. Still, you are running Docker images of about 9 GB on a third-party backend, so review the generator code first, as you would for any skill or harness you did not write.

Does this compete with existing Lean benchmarks? It is different in kind. Most Lean benchmarks use known, already-solved statements. These statements come from a fresh research release, with reference proofs that are new and not independently reviewed. That makes them more interesting and more fragile at once.

What does a nonzero reward prove? That a proof of the exact formal statement passed the Lean kernel using standard axioms. It does not prove the formal statement matches the informal theorem. The card tells users to read any proof that scores 1.

Why 4 hours per task? That is the agent timeout per the card, with a verifier timeout of several hours for the heaviest proofs, which is why a full sweep of 369 tasks is a serious compute commitment, not a weekend script.

How to try it

Per the dataset card:

pip install "harbor[daytona]>=0.24" daytona
hf download FineEnvs/openai-math --repo-type dataset --local-dir openai-math
cd openai-math

# build the shared sandbox image once: Lean 4, Mathlib, Comparator, about 9 GB, around an hour
(cd generator && python -m openai_math_harbor.snapshot)

# run an agent on a couple of tasks
harbor run -p tasks -e daytona --ek snapshot_template_name=SNAPSHOT_NAME \
  -a AGENT -m MODEL -i plane-coloring -i hilbert-crouzeix -n 2

Replace SNAPSHOT_NAME, AGENT and MODEL with your own values. You need a Daytona API key and credentials for whatever agent you run. A sensible first step is the oracle run on one task, which submits OpenAI's own proof so you can confirm your setup grades correctly before spending model budget.

What to watch next

• Whether anyone reports a nonzero reward from an open model on any of the 369 tasks, and whether those proofs survive review.
• Whether a more forgiving reward, accepting equivalent formulations or partial progress, is released alongside this strict one.
• Whether the 36 excluded problems get covered once the sandbox gains extra Lean packages and more memory.
• How the same pipeline extends to the remaining formalizations OpenAI says it will add.

Related reading

• Hugging Face puts RL environments on the Hub: OpenEnv explained
• OpenAI's 722 math manuscripts: what to check
• OpenAI math results that matter: expert reactions
• The OpenAI 400 math papers rumor: claimed versus verified
• Association for Human Mathematics statement on OpenAI
• Opus 5.5 agents and magnetic semiconductor candidates
• Sources: FineEnvs/openai-math dataset card, Harbor, Comparator

Counts and requirements come from the dataset card as read on October 11, 2026 and may change as the dataset is updated.