100 years ago, the world of mathematics experienced a foundational crisis: the identification of several paradoxes revealed cracks in the pillars supporting all areas of math. The most famous of which is Russel’s paradox, which points to the contradictory “set of all sets that do not contain themselves”, thereby showing the inconsistency of naive set theory. This had spurred mathematicians to search for a rigorous foundation for math without contradictions. In particular, David Hilbert initiated a program to design a system of axioms that are complete and consistent, meaning one should be able to derive all mathematical truth from the axioms, while avoiding paradoxes—“the truth, the whole truth, and nothing but the truth”. Such a goal was natural for mathematicians, as it would place their work on firmer grounds. It was therefore also a seismic event when Gödel dealt the death blow to Hilbert’s program with his incompleteness theorems: such a complete, consistent system for math cannot exist!

Although such an impossibility result ought to further deepen the existential crisis, mathematicians soon recovered and carried on: improvements to naive set theory, such as Russel’s theory of types, were proposed; and while such systems still cannot be formally proven to be consistent due to Gödel’s results, they are largely believed to be consistent, and it turned out the foundational cracks have had little effects on the kind of math people care about. In fact, type theory has grown so mature that it forms the basis of interactive theorem provers like Lean, making it possible to formalize a growing portion of math in computer languages, so that proofs can be automatically checked by programs from the ground up.

Besides the axiomatic system, Hilbert also proposed a related goal in his program: the development of an algorithm to automatically decide the truth of any mathematical statement, thereby reducing theorem proving to the mechanical application of rules. This goal was also shown to be impossible by Alan Turing, in his landmark proof of the undecidability of the Halting problem which gave birth to the fertile field of computer science. It’s rather a poetic contradiction that, in establishing the impossibility of Hilbert’s program, Gödel and Turing created the most powerful computing machines that can.

A century has passed since the times of Hilbert, Gödel and Turing. Against all odds, we are now witnessing the realization of Hilbert’s “proof machine” incarnated as AI agents armed with mechanized formal systems found in proof assistants like Lean. This development, as it turned out, has had a far more devastating effect on the mathematical community compared to the fall of Hilbert’s program. I am not sure if Hilbert himself had considered the consequences had his program succeeded, but von Neumann showed incredible prescience:

When undecidability fails, then mathematics as it is understood today ceases to exist; in its place there would be an absolutely mechanical prescription with whose help one could decide whether any given sentence is provable or not.

I am not a mathematician, but a computer scientist. In computing, the impact of AI has been less violent, with the majority even cheering it on, churning out code at an ever-increasing speed. What I sense, though, is an air of abandonment: it is now becoming standard practice to stop reading AI-generated code. This is a great tragedy for computer science. We are one of the very few disciplines where it is possible to get to the very bottom of things—we can understand exactly what a program does as long as we have its source code, yet we are now giving this up! We now have machines that can do everything Hilbert dreamed of, but we have abandoned what he considered the very soul of science:

We must not believe those, who today, with philosophical bearing and deliberative tone, prophesy the fall of culture and accept the ignorabimus. For us there is no ignorabimus, and in my opinion none whatever in natural science. In opposition to the foolish ignorabimus our slogan shall be Wir müssen wissen – wir werden wissen ("We must know – we will know").

As computer scientists, we should consider what’s happening in math: refusing to read the code for a program that passes all tests—even formal verification—is akin to ignoring the proof as soon as AI solves a theorem in Lean. In fact, they are the same in the literal sense, as a program is a proof via the Church-Howard correspondence, and that is exactly how theorem provers like Lean operate. When an AI generated proof is too long to read, mathematicians don’t give up understanding it, but take great pains to simplify the proof until it’s digestible. We must take the same attitude in computing: use abstractions, refactor, refine scope, invent and adopt higher-level languages, until we can hold the code in our head.

I don’t know if AI will eventually exceed humans at all activities—I believe we think with our brains which are just biological computers with a different architecture—but I know we will end up badly if we give up thinking to the machines. Consider the growing cases where people lose their lives by relying on AI for medical advice: the more we take the machine’s words for granted, the less we are in control of our own destiny. We must know – we will know.