AI theorem provers and the Foundations of Mathematics

The mathematics community is in the grip of an existential crisis. After the wave of AI announcements in September and October of 2026, most notably the AI-generated counterexamples to long-standing problems like the Jacobian Conjecture (to me) and others, mathematicians have rushed to redefine their profession. Turn to almost any major mathematics blog and you will find the same thing: an urgent, somewhat insecure attempt to justify the human mathematician to the rest of the human race, dressed up as philosophy.

Amid the panic, one irony is being overlooked. The best defense of mathematics against the supposed threat of AI is a simple historical fact: computer science and AI theorem provers are direct descendants of mathematical logic. AI did not emerge from a vacuum. It grew out of the foundations of mathematics. I was recently reading Thomas Hales’s guest post on Terence Tao’s blog about the Lean theorem prover, its reliability, and the role of AI. It is an excellent and informative piece. Hales did not set out to make my point, but the historical footprints are all over his commentary. In discussing formal verification, he invokes Russell’s paradox (1901), Zermelo–Fraenkel set theory (ZFC), and Gödel’s incompleteness theorems (1931), the old bedrock of the Foundations of Mathematics, a field devoted to logic and set theory.

So what happened to those foundations?

By the time I entered college in the 1970s, mainstream mathematics had made up its mind. Foundations had been demoted to “old-fashioned,” a stagnant backwater of eccentric holdouts. As students, we were practically trained to laugh at anyone who specialized in it. I remember hearing of Ashvini Kumar at IIT Kanpur, who rejected proofs by induction, and of others who refused contrapositive arguments. The consensus was that these people were contrarians, perhaps even a little crazy.

Mainstream mathematics abandoned its foundations to board a train to infinity, a soaring journey into specialized, abstract realms that the rest of the human race ultimately missed. (In my observation, this often goes with painful and artificial attempt to give “geometric interpretations” and connections.) That train is unlikely to return.  The human race is never going to catch up with the advances of mathematics, that even the human mathematicians themselves can barely appreciate. 

It is a bare historical fact that when pure mathematics stepped off the platform of foundational logic, computer science stepped on. Theoretical computer science picked up the tools mathematicians had discarded as relics of the early twentieth century. Looking back, the boundary between theoretical computer science and pure (foundational) mathematics is artificial. As Hales notes, milestones such as Werner’s 1997 paper on “Sets in Types, Types in Sets”, showed that the line had blurred decades ago.

I know this pattern of an establishment abandoning its roots well from my own field. My early research was in classical algebraic K-theory and projective modules, and it later moved toward Quillen K-theory, which I now call Arrowtic K-theory because arrows are its atomic building blocks. Like the logicians of the 1970s, I have been told by the reigning experts that Quillen K-theory is “old-fashioned” and that nobody works on it anymore. The modern establishment has moved on to motivic homotopy theory and motivic cohomology, claiming the K-theory label while practicing what is fundamentally homotopy theory. I won’t claim to have been wiser, but my philosophy has long been simple: we do algebra without apology. I refrained from struggling to find painful geometric connections, in my work. Arrowtic K-theory is an explicit attempt to keep algebraic K-theory within the concrete foundation of Quillen K-theory, and to keep structural rigor from being erased by shifting academic trends (some of which is ad-hoc).

The AI tsunami now hitting mathematics is not a foreign invasion. It is the revenge of the foundations. Proof assistants like Lean, which are changing how we verify theorems, are built on the logic, type theory, and foundational frameworks that mainstream mathematics abandoned half a century ago. Computer science took our “old-fashioned” ideas, gave them technological life, and built a mirror that now forces the mathematical establishment to look at its own worth.

As a self-described observer of these shifts, I find the unfolding drama a pleasure to watch. If the establishment wants to survive its identity crisis, it need not reinvent its purpose or draft panicked justifications for the public. It simply needs to take credit for the vindication of the invincibility and rigor of the Foundations of Mathematics, without apology.