When I began studying machine learning and mathematics in 2013, I quickly came to believe that AI would take over math research: that the great proofs of the future would be written by machines.
This was a contrarian view for a long time. When LLMs came along, they really struggled with math. They could barely do arithmetic. Real progress only began in late 2024, with the advent of reasoning models. Applying more test-time compute allowed the models to carry out mathematical arguments without tripping up.
Earlier this year the endgame came into sight: frontier reasoning models had both (1) intuition good enough to generate useful ideas and (2) reasoning good enough to write a bite-size novel proof. Combined with Lean for formal verification, you could basically run that in a loop and slowly grind your way through proofspace. In May, OpenAI published a proof of the Planar Unit Distance Problem, which fired the starting gun for this new age.1
I had wanted to work on automated theorem proving for a long time, and the time seemed ripe, so I blocked off a few weekends to give it a try.
I noticed that most people active in the space appeared to work on non-formalized mathematics: generating proof text in Markdown or LaTeX, and then formalizing in Lean afterwards. I doubted that the models would be cogent enough to sustain correct arguments of dozens or hundreds of pages without formalization. Therefore, I focused my automated theorem prover on working entirely in Lean.
To that end, I developed a private fork of Lean4. (I found the stable open-source release to be mostly fine for formalizing existing theorems, but lacking for high-efficiency proof search.)
I wrote a custom harness to AI-generate proof strategies and to parallelize approaches and handoffs between many subagents. (The default harnesses of Claude Code/Codex got lost too easily when managing long-running context, and the way they handled that context would easily become too expensive.)
I focused my research on problems in graph theory, which seemed most amenable to automated theorem proving, and built out additional specific tooling, like a metaprogram for generating highly parallelizable C++ programs to search for adversarial counterexamples to direct proof strategies. There were lots of details to get right: my harness managed distributed compute, core utilization, API rate limits, cached internal lemmas and made them highly searchable, and so on. Just managing the massive context/state of an ongoing proof search was a great problem to think about. I had fun! I was proud of the engineering that went into this project.
All of this was to prepare me for the bitter lesson.
Using GPT-5.5, my approach was productive for proving some novel theorems.2 But it was slow. The model would still generate lots of incorrect or incoherent statements, and it would run into walls all the time from a strategy perspective.
When GPT-5.6 Sol came out, efficacy improved meaningfully. The model was much better at generating correct statements and productive proof strategies.3 I generated a few hundred thousand lines of Lean toward trying to resolve the degree-57 Moore graph problem and prove the Hadwiger Conjecture.4 Around then, Levent Alpöge turned up the heat by posting the Jacobian counterexample: a major result, but a brief one -- nobody had begun publishing long novel results yet. Feeling urgency, I really tried, but couldn’t quite get the Hadwiger proof to completion. Every time I approached a powerful reduction, it wouldn’t quite close, and my prover had to pivot strategy.5
Four weeks later, OpenAI ran an unreleased new frontier model against 4,000 major problems, using about 3.5 hours of ChatGPT-Pro-Thinking equivalent compute on average per problem. (Which I read as basically nothing, maybe $100 of compute per problem, tops.) The result was the math repo, claiming hundreds of major results, which included a disproof of Hadwiger. No wonder I couldn’t ever get those reductions to close.
Looking back, there were five things that really impressed me:
The crazy improvement from model to model. Sometimes you have to get up close with a model, using the full extent of its frontier capabilities, in order to really feel the difference. Throwing hard math problems at them was the right test in 2026: the models were capable enough to make progress and fully display their intelligence, but not capable enough for the problems to be easily solved, and so you could see the improvements with each update in perfect resolution.
The extent to which all my clever engineering didn’t matter. It was fun and fulfilling to work on this problem, but the bitter lesson reigns supreme: all your sophisticated work to build special-case solutions on top of a model gets squashed by improvements in the base model, sooner or later. I think I’ve been more bitter-lesson-pilled than most for many years now, and this still struck me in a visceral way.
The suddenness of the change. I expected that we would “slowly” -- over the course of months, maybe a year or two -- move into the AI-math era, major results getting dropped one at a time. I expected there would be a sense of conquest, hope, excitement, collaboration as mathematicians slowly woke up to what had become possible. But instead, the moment we crossed some capabilities threshold, we got divine insights dumped on our front porch by the unromantic truckload.
How short the window of human-AI collaboration was. Many idealists have been imagining an era of human-AI collaboration in the sciences and other fields. But this year we went from the field of mathematics being entirely human-dominated since the beginning of time, to one summer of productive human-AI collaboration (hat-tip to Mr. Alpöge), to being entirely AI-dominated,7 presumably until the end of time.
The fact that all this progress was in non-formalized math! It seems8 that the proofs were generated in plaintext, and then about half of them were formalized afterwards,9 which is mind-blowing to me, because the underlying conceptual work of following these massive, convoluted arguments with finicky notation and high conceptual abstraction is so, so hard. My intuition had been that you had to operate in Lean so you could formalize as you go and prevent the model from drifting off-course. The fact that they can keep these arguments straight, apparently get to a solution without any formalization, and then formalize after the fact is insane to me because of the sheer cognitive difficulty of the task. It actually leads me to believe that the models here are much, much smarter than they seem; the spikiness of this intelligence may still be wildly underrated.
After software engineers, the mathematical community is now the next one to go through the AI-induced stages of grief: shock and denial being the currently dominant emotions.
But what has been lost for them? Before AI, most mathematicians would realistically never expect to prove a major theorem, and they would understand well only a small area of mathematics, with the rest being unfamiliar abstractions. Post-AI, this state of affairs is actually still the same, with the exception that an individual mathematician’s probability of making a major contribution has dropped from slim to zero.
By this standard, the field of mathematics at present gets disentangled into two totally different practices:
Relative to how we’ve historically done mathematics, the field basically becomes one of the humanities — worth studying not for a professional purpose or for the sake of advancing its frontier, but for the inherent virtue of education and pleasure of knowledge. The joy of studying mathematics — learning proofs that were already discovered by someone else — is the same as before, and more accessible yet. 3Blue1Brown remarks, from this perspective, that there has never been a better time to go into mathematics.
As for the discovery of knowledge, the gains ahead seem limitless. We will answer the great questions of our universe — P=NP, the Riemann Hypothesis, every question you can imagine and all those you can’t.10 At its most fundamental level, we will harness the power of the sun and turn it into truth. These prospects are as elegant as they are exhilarating.
Candidly, I had felt a little disappointment that the human-AI collaboration window turned out to be so short. But on reflection, this disappointment came from my competitive streak: I had hoped to prove some novel theorems, to use the tools to do something impressive. But that competitive drive to do something before someone else is ultimately just a game of ego. When AI humbles us and levels the playing field, it forces us to transcend that game of ego and focus on the virtue of understanding. This actually seems11 like a good thing.
As mathematicians, we lose the competition in and privilege of expanding the frontier ourselves. But we gain limitless understanding, and retain the ability to play within the infinite area discovered for us by AI. All things considered, I think this is a good trade. And this same dynamic will soon come to all other disciplines, too. It may feel unnerving for some to adjust to this new reality — that some of the competitive games of old may cease to be — but I am optimistic that this will prove for the better.