After 722 AI-written math manuscripts landed at once, several of the most-read pieces over the next two weeks raised the same problem: checking and understanding can’t keep pace with generation. OpenAI posted them on October 6 to its public repository, openai/math, and withdrew three the next day. A Fields medalist admitted the release had made them cry, while a video titled “There’s never been a better time to go into math” took off. I read the posts about all this that reached the top of Hacker News (HN) through October 19.
722 manuscripts, 4,000 problems
OpenAI put the manuscripts and Lean proofs in a public GitHub repository, openai/math. The first README listed 722 manuscripts in 372 families of related papers. The vast majority came from the same procedure using an unreleased internal model. Each result used three hours of ChatGPT Pro thinking compute on average, and the model was posed roughly 4,000 problems.
Scott Aaronson works it out on his blog, Shtetl-Optimized: the model “merely” solves about 10% of the longstanding open problems it is asked about, after a single three-hour attempt. The release includes a proof of Subhash Khot’s Unique Games Conjecture. The README, though, says results are at different stages of verification. Not all have Lean formalizations, and some of the unformalized results could have issues.
OpenAI first released 722 manuscripts. One dot is one manuscript.
They are grouped into 372 families of related papers. Dot positions do not follow any order.
The next day, October 7, three of them were withdrawn, leaving 719.
A single sign error in one manuscript took down two others built on the same construction.
As of that day, 300 top-line results, about 42% of the remaining 719, were formalized in Lean.
The rest have not had a computer check their proofs step by step.
Three withdrawn the next day
On October 7, an entry in the repository’s change log (history.md) withdrew three manuscripts tied to the Hodge conjecture. The reason is short: a sign error in one paper invalidates a cancellation argument, and two papers that used the same construction went with it. The withdrawal notices add that they concern the proofs and do not assert that the statements are false. The same update revised 14 other manuscripts with proof repairs, corrected statements and more, and added 6 Lean formalizations. Of the 719 manuscripts that remain, 300 top-line results, about 42%, are now formalized.
OpenAI’s Dan Roberts announced the update on X, where the post drew 1,804 likes and 544,000 views; on HN it reached 381 points and 612 comments. The README also notes that some outputs build upon earlier results produced by the models. That is how one error reached three manuscripts.
What Lean checks, and what it doesn’t
When a result is formalized in the Lean proof assistant, a computer checks the proof step by step. In a guest post on Terence Tao’s blog, Thomas Hales marks the limits of that guarantee. A proof the kernel accepts can still be wrong if the kernel has a bug; this summer, a Lean bug produced an illicit “disproof” of the Collatz conjecture (since fixed). The more common trap is the statement: Lean checks that a proof matches its statement, not that the statement and definitions mean what we intend.
A proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity.
Thomas Hales, guest post on Terence Tao’s blog
Hales adds that this audit is generally massively easier than checking the proof itself. As I see it, the 42% figure is a starting point: the unformalized manuscripts still need formalizing, and the formalized ones still need their statements audited.
Some weep, some welcome it
In the essay “I know why the mathematicians weep” (397 points on HN), Derek Thompson gathers reactions from mathematicians. Hugo Duminil-Copin, who won the Fields Medal in 2022, said this after the October release:
Tuesday night, I cried and it woke up my daughter. They have annihilated my field of research.
Hugo Duminil-Copin, quoted by Derek Thompson
On the day of the release, Terence Tao posted a four-part thread on Mathstodon (614 points on HN). In what Tao calls “Math 1.0”, when a long-standing conjecture falls, its authors give talks and workshops follow; collaborations and follow-up problems appear, new people join the field, and the proof is streamlined into the next generation’s textbooks. Tao writes that the opposite is now often happening: people who have AI solve a problem move on without understanding the output well enough to explain it, and far fewer seminars and collaborations follow. Promising directions are even being withheld for fear of being scooped.
Solutions to open problems are now being harvested at large scale in an unsustainable fashion.
Terence Tao, Mathstodon, 2026-10-06
Tao’s “Math 2.0” would count exposition, community building and opening new directions as mathematical progress alongside problem solving. Tao believes AI can contribute to all of these, but says it will take more imagination and ambition than pointing a favorite AI agent at open problems and asking for a solution.
Aaronson’s post (409 points on HN) strikes a different note. Some of the results come with Lean certificates, yet almost no one has understood the proofs. Even so, Aaronson calls the position that no one should spoil the fun by solving open problems with AI “totally untenable”; these capabilities will reach anyone with a GPT or Claude subscription anyway.
No human has understood just about any of these proofs yet; the race to do so has just started.
Scott Aaronson, The Mathocalypse
Aaronson sees two models emerging for announcing AI math results. One is OpenAI’s: post the AI’s proofs as they are. The other is Anthropic’s. Virginia Williams and Josh Alman improved algorithms for 3SUM and All-Pairs Shortest Paths with a key idea from an Anthropic model, and Anthropic paid them to write and announce a digested version rather than posting the raw output. Aaronson says both have strengths and weaknesses: the first sets off a race among humans to decode messy proofs, and the second lets a company pick which mathematicians get to present the AI’s work.
Around the same time, 3Blue1Brown’s video “There’s never been a better time to go into math” reached 541 points on HN. The title alone sets the opposite mood. I have not covered the video’s content here.
The same questions for code
As I see it, this has the same shape as software development now that AI writes code. The Lean kernel’s check corresponds to tests and type checks. Auditing whether a statement means what we intend is code review, where a person reads the spec. And Tao’s follow-up activity corresponds to keeping people who understand the code on the team.
Start with checks a machine can run. Tests, types, formal verification: checks that run without a person.
Have a person look at what those checks actually check. If a test guards the wrong spec, a green build means nothing.
Keep someone who can explain it. Without anyone to explain a result, the next person cannot build on it.
When 722 manuscripts landed at once, checking and understanding could no longer keep pace with generation. In math and in code alike, closing that gap is the work ahead.
Sources (numbers as of October 19, 2026)
OpenAI, Sharing AI progress in mathematics · 1,363 points on HN
Dan Roberts, post on X · 1,804 likes · 544K views · 381 points on HN
Thomas Hales, What mathematicians should know about the Lean Theorem Prover · 208 points on HN
Derek Thompson, I know why the mathematicians weep · 397 points on HN
3Blue1Brown, There’s never been a better time to go into math · 541 points on HN