Three years after 'artificial intelligence' was coined at Dartmouth in 1956, Alan Newell and Herbert Simon predicted digital computers would match human capabilities in mathematics within a decade. They were wrong—by about seventy years—but the deadline keeps getting revived. Now DeepMind has silver medals from the 2024 International Mathematical Olympiad and gold from 2025 sitting in its trophy case, while OpenAI runs the same gauntlet. Silicon Valley's biggest players see mathematics as the purest test of machine reasoning, and they're throwing staggering resources at it: the collective market cap of math AI ventures could fund two hundred PhDs annually for five centuries—roughly the number lost to US graduate program cuts this year alone.
The Formalization Fantasy
The dream of mechanizing mathematical proof goes back further than you'd think. Leibniz dreamed of a 'universal characteristic' that would eliminate ambiguity and let correct answers emerge from calculation. David Hilbert carried this torch into the twentieth century, convinced every mathematical claim could be formalized in symbolic language where error became impossible. Then Kurt Gödel published his incompleteness theorems in 1931. The first assumption—that formal systems can capture all mathematical truth—turned out to be hopeless. But here's the thing: the second held up. You can verify proofs mechanically, syntax checking for validity without caring whether anyone understands what it means. This is where tools like Lean come in. Originally developed for software verification, proof assistants like Coq/Rocq, Mizar, Isabelle, and HOL have matured into a self-sustaining branch of mathematical practice. The Lean community now counts 437 members, while computational number theorist Seewoo Lee curates a list of 170 papers exploring AI and machine learning for mathematical discovery. Thomas Hales launched the Flyspeck project in 2003 to formalize his proof of Kepler's conjecture—a century-old problem about sphere packing—spending eleven years translating 100,000 lines of code into machine-readable syntax. 'This technology cuts the mathematical referees out of the verification process,' Hales told New Scientist. 'Their opinion about the correctness of the proof no longer matters.'
The Syllogism That Falls Apart
Here's where the AI-boomers get sloppy. Their argument runs: they said an AI could never solve Go, but AlphaZero solved Go; Go is a game and mathematics is also a game; therefore AI will 'solve' math. Sounds reasonable until you formalize it and watch the logic collapse. The syllogism never actually asserts that whatever holds for one member of a set holds for all members of that same set—that's not how deduction works, that's just pattern-matching on steroids. Mathematics isn't just another game with different rules waiting to be cracked by better training data.
Understanding as the Irreducible Core
Mathematicians themselves have a hard time explaining why they do what they do. When Stefaan Vaes received Belgium's Francqui Prize, he told Queen Mathilde: 'Omdat wij dit graag doen'—because we like it. Pierre Deligne chose mathematical research after learning 'one could earn one's living by playing.' Fields Medalist William Thurston put it this way: 'It may sound almost circular to say that what mathematicians are accomplishing is to advance human understanding of mathematics.' But that's exactly the point. Yuri Manin, most philosophical mind of the Moscow school, defined it with an epigram: 'A good proof is a proof that makes us wiser.' The philosophers are still arguing over whether machines can understand in any meaningful sense—whether there's even a useful definition of mathematical understanding that isn't circular. Meanwhile, the vast majority of working mathematicians go about their routine and like it, oblivious to the boom-and-doom predictions from both sides. When Silicon Valley's prophets claim they're democratizing knowledge creation while mechanizing reasoning into alienated labor, it's worth remembering: the technology enabling this vision—from Gödel to Lean—derives directly from that very human desire for understanding.
The Bottom Line
The tech industry sees mathematics as the final boss of AI capability benchmarks. But reducing proof to syntax verification isn't the same as advancing human understanding—and no amount of GPU money changes what mathematicians actually do when they 'play.' Silver and gold medals at the IMO don't tell you whether anyone got wiser.