Something remarkable happened this week. A human-AI collaboration formally verified Maryna Viazovska’s Fields Medal-winning proof of optimal sphere packing in 8 and 24 dimensions. Math, Inc.’s AI agent Gauss autoformalized the 24-dimensional proof — over 200,000 lines of Lean code — in just two weeks, with no pre-existing blueprint to work from.
This follows a year of milestones that would have seemed like science fiction a decade ago. In July 2025, Google DeepMind’s Gemini Deep Think scored 35 out of 42 on the International Mathematical Olympiad — gold medal performance — solving five of six problems within the standard 4.5-hour time limit, all in natural language, with no human translation into formal systems required. A year earlier, DeepMind’s AlphaProof had achieved silver at the same competition, and notably cracked Problem 6 — the hardest problem, solved by only five of 609 human contestants.
In May 2025, AlphaEvolve discovered a new algorithm for multiplying 4×4 complex-valued matrices using 48 scalar multiplications, breaking Strassen’s 1969 record of 49 — a barrier that had stood for 56 years. In October 2024, Meta’s AI cracked a century-old problem in dynamical systems, discovering Lyapunov functions at ten times the rate of previous state-of-the-art methods. And at Oxford and Sydney, researchers working with DeepMind used machine learning to uncover new connections in knot theory and representation theory, generating conjectures that humans then proved — the first time AI had participated in genuine mathematical discovery of this kind.
Meanwhile, Princeton’s Goedel-Prover-V2 became the strongest open-source theorem prover, capable of self-correcting its own proofs. Terence Tao — perhaps the greatest living mathematician — has been collaborating directly with AlphaEvolve on 67 open problems, and using ChatGPT to formalize proofs in Lean through what he calls “vibe coding,” where the human provides direction and the AI plays code improvisationally while the proof assistant acts as referee.
The evidence is overwhelming. AI is not approaching the frontier of mathematics. It has arrived.
Now comes the question everyone wants to argue about: is this a good thing? And is it valid science?
I think the answer to both is unambiguously yes. But to see why, you have to understand what’s actually shifting.
For centuries, mathematics has fused two distinct capabilities in the figure of the “great mathematician”: the capacity for deep structural intuition — seeing patterns, sensing what should be true, feeling the shape of a solution before you can articulate it — and the capacity for rigorous formal manipulation, the painstaking construction of proofs, the mechanical grinding through of derivations and verifications.
These two capabilities are very different cognitive activities. And historically, you had to possess both to contribute at the frontier. If you could see the truth but couldn’t prove it, you were an amateur. If you could prove things but had no intuition for what to prove, you were a technician. The rare individuals who had both in abundance — the Ramanujans, the Grothendiecks, the Taos — were the ones who moved the field forward.
What AI is doing is decoupling these two activities. The formal manipulation — the proof construction, the verification, the exhaustive case analysis — is increasingly something machines can do. And they can do it faster, with fewer errors, and at a scale no human can match. AlphaProof doesn’t hallucinate proofs; it operates in Lean, where every step is formally verified. There is no ambiguity about whether its output is correct. It either compiles, or it doesn’t.
This means the bottleneck shifts. The scarce resource is no longer the ability to grind through proofs. It’s the ability to know which proofs are worth grinding through. It’s intuition. It’s taste. It’s the capacity to look at the vast landscape of mathematical possibility and say: there — that’s where something interesting is hiding.
Consider what Tao himself said about the AlphaEvolve collaboration: AI excels at exhaustive exploration of defined solution spaces. It struggles with conceptual breakthroughs. It’s best used in partnership with human insight, not as a replacement for it. He describes a future where AI first performs a low-quality survey of millions of problems, generating a preliminary map of the landscape, and then human mathematicians use that map to direct their resources toward the most promising directions.
This is not a vision of humans being replaced. It’s a vision of humans being amplified. The mathematician becomes less like a solitary craftsman and more like a navigator — someone who reads the terrain, senses where the currents flow, and steers the ship, while AI handles the engine room.
And this, I believe, has a profound implication for who gets to participate at the frontier.
Traditional mathematics has been, bluntly, a gatekeeper’s paradise. You needed years of formal training. You needed the right academic credentials. You needed to be the kind of person who could hold immense chains of symbolic reasoning in your head. If your strength was in seeing connections across domains, in intuiting deep structural relationships, in sensing what should be true from the physics or the philosophy or the computational patterns — but you couldn’t produce publication-ready proofs on demand — the frontier was closed to you.
AI changes this. Not by lowering the bar, but by changing what the bar measures.
If a theorem prover can verify your conjecture in Lean, the conjecture is verified. It doesn’t matter whether you proved it by hand in your study over seven years, like Andrew Wiles, or whether you intuited it from patterns in cellular automata and then pointed an AI at the formal verification. The mathematical truth is the same. The proof is the same. The verification is the same.
What differs is the path. And the path is where the human contribution lives.
I speak from experience here. My own work on the mathematics of self-referential systems has always been driven by structural intuition — sensing how reflexive principles should connect physics, logic, computation, and thermodynamics. The formal validation has been a separate step, and an increasingly automatable one. In this new landscape, that’s not a weakness. It’s the whole point. The value was never in the calculation. It was in knowing what to calculate, and why.
There is a legitimate concern worth addressing: can humans really understand the results of increasingly complex AI-generated derivations? When Lean verifies a proof that spans 200,000 lines of code, as in the Viazovska formalization, can any human hold that in their head?
Maybe not initially. But this is not a new problem. No single human understood every line of the proof of the four-color theorem when it was first verified by computer in 1976. No single human holds the entirety of the classification of finite simple groups — a proof that spans tens of thousands of pages across hundreds of papers — in their mind. Mathematics has been pushing past the limits of individual human comprehension for decades. What we have instead is trust in the verification process, and the ability to study the results at whatever level of abstraction is useful.
And here, AI helps twice. It not only generates and verifies the proofs; it can also explain them. Large language models are already being used as tutors and explainers, translating formal proofs back into natural language, highlighting the key insights, identifying the critical steps where the interesting mathematics happens. The same technology that makes proofs possible at superhuman scale can make them comprehensible at human scale.
We are at an inflection point. The Quanta Magazine piece published this past year put it beautifully: mathematicians will continue to be the architects of new mathematical cathedrals, but they’ll no longer need to be the construction crew as well, crafting every brick and nail. And as Tao envisions, large theorems may soon be proved by a combination of twenty people and a fleet of AIs, each contributing different pieces, connected and verified through formal systems that guarantee correctness regardless of who — or what — produced each step.
This is not the end of human mathematics. It’s the beginning of a new kind of mathematics — one that values vision over computation, navigation over calculation, and intuition over mechanical skill. The frontier hasn’t moved away from humans. It has moved deeper into what makes us human.
The age of the genius calculator is giving way to the age of the genius navigator. And I, for one, am ready to sail.