Verified Is Not Discovered: What a Proof-Checker Can't Tell You已验证不等于有发现：证明检查器无法告诉你的事

On October 26, 2026, OpenAI said an internal model had done something that, taken at face value, would be among the most important scientific events of the decade. It disproved the Exponential Time Hypothesis, a cornerstone of computational complexity. It proved the local smoothing conjecture in every dimension, which the company says also settles the Kakeya and Stein restriction conjectures. And it produced existence proofs for key quantum field theories, including QCD and Yang-Mills — the kind of problem that carries a million-dollar prize. Two of the three arguments were checked line by line by a proof assistant called Lean and posted to a public repository for anyone to inspect.

The natural conclusion — the machine did the research, and the machine's work has been verified — is the one almost every headline reached. It is also the one claim a Lean check cannot support. A proof assistant certifies exactly one thing: that a chain of formal steps follows from the axioms it was given. It says nothing about whether the statement at the top of that chain is the famous conjecture, whether the result is new, or, in the physics case, whether the symbols describe the real world. Verification narrows the thing you have to trust. It does not hand you a discovery you can stop thinking about.

What a proof assistant actually certifies

Lean belongs to a family of tools built on an old idea, sometimes called the de Bruijn criterion: instead of trusting a long, clever argument, you reduce it to small, dumb steps and let a tiny, trusted program re-check every one of them against a fixed set of axioms. If the program accepts the proof, you have about as much certainty as mathematics offers that the formal theorem really does follow from the formal rules. This is a genuine advance over much of what AI systems have produced in mathematics so far, which has often been fluent natural-language argument that falls apart under scrutiny. A Lean-accepted proof does not fall apart that way. It eliminates the single most common way a formal argument dies — a hidden logical gap that everyone, including the author, overlooked — provided you also trust the kernel's own code and that the axioms it starts from are consistent rather than quietly contradictory.

So when OpenAI formalized its computer-science result on October 17 and its mathematics result on October 19 and put both on GitHub, it did something real and checkable. Reviewers do not have to take anyone's word that the arguments hang together. The kernel already said they do.

But notice what that sentence contains and what it leaves out. The kernel verified that a specific formal theorem — call it T — is derivable. T is a string of symbols a human wrote down to stand in for an informal conjecture — call it C — that lives in textbooks and in the heads of the people who have spent careers on it. The kernel never checks that T means C. It cannot. "Means" is not a formal relation; it is a human judgment about whether a translation is faithful.

The check reads one side of a translation

Here is the move that the word "verified" quietly performs. Every formal proof of a famous result rests on a translation step that no proof assistant can audit: someone has to write the formal statement, and someone has to agree that it says what the conjecture says. If that translation is faithful, the Lean check is close to decisive. If the translation quietly weakens the claim, adds a convenient hypothesis, or defines a key object in a way that makes the proof go through, the kernel still prints the same green result. The proof is valid. The theorem is just not the one you thought.

This is not a hypothetical worry. One recent human audit of OpenAI's earlier AI-generated proofs, published this autumn by Mikołaj and Krzysztof Sienicki, draws exactly this line: formal verification confirms that a proof obeys its formal rules without guaranteeing that the proof is mathematically sound or novel. A result can be formally verifiable and still carry unstated assumptions, logical gaps relative to the intended claim, or no genuine insight at all. Verification, they argue, is necessary and nowhere near sufficient; the mathematical content still has to be judged by mathematicians.

The checker, in other words, reads one side of the translation with perfect care and never looks at the other side. The harder and more surprising the claim, the more weight the translation has to bear — and the less a green check tells you.

What OpenAI released, and what it held back

The company's own conduct is the clearest evidence that it knows the check is not the claim. The mathematics and computer-science formalizations were released. The physics was not. OpenAI says it formalized its Yang-Mills result in Lean on October 16, and then — instead of posting it — withheld the artifacts and handed them to a human group that includes David Gross, Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov. Jaffe helped write the official statement of the Yang-Mills problem in the first place. If a Lean formalization settled the matter, there would be little left for that group to do. The decision to route the boldest claim to human experts, rather than let a public Lean file stand on its own, tells you a great deal about what OpenAI thinks the check settles. Some of that reticence may be strategic — a company does not have to publish everything — but the plainest reading, reinforced by the language of the announcement, is that a formalization of a physics existence proof is only as trustworthy as the definitions it starts from, and judging whether those definitions capture real physics is a job for physicists, not a kernel.

The language in the announcement points the same way. OpenAI called the model's output "raw research data that must still be converted into scientific understanding," and conceded that its choice of which experts to involve first "inevitably shapes who becomes involved first and creates an asymmetry of information." That is a company describing unfinished work handed to humans to finish — not a settled discovery.

None of the three claims has been peer-reviewed. The model that produced them is internal and unreleased, so no outsider can reproduce the result or probe where it is fragile. Even the headline is more modest than it sounds: the disproof of the Exponential Time Hypothesis comes with an algorithm that runs in roughly two-to-the-n-over-root-log-n time — subexponential, but still far slower than any polynomial, so it leaves the P-versus-NP question exactly where it was. And the repository already contains a cautionary example. On October 7, one day after an earlier large release, a sign error in an AI-written manuscript invalidated an argument and three papers were withdrawn. Lean catches the errors that live inside the formal proof. It does not catch the ones that live in the step before it, where a human turns an idea into symbols.

The strongest case that this time is different

The fair counter deserves a hearing, because it is strong. A Lean proof is not nothing. It removes the failure mode that has embarrassed every previous wave of AI mathematics, and it does so publicly, in a form specialists can attack. The people doing the checking are not a marketing department; they are, in several cases, the very researchers who posed the conjectures. Russell Impagliazzo and Ramamohan Paturi, two of the three who introduced the Exponential Time Hypothesis more than two decades ago, are reviewing its claimed disproof alongside Ryan Williams of MIT. These are the right judges, and they now hold the formalizations in their hands. If they come back and say the formal statements are faithful translations and the proofs are novel and correct, the headline will have been earned.

That is the point, though, not a rebuttal of it. The thesis here is not that the results are wrong. Any of them might be a real advance; the mathematics community will tell us. The thesis is about what is doing the confirming. In every version of the good outcome, it is the human review that ratifies the discovery, with the Lean check as a strong but junior witness. The green result got the proofs into the room. It is the people in the room who decide whether a translation is faithful and whether an argument is new. That labor cannot be formalized, which is exactly why it has not been.

There is a sharper version of this counter worth stating plainly, because it cuts against our own framing. We have leaned on the translation step — the gap between the formal statement and the famous conjecture — as the place where trust now sits. But for conjectures this famous, the formal statements are not obscure. The Exponential Time Hypothesis and the Yang-Mills existence problem have canonical, publicly argued statements that specialists can read and compare against a formalization in an afternoon. Where the conjecture is standard, the faithfulness question is narrow and quickly closeable, and a Lean check really does come close to settling the argument. That is the honest limit of our point. For these particular results the residual gap is less about whether the statement is faithful and more about whether the proof is a genuine discovery — new mathematics — rather than a well-formalized assembly of known moves. Faithfulness a specialist can check in an afternoon. Novelty and significance they cannot, and no proof assistant was ever built to try.

Verification moves the trust; it does not remove it

Strip away the spectacle and a simple structure remains. A proof assistant converts the question "is this argument internally correct?" — which used to swallow most of a referee's time — into two questions it cannot touch: "is the formal statement really the conjecture?" and "is this a genuine discovery?" Both are judgments about meaning and novelty, and both still belong to humans. Verification did not abolish trust. It relocated it, from the long chain of proof steps to the short, unglamorous translation at the top and the harder question of worth underneath.

That relocation is real progress. Moving your trust from a thousand fragile steps to one well-scrutinized definition is a better place to stand. But a better place to stand is not the same as no longer having to stand anywhere, and the headlines are selling the second thing while OpenAI, in its own repository and its own careful sentences, is doing the first.

What this means if you use AI to do your own work

This is not really a story about Millennium Prize problems. It is the everyday shape of working with capable AI, scaled up to its most dramatic form. You ask a system to produce something, and it hands you an artifact that passes a check: the tests are green, the code compiles, the proof is accepted, the linter is clean. The temptation is to read the passing check as "done." These checks differ enormously in strength — a Lean kernel proof is a complete deductive guarantee relative to its axioms, while a passing test suite is only a handful of sampled examples — and the lesson survives the difference, because even the strongest possible check is silent on the same three things. A check only ever tells you that the artifact is internally consistent with the specification you gave it. It is silent on whether the specification was right, whether the output is novel or merely a fluent rearrangement of what already existed, and whether the thing was worth building at all. Those are the same three questions the Lean kernel cannot answer, wearing work clothes.

The practical move is to keep the human judgment step and refuse to let "verified" stand in for "correct and worth doing." A green check is an input to your judgment, not a replacement for it. This week's small test costs nothing: take one AI output you called "done because it passed," and write down, in a single sentence, the one thing the check did not actually verify. If you cannot name it, you have not finished reviewing — you have only watched the machine review itself.

What would change our mind

The judgment here is falsifiable, and the next few months will test it. If the named expert groups — Impagliazzo, Paturi and Williams on the Exponential Time Hypothesis, and the Gross group on Yang-Mills — publicly confirm in peer-reviewed venues that the formalized Lean statements are faithful to the classical conjectures and that the proofs are novel and correct, then human review will have ratified all three headlines, and the role of the Lean check as decisive-by-itself will look stronger than argued here. The opposite also counts: if review turns up a formalization gap, a quietly weakened statement, or a withdrawal like the one on October 7, the case that verification is a narrow witness rather than a verdict gets stronger still. Either way, watch the humans, not the checkmark. The checkmark has already told you everything it knows.