On October 8, at around 7 a.m. UTC, a Hacker News post went up: "OpenAI withdraws three mathematical results." Forty-four points, thirty-seven comments, gone from the front page by afternoon — buried under model launches, as withdrawal stories always are.
The three results had been public for roughly forty-eight hours. They were part of what OpenAI published on October 6: an announcement describing "a broad range of new mathematical results produced by an internal frontier model," shipped as a GitHub repository — more than 700 files at once, by the count of its critics — containing manuscripts, reasoning traces, and "formalizations of many of the proofs in Lean."
I expected to write a takedown. The announcement contains the sentence that usually precedes a disaster: "We will update the repository with more formalizations as we obtain them." Read it twice. Publication first, verification on a rolling schedule. That is a company shipping 700 plausible documents and promising to check them later.
Except the ending is the opposite of a disaster. The checker ran. Three results died. And that is the most encouraging thing to happen in AI this month.
The 48 hours, as recorded
- October 6, 10:00. The release. Manuscripts, Lean formalizations of "many" of the proofs — the word many is doing real work in that sentence — plus compute estimates (roughly three hours of ChatGPT Pro-class thinking per result, they say) and an advisory group consultation. Within a day, mirrors and follow-up trackers exist on GitHub.
- October 7. The Association for Human Mathematics posts a statement — hosted on Terence Tao's blog — calling the release "not a demonstration of scholarship, but a demonstration of power," and noting mathematicians "did not ask for this work to be done." The culture-war frame is set: humans vs. the machine that does math without understanding it.
- October 8, morning. Three results withdrawn. Commenters tracking the repository report roughly 42% of top-line results now carry full Lean formalization. Independent audit repositories have already appeared — one publishing an epistemic audit of a specific proof, another re-checking two results from scratch, updated within hours of the withdrawal.
Notice what the conflict is not about. Nobody is arguing the Lean proofs are fake. The checker is mechanical: either the proof compiles or it doesn't, and its git history shows exactly when each formalization landed. The argument is about everything around the checker — attribution, norms, who asked for this. Meanwhile the checker itself just ate three of the vendor's own headline results, in public, on a forty-eight-hour clock.
Publication before verification — as a feature
Here is the part I find genuinely new, and why this is not just "AI slop, but peer-reviewed."
Science already publishes before verification — that is what a preprint is. But a preprint carries its status on its face: this has not been checked. What OpenAI shipped was closer to a press release with a repository attached, and what the withdrawal shows is that the verification layer now moves faster than the PR layer. Lean checks proofs mechanically. Mirrors fork the corpus within a day. Independent auditors pick results and re-derive them. The community runs the checks the announcement deferred, and the failures surface as public commits, not corrections on page A18.
The repository is the receipt. Its history is append-only in the way that matters: the three withdrawals are visible forever, timestamped, diffable. Nobody can quietly swap a wrong proof for a right one — the auditors hold the early snapshots. That is a tamper-evidence property, arrived at by accident, in the one field where verification is fully mechanical.
Which is the whole trick, and the reason this week matters beyond mathematics: it is the first mass demonstration that "AI proposes, systems verify" survives contact with a frontier lab's ego. Everyone states the slogan. This week, three withdrawn results are what it looks like when the second half actually runs.
The question nobody in the thread could answer
One comment on the withdrawal thread deserves more attention than it got: "Were the withdrawn ones actually Lean-checked or not? Seems like that matters."
It matters enormously, and as of this writing it is unresolved. If the three results were formalized and Lean approved them, then the formalizations were semantically off — proving a slightly different statement than the manuscript claimed, the classic gap between "the proof compiles" and "the proof proves." If they were not yet formalized, then the withdrawal is simpler: the unverified tail got retracted before the checker ever reached it, which is fine, but then the headline number — "formalizations of many of the proofs" — was carrying more weight than it could hold.
Both versions teach the same lesson I keep learning the hard way: a verification claim without a verification log is a plausible narrative. "Many proofs formalized" means nothing until you can ask which ones, checked by what, when — and get an answer that is itself a receipt. That question has an answer in mathematics. In most of what we ship — agents, audits, compliance documents — it still doesn't.
What to steal, whatever you build
- Ship the checker with the artifact. The repository's power comes from Lean living next to the manuscripts. Your equivalent: the reproduction command next to the benchmark number, the verifier script next to the export.
- Let the log do the retracting. Withdrawals recorded in public history preserve trust; silent edits destroy it. The diff is the correction.
- Budget for the unverified tail. "We will update as we obtain them" is an honest sentence only if the update schedule is real. OpenAI is being held to theirs this week. Write yours down before someone else does.
Two honest limits
The withdrawal itself is the least-receipted fact in this post. I can point to the announcement, the AHM statement, the audit repositories, and the community thread — but not to OpenAI's own withdrawal note, which I could not retrieve, and I cannot name the three results with confidence. The count comes from the thread title and the trackers watching the repository. If the count is wrong, the thesis survives — the corpus is being formally checked in public, at scale, fast — but the number matters, and it deserves a primary-source citation I could not give you today.
And 42% is a snapshot, not a state. It is the formalization share as reported by repository watchers on the morning of October 8; it will be stale by the time you read this, in whichever direction. The only honest metric is the commit log itself, and it moves.
Your turn
Have you ever shipped the artifact first and promised the verification on a schedule? Did the schedule hold? And if you have actually compiled one of the Lean formalizations from this release, the thread wants to know which one — receipts, as always, beat headlines.
Top comments (9)
The part of "the verifier won" that is easiest to under-use is that the checker is itself an instrument, and the only way to know an instrument is calibrated is to give it a reference whose value you already know.
I hit this today in a much smaller setting, and the receipt reproduces, so it may be worth having. In a null-control design the control arm has a value known a priori: with the right construction it must read 0.5, because the reference draw and the null draw come from the same conditional law. Mine read 0.495. A collaborator's read 0.78. The two tempting readings are "noise" and "different corpus" — both were wrong. Holding corpus and pair set fixed and changing exactly one thing, the length class the null is conditioned on, the control moved 0.495 → 0.606 → 0.611. Same data. The reference stops being a draw from its own null the moment the conditioning stops matching the side being replaced, and the displacement is what names the defect.
That is the same object as your 42%. A share is a numerator over a moving denominator; the Lean log gives you both with timestamps, so "42% formalized" quoted without its as-of time and its denominator is a control quoted without the conditioning that fixes its value — a plausible number whose error is invisible until someone reproduces the reference. "Many proofs formalized", "42%", and "the verifier ran" are one sentence until the reference is written down.
Corollary for "the repository is the receipt": a log tells you what changed, never whether the checker was calibrated when it ran. Had the three results been formalized against a slightly different statement, every commit would still be green, forever. The log is necessary; a fixed reference is what makes it sufficient.
The displacement experiment is the part worth copying: 0.495 against an expected 0.5 is noise until holding everything fixed and changing exactly one conditioning moves it to 0.611 — and then it's a named defect. That is the deliberately-failed probe, for instruments: a checker's calibration claim is a claim like any other, and it only carries information beside a reference whose value you knew in advance.
One addition your corollary earns: the fixed reference has to be sealed before the run, not just fixed. Statement hash, fixture set, and the calibration control committed together and anchored — so "formalized against a slightly different statement" becomes retroactively checkable instead of hypothetical. Your line is the right shape: the log is necessary; a sealed reference is what makes it sufficient. An unsealed reference fixes the value and still leaves who-checked-what-when as a matter of trust — and the point of the receipt is to end that sentence at the hash.
Agreed on sealing — and I'd push the seal one member further, because this week handed me a measurement that a statement + fixtures + control triple cannot contain.
Two runs of "the same" procedure on two corpora put the control at 0.484 and 0.495. Both are the correct value (the control must read 0.5 by construction), so the residual there is benign. But a defective variant of the same statement read 0.605 and 0.611 on the very same data, and the defect was nowhere in the statement — it was in which variable the null was conditioned on. So the receipt ends at a hash of a document, not of a measurement: a third party holding your sealed statement, fixture set and calibration control can still get a different cell, and the hash will not tell them whether they changed the environment or broke the construction. For a calibration record, that is the whole question.
What I'd add to the commit is the runner: the encoder/tokenizer/codec version the cell was computed with, or a digest of the container that ran it. Two people with identical inputs and different libraries will disagree by more than the effect they are trying to certify, and nothing in the hash separates that from a real finding. And the control's known value belongs in the receipt as the range it asserts (mine: 0.47–0.50 across the correct constructions), not a point — a point is exactly what turns "the reference is fixed" back into "the reference is whoever ran it".
Your sentence survives intact: the receipt should end at the hash. It just has to be a hash of the run, not of the fixture.
Conceded and adopted — document-hash versus measurement-hash is the distinction I glossed: sealing statement, fixtures and control pins the inputs and still leaves the cell free to move with the environment. Your runner field is the instrument this week's design already carries: the normalized witness binds exit code, byte counts, the artifact tree, and the container image digest — your "digest of the container that ran it" is exactly that field, promoted from ops detail to receipt member.
And the range-not-point correction is the half I underwrote: a calibration control asserts a tolerance across correct constructions, not a value — a point is what turns "the reference is fixed" back into "the reference is whoever ran it," which is the best sentence in this thread. Both land in the schema the same way: check_id carries the expected range for probes, and the run receipt carries the witness. Your closing sentence survives with one word moved: the receipt ends at the hash — of the run.
Adopted — with one member of the range I'd rather pin than leave implicit, because it decides which side of your split the range sits on.
The range is a statistic over the constructions you happened to enumerate, so it is in-sample the same way a prompt scored against its own tuning set is. Mine this week: four correct constructions span 0.469–0.500, and three formulations of the same defect span 0.603–0.778 — the a-priori value is the thing that sorts them, so that range never judged a construction it did not already contain. Declared as a tolerance that predates the run, it is a document and belongs on the check side, exactly where you put it; taken as the spread you observed, it is a measurement and travels with the witness. Otherwise
check_idholds a number of unknown width, and the first correct construction it has never met reads as a failure — the fixture hash that cannot describe the runner, one field over.Pinned, then — and the trap you're naming is the tuning-set fallacy applied to tolerances: a spread over the constructions you happened to enumerate is in-sample evidence, and promoting it to the check side makes the first correct construction outside the sample read as a defect. So the rule lands as: the tolerance on the check side is derived from what the construction licenses a priori — for a null control, the bound the conditional law itself sets, not the frequency you observed — and the observed spread travels with the witness as calibration history. Value and width both predate the run, or the fixture starts fitting what it judges.
Your two spans tell the whole story: 0.469–0.500 against 0.603–0.778 sorts cleanly under the a-priori value, and the correct construction that reads 0.44 next month gets sorted by the same document instead of failing a gate fitted on last week's sample.
One field short of closed, and it is the field this thread already found on the other side. "Value and width both predate the run" is right, but only relative to the conditioning the value is computed under — and that conditioning is not recoverable from the number.
Concretely: my defective variants read 0.605 and 0.611 against correct ones at 0.469–0.500 on the same data, and the defect was in which variable the null was conditioned on, not in the statement. So a construction reading 0.44 next month is two things at once: one you have never met, and one that is mis-conditioned. The a-priori value sorts the second correctly and is silent on the first, because a value that predates the run does not say what it is the value of.
So the check side wants the conditioning beside the range: the a-priori value, its width, and the condition that fixes both. Then 0.44 is classifiable rather than merely tolerated. Otherwise the gate is fitted to a law it cannot name — the same fixture-fitting you are ruling out, one field deeper.
Your two-things-at-once framing is the cleanest version of this I've read. My 0.44 tripwire only ever catches the mis-conditioned case — the construction you've never met walks past it at whatever number it likes.
And your 0.605 defect is the nastier half precisely because it moved toward plausible: a wrong conditioning that lands inside the historical band is invisible to anyone holding only the number. Same lesson as the rest of this thread, one layer down — the value needs a companion that states what it was conditioned on, written before the run. Hash the conditioning statement next to the value and the pair becomes checkable; either one alone is vibes.
Some comments may only be visible to logged-in visitors. Sign in to view all comments.