An Exciting Time to Be a Mathematician

The kid Scarciotti is worried about

In his latest video, titled “You Truly Don’t Understand What Just Happened to Mathematics,” Prof. Giordano Scarciotti of Imperial College London worries that AI will convince a gifted 17-year-old to give up on mathematics. A few years ago, I was that kid.

When I started college in the United States, freshmen kept asking each other the same question: “Did you play any sports in high school?” Sports culture back home in Vietnam was much smaller than in the US, so I named the sports I played for fun with friends during recess. Looking back, my sport was mathematics. I fell in love with math in my early years of school, and my teachers pushed me into olympiad after olympiad through middle and high school. I won medals in several national and international competitions, and my proudest results were two finishes in the top 20 among Vietnam’s entrants at the Australian Intermediate Mathematics Olympiad and two golds at the HAC Maths Olympiad. I went on to study Computer Science and Mathematics at Gettysburg College.

So when OpenAI released hundreds of AI-written proofs on October 6 and the internet ran with the name “Mathocalypse,” the question felt personal. I think this is the most exciting time to be a mathematician in my lifetime.

What happened

On October 6, 2026, OpenAI published about 720 manuscripts, grouped into 372 results, from an unreleased internal model. The company says it posed roughly 4,000 problems, and that each result used, on average, about as much computing as three hours of ChatGPT Pro thinking. The set includes claimed progress on the Unique Games Conjecture and several Erdős problems. Part of it comes with Lean formalizations, and the rest are informal write-ups. A month earlier, on September 8, OpenAI had separately claimed a proof that a forced version of the Navier-Stokes equations, the subject of a Millennium Prize problem, can blow up in finite time.

The next day, OpenAI withdrew three manuscripts over a sign error and revised 14 more. Scott Aaronson titled his blog post on the release “The Mathocalypse,” and the name spread.

The proofs are also hard to read. Dana Moshkovitz, who spent years on the Unique Games problem, said she could only read OpenAI’s Unique Games paper with AI help. Aaronson wrote that almost none of the proofs had been understood by a human yet. Harvard’s Melanie Wood made the same point.

Euler called it barely math

In 1736, Leonhard Euler took on a puzzle: could someone walk through Königsberg crossing each of its seven bridges exactly once? He turned each landmass into a point and each bridge into a line, then showed the walk was impossible. In a letter that April, he wrote that the solution had little to do with mathematics.

That small puzzle founded graph theory. Gustav Kirchhoff used graph ideas to analyze electrical circuits in 1847. Edsger Dijkstra designed his shortest-path algorithm in 1956, about 220 years after Euler, and it now runs underneath GPS navigation and internet routing. Every CS student also knows it as the algorithm they traced by hand at 2 a.m. before the algorithms final, which is its own shortest path to suffering. Sergey Brin and Larry Page built PageRank on graph structure in 1998. Euler saw none of it.

Scarciotti makes this point too, that the value of mathematics lives in the exploration that produces fields like graph theory. I agree with him there. We part ways on what AI does to that exploration. I think it hands every mathematician more bridges to think about.

We have been here before

In 1976, Kenneth Appel and Wolfgang Haken proved the four color theorem by having a computer check 1,834 cases. No human could verify the whole argument by hand, and mathematicians argued over whether it counted as a proof at all.

Then people went to work. A 1981 thesis reported an error in part of the argument, and Appel and Haken published corrections in 1989. In 1997, Robertson, Sanders, Seymour, and Thomas produced a simpler computer proof with 633 cases. In 2005, Georges Gonthier and Benjamin Werner formalized the entire proof in the Coq proof assistant.

From the first proof to full trust took 29 years, and humans did the work at every step: checking, simplifying, formalizing. The Mathocalypse is the same story at a much larger scale. Seven hundred manuscripts means years of that work, and it starts now.

That work has already started on OpenAI’s release. Mathematicians quoted by Quanta largely believe its quasi-Riemann result is correct, and Princeton’s Peter Sarnak still won’t call it a theorem until humans check every detail. OpenAI has acknowledged that its Navier-Stokes Lean proof and its written proof differ, and EPFL’s Gonzalo Cao-Labora says the two follow different approaches. Formalization keeps catching errors in human work too. Axiom Math reports that while its agents formalized the Classification of Finite Simple Groups in Lean, they found 34 deviations from the published record, including a counterexample to a lemma.

175018001850190019502000

1. Euler solves the bridgesEuler shows no walk crosses all seven Königsberg bridges exactly once, and calls the solution barely math.: 1736
2. Kirchhoff's circuit lawsKirchhoff uses graph ideas to analyze electrical circuits.: 1847
3. Dijkstra's shortest pathsDijkstra designs the shortest-path algorithm now under GPS navigation and internet routing.: 1956
4. Four color proof by computerAppel and Haken prove the four color theorem by having a computer check 1,834 cases.: 1976
5. PageRankBrin and Page build PageRank on the web's link graph.: 1998
6. Four color proof in CoqGonthier and Werner formalize the whole four color proof in the Coq proof assistant.: 2005
7. OpenAI's 720 manuscriptsOpenAI publishes about 720 manuscripts from an unreleased model, grouped into 372 results.: 2026

People carried every milestone before 2026, often decades apart. The 2026 release is the next one they will have to carry.

The new mathematician

I believe mathematics will be disrupted the way software engineering already has been. A few years ago, headlines predicted that AI would replace every software engineer. That has not happened. The roles changed. Engineers now spend less time typing code and more time designing systems, reviewing AI output, and deciding what to build.

New jobs also grew out of software engineering. Forward deployed engineering, once a niche role at Palantir, has spread across AI companies, with engineers embedded at customers to build AI into their workflows. AI engineers design the pipelines, agents, and evaluations around large models. Product managers, analysts, and designers now prototype with code, so roles that used to be nontechnical are becoming technical. Mathematics is heading into the same shift. The mathematician’s job will change, new roles will grow out of it, and they start with these skills:

• Building harnesses. Someone has to design the environment an agent works in. What it may try, how it records progress, and when it stops.
• Orchestrating agents. Proofs can come from several agents that explore, critique, and referee each other. Designing that collaboration is a research problem in its own right. On the First Proof benchmark of unpublished research problems, an ETH Zurich harness that coordinates several models solved 9 of 10 for $1,888. A single frontier model working alone solved 7 of 10 for $36. Knowing when two extra problems are worth the extra cost is part of the skill.
• Spending compute wisely. OpenAI reportedly spent millions of dollars in compute and ran about 10,000 agents on its claimed Navier-Stokes result. No university department has that budget. Choosing the right model and settings, and getting the most from a small budget, becomes a core skill.
• Translating proofs. A proof creates value once humans understand it, teach it, and apply it. Turning a machine proof into ideas people can use is real mathematical work.
• Verifying. A machine-checked proof is only as good as the statement it checks. Someone has to confirm that statement says what we mean.

I have lived a small version of this. My senior capstone at Gettysburg was on Chomp, a game where two players take turns biting squares off a chocolate bar and whoever eats the poisoned corner loses. I spent the semester on three-row Chomp, where Byrnes proved that the winning positions eventually repeat in a periodic pattern, and I wanted to know how long “eventually” is. His proof shows that the pattern must start repeating, but it gives no way to compute when it starts. The semester ended before I could solve it, and that frustration stayed with me. I wanted to keep going, so I built an agent harness to keep attacking the problem. It runs two independent explorer islands, a referee that judges arguments with their authorship stripped away, an append-only ledger of results, and a hard budget cap. The agents are tireless. They have made about 5,300 model calls on roughly $34 of a $45 budget, logged more than 400 entries, and pushed nine claims through the referee. My own judgment still mattered at every step. The first result to pass the referee was correct, and it had also been in print since 2005, one line after the recurrence it came from. The referee once rejected a correct argument by quoting a sentence that did not exist. The agents could check whether a proof was right, but deciding whether it was new, and whether a rejection was fair, was still my job.

The result I am proudest of is an explicit answer to my capstone question. For a board whose top row has r squares, the pattern must start repeating by the time the middle row is about 2^(r²/2) squares long. It is a huge number and a modest result. A later proof by Doron Zeilberger implied that such a bound exists without ever stating it, and the harness turned his argument into a formula. Still, it is the first time I have seen that number written down anywhere, and I would not have found it alone in a semester.

Verification stays human work too. A Lean proof checker confirms the logic, and the statement it checks still has to capture the problem we care about. A recent paper by Bastounis, Circelli, and Hansen reports exactly this kind of mismatch between OpenAI’s Navier-Stokes proof and its Lean version. Picture a result that feeds into the design of a new aircraft. Someone has to stand behind its safety, and that someone is a mathematician who understands the proof.

So the mathematician’s daily work moves from solving toward understanding, verifying, teaching, and applying. The joy of solving stays with anyone who keeps trying.

The ethics we are missing

No rule says how an AI lab should release a solution to an open problem. Ethics should guide it anyway, and OpenAI’s release shows why.

In September, mathematician Dor Minzer heard by text message that OpenAI was closing in on the Unique Games Conjecture. Quanta Magazine reports that his team raced to finish their own proof before an OpenAI press release could overshadow years of their work. Princeton’s Mark Braverman said math by press release is unhealthy for the field. OpenAI’s Navier-Stokes claim produced a public dispute over credit with NYU’s Tristan Buckmaster, and the two sides still tell different stories.

The race has only sped up. On October 26, OpenAI and Anthropic reportedly posted claimed refutations of the Exponential Time Hypothesis, a central conjecture in computer science, about six hours apart. Ryan Williams, who is helping coordinate the review, calls it a “claimed refutation.” When two labs race to announce the same result within hours, the announcement comes first and the checking comes later.

Mathematicians are starting to propose new norms. In a guest post on Terence Tao’s blog, Buckmaster argues that credit should follow understanding. Northwestern’s Bryna Kra has proposed that journals credit discovery, proof, formalization, and explanation separately. Oxford’s Andras Juhasz suggests listing an AI model as an author when its contribution is substantial, with at least one human author who stays accountable. None of these proposals yet asks a lab to contact researchers before announcing, and that is the gap I want to see filled.

Someone who has spent a career on a problem deserves to hear about its solution before the press does. That courtesy costs a lab one email. The Leiden Declaration, endorsed by the International Mathematical Union this June, already asks for disclosure of AI use and precise credit to prior work. Legally, OpenAI owes no one anything here, and a lab can argue it is free to publish whatever its models find. I see this as a question of ethics. A lab that solves a problem someone has spent their life on has two respectful choices: contact that researcher and discuss the results before announcing, or keep the result unpublished. Publishing first and letting them find out from the news treats a life’s work as a benchmark.

An exciting time to be a mathematician

Euler thought his bridge puzzle was barely mathematics, and it gave us GPS. OpenAI’s release holds hundreds of results nobody fully understands yet. Understanding them, checking them, teaching them, and turning them into things people use will take a generation of mathematicians.

That future asks a lot of everyone involved, starting in the classroom. AI can now do a student’s homework, and the skill and the joy of mathematics come only to students who do the work themselves. That part is on each of us. Juhasz has also proposed limiting graded work to supervised written and oral exams, and I expect more departments to take that step.

The profession faces real pressure too. In an August survey of MIT math graduate students, about three in four of the 45 respondents worried that AI will make tenure-track jobs harder to get, and 71% said their chances of staying in academic math had declined. If universities and funders start measuring mathematicians by proofs completed, the job could shrink into proofreading AI output. Whether this work turns bleak or rich depends on what institutions choose to reward, and mathematicians still shape those incentives inside academia. Some of those students will find the new roles I described earlier: building harnesses, verifying statements, and translating proofs. The work itself can be rich. Reading a machine proof until you understand it, connecting it to what is already known, and explaining it to others is some of the most creative work the field will offer.

So I still believe this is an exciting time to be a mathematician. It is also a demanding one. It asks AI labs to release results with care, teachers to protect the struggle that builds understanding, and institutions to reward the people who understand the mathematics.

That work is what I want to build my career around. Right now I do it as an AI engineer, building tools that make machine reasoning something humans can read, trust, and build on. Someday I hope to carry that work into AI research as well.

To the 17-year-old wondering whether math still has a future, it does, and it needs you.

If you work in mathematics, I would love to hear how your work is changing.

Sources

• OpenAI: Sharing AI progress in mathematics
• openai/math repository
• Scott Aaronson, The Mathocalypse
• TechCrunch on field standards
• Retraction Watch on withdrawn manuscripts
• Quanta on the Unique Games race
• OpenAI Navier-Stokes announcement
• Bastounis, Circelli, and Hansen on the Navier-Stokes Lean proof (arXiv:2610.08144)
• Quanta on the quasi-Riemann result
• Startup Fortune on the Navier-Stokes Lean mismatch
• The Decoder on Cao-Labora and the Navier-Stokes proof
• Axiom Math on formalizing the finite simple groups
• TechTimes on the First Proof benchmark
• Lilting on the Exponential Time Hypothesis claims
• Buckmaster guest post on Terence Tao’s blog
• Proofs and Prompts essay citing Kra’s credit proposal
• Juhasz on AI, credit, and education
• Boston Globe on the MIT survey
• Decrypt on the Buckmaster dispute
• Leiden Declaration
• Euler’s letters (USP)
• Four color theorem
• Chalkdust on Dijkstra
• Prof Gio YouTube channel