The proof checker doesn't care who wrote the proof

TL;DR

• OpenAI published 722 manuscripts from an unreleased model and says they resolve open problems. Only some are machine-checked in Lean.
• The 2022 paper ran a loop: search for Lean proofs, then fine-tune on the proofs found. Given graded problems, it climbed to harder ones without human proofs.
• A Lean check makes a proof trustworthy whoever wrote it. It doesn't confirm the formal statement says what the paper claims, or that the result is new.

What happened

On October 6, OpenAI released 722 manuscripts, grouped into 372 "result families", in the public openai/math GitHub repository under an Apache-2.0 license. The README says an unreleased internal model produced the vast majority of the results. It says the model was given roughly 4,000 open problems and that the average result used about three hours of ChatGPT Pro-equivalent "thinking" compute. OpenAI claims some of the results resolve long-standing open problems (Unite.AI). For a subset of the manuscripts, a formalization catalogue (lean/formalization.yaml) points to a Lean theorem for the main result. The README adds: "Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly."

Independent checking is a separate matter. The Lean files can be re-checked by anyone, and Scientific American notes that the formalized results are "all but certain to be correct." The rest are claims until mathematicians review them. MIT's Andrew Sutherland told the magazine that until OpenAI releases the model, claims about one-shotting problems should be treated "as unverified." An advisory group on mathematics and AI at the Institute for Advanced Study had asked companies to publish the model, the exact prompt and the compute behind each result. OpenAI disclosed only the average compute. Unite.AI quotes the group: "we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models."

The paper in brief

In 2022, OpenAI researchers had a 774M-parameter GPT-style model propose proof steps ("tactics") for the Lean proof assistant, and used Lean to accept or reject every step. The core idea is expert iteration. Run proof search over a set of statements, keep the proofs that Lean accepts, fine-tune on them, and repeat. When the statements varied in difficulty, the loop solved easy ones first and then increasingly hard ones, with no human-written proofs for the hard ones. On miniF2F, a benchmark of formalized competition problems, test pass@1 rose to 29.6% from the previous best of 24.6%. The paper mattered because it showed that, in formal math, a supply of statements can stand in for the self-play opponent that drove game-playing AI.

The math

Proving as search

A proof starts from a goal $g_0$, the theorem statement as a Lean tactic state. The model reads the current goal and samples a tactic $t_1$. Lean runs it and returns a new state $g_1$, which may contain several subgoals, or an error. The proof is complete when no goals remain. The action space is unbounded, because a tactic can contain any term the model chooses to write, such as a witness for "there exists an $x$".

The first-round model scores a partial proof by how likely the model found its own steps:

$$s(g_n) = \sum_{i=1}^{n} \log p_\theta(t_i \mid g_{i-1})$$

Here $p_\theta(t \mid g)$ is the language model's probability of tactic $t$ given state $g$ (in the paper, also given the theorem's name), and $\theta$ are its weights. This is the chain rule of probability in log space, the same sequence log-likelihood you maximize in MLE. Best-first search keeps a queue of open states, expands the highest-scoring one by sampling $e = 8$ tactics, and stops after $d = 512$ expansions. (This is my compact version of the GPT-f search the paper cites; it leaves out bookkeeping for multiple goals.)

A learned value: expected shortness

Log-probability favours short, confident proofs, but it can't tell when a goal is a dead end. Later models learn a value instead. For each goal visited during past searches, the model is trained to emit one token: a bucket $b \in \{0, \dots, 10\}$. Bucket 0 means "never proved", 1 means a proof longer than 20 steps, and buckets 2–10 cover shorter proofs, with 10 the shortest. At search time:

$$v(g) = \frac{1}{10}\sum_{b=0}^{10} p_b(g)\, b$$

$p_b(g)$ is the model's softmax probability for bucket $b$ at goal $g$. The paper writes the normalizer as $\#B$, the number of buckets. I use 10 so that the endpoints come out at 0 and 1, matching the paper's own example. This is an expected value under a categorical distribution, trained with ordinary cross-entropy. No separate value head is needed, only extra training examples.

Worked example. Goal A has $p_0 = 0.5$, $p_6 = 0.2$, $p_{10} = 0.3$, so $v = (1.2 + 3)/10 = 0.42$. Goal B has $p_0 = 0.1$, $p_3 = 0.9$, so $v = 0.27$. Search expands A first, even though A is more likely to be a dead end, because when A is provable its proofs tend to be short. The value mixes "provable?" with "how quickly?", which pushes the system toward shorter proofs.

Expert iteration

Let $S_k$ be the successful searches from round $k$, run with model $\theta_k$. Each round builds a dataset $D_k$. It contains the human tactic data, every (goal, tactic) pair from proofs found so far, and (goal, bucket) pairs, where goals visited but never proved are labelled "infinite". The pairs are deduplicated across rounds, keeping the shortest proof size for each goal. Then:

$$\theta_{k+1} = \operatorname{FineTune}_{\text{1 epoch}}\!\Big(\theta_0;\ \mathcal{L}(\theta) = -\sum_{(x,y)\in D_k} \log p_\theta(y \mid x)\Big)$$

$x$ is a prompt (a goal, plus the theorem name), and $y$ is either a tactic or a bucket token. Each round fine-tunes the fixed base model $\theta_0$ rather than the previous model, and runs exactly one epoch. One useful way to read this is as approximate policy iteration. Search with the current policy finds better behaviour than the raw policy (the "expert"), and fine-tuning distills that behaviour back into the policy.

Training on a model's own outputs usually risks amplifying its mistakes. What makes it safe here is that every positive example passed Lean's checker, so the positives have no label noise. The negatives are noisier: a goal marked "unproved" may simply not have been explored. The paper notes this.

Why a curriculum works

Here is a toy model. It treats a proof as $n$ independent steps that each succeed with probability $q$, and every attempt as a fresh, independent sample. Real tree search is smarter than this, so the model is only for intuition. Then

$$\text{pass@}k = 1 - \left(1 - q^{n}\right)^{k}$$

where pass@$k$ is the chance that at least one of $k$ attempts succeeds. With $q = 0.5$ and $n = 6$, pass@8 is about 11.8%. Raise $q$ to 0.7 and pass@8 jumps to about 63%. Easy statements raise $q$, and because $q$ enters as $q^n$, a gain in $q$ helps deep problems the most.

Toy model: more attempts vs. a better policy

interactive

• pass@k at q
• pass@k at q + 0.1

Hover or drag across the chart to read values.

per-step success q0.5proof steps n6

per-attempt success qⁿ:

1.56%

attempts for 50% at q:

45

attempts for 50% at q + 0.1:

15

What the results say

• Learning beats sampling at equal compute. On held-out mathlib theorems, pass@1 rose from 56.3% ($\theta_1$) to 62.6% after eight rounds. That beat a sample-only loop even after the loop was given the extra compute that expert iteration spent on training.
• The curriculum effect. On 5,600 generated inequalities with no proofs supplied, the loop eventually closed 6 problems at the hardest composition depth ($N_D = 6$). The sample-only loop closed none at that depth.
• miniF2F. On the test split the fully iterated model reached 29.6% pass@1 and 36.6% pass@64, against 24.6% pass@1 for the earlier PACT baseline. Solved problems included 26 from the AMC12, 6 from the AIME and 2 adapted from the IMO.

Limitations. The authors say the models rarely chain more than 2 or 3 non-trivial reasoning steps, and they are "very far" from competing with top students. Only 100 of the 327 hand-formalized curriculum problems were ever closed. The full run took about 2,000 A100-days, and only one model size was studied. A footnote is telling: one "IMO" problem the model solved is "a much weaker version than the original problem." And "no ground-truth proofs" still meant humans had to write the formal statements.

Connecting the dots

This paper is background on the idea, not the method behind the release. OpenAI hasn't described how its new model works, and nothing here says it uses expert iteration or best-first search. What the paper does explain is the logic of trust.

Lean accepts a proof only if its small kernel type-checks every step. That is why a proof can be trusted without trusting whatever wrote it, whether a 774M model, an unreleased frontier model or a graduate student. In 2022 every result was formal by construction, because the search ran inside Lean. The new release is different: it is mostly natural-language manuscripts, and Lean formalizations cover only some main results. The guarantee applies to that subset and nowhere else.

Even there, a kernel check certifies the formal statement. It can't tell you whether that statement faithfully captures the claim in the paper, as the weakened IMO problem shows. Nor can it tell you whether the result is new, which is a question about the literature, not about logic. That is why mathematicians' objections centre on review, attribution and access to the model, not on whether Lean works.

Why it matters

For practitioners, the 2022 lesson travels well. Self-training is safe roughly to the extent that you have a reliable checker, whether that's Lean, a test suite or a simulator. For researchers, the paper's conclusion still reads as the agenda: progress may come down to generating good statements at the right difficulty.

For the mathematical community, a fast-growing pile of claims makes the line between "checked" and "claimed" the central issue. Things to watch next:

• whether the formalized share of the catalogue grows, and whether outside experts audit the formal statements against the manuscripts;
• whether OpenAI releases per-result prompts and compute, as the advisory group asked.

Go deeper

• Formal Mathematics Statement Curriculum Learning (PDF), plus the paper's lean-gym environment
• openai/math on GitHub: the manuscripts, the README caveats and lean/formalization.yaml
• OpenAI's announcement and Unite.AI's report
• Scientific American on mathematicians' reactions
• Prerequisite: Generative Language Modeling for Automated Theorem Proving (Polu & Sutskever, 2020), the GPT-f paper that introduced the proofstep objective and log-probability search