100 years ago, the world of mathematics experienced a foundational\ncrisis: the identification of several paradoxes revealed cracks in the\npillars supporting all areas of math. The most famous of which is\nRussel’s paradox, which points to the contradictory “set of all sets\nthat do not contain themselves”, thereby showing the inconsistency of\nnaive set theory. This had spurred mathematicians to search for a\nrigorous foundation for math without contradictions. In particular,\nDavid Hilbert initiated a program to design a system of axioms that are\ncomplete and consistent, meaning one should be able to derive all\nmathematical truth from the axioms, while avoiding paradoxes—“the truth,\nthe whole truth, and nothing but the truth”. Such a goal was natural for\nmathematicians, as it would place their work on firmer grounds. It was\ntherefore also a seismic event when Gödel dealt the death blow to\nHilbert’s program with his incompleteness theorems: such a complete,\nconsistent system for math cannot exist!
\nAlthough such an impossibility result ought to further deepen the\nexistential crisis, mathematicians soon recovered and carried on:\nimprovements to naive set theory, such as Russel’s theory of types, were\nproposed; and while such systems still cannot be formally proven to be\nconsistent due to Gödel’s results, they are largely believed to be\nconsistent, and it turned out the foundational cracks have had little\neffects on the kind of math people care about. In fact, type theory has\ngrown so mature that it forms the basis of interactive theorem provers\nlike Lean, making it possible to formalize a growing portion of math in\ncomputer languages, so that proofs can be automatically checked by\nprograms from the ground up.
\nBesides the axiomatic system, Hilbert also proposed a related goal in\nhis program: the development of an algorithm to automatically decide the\ntruth of any mathematical statement, thereby reducing theorem proving to\nthe mechanical application of rules. This goal was also shown to be\nimpossible by Alan Turing, in his landmark proof of the undecidability\nof the Halting problem which gave birth to the fertile field of computer\nscience. It’s rather a poetic contradiction that, in establishing the\nimpossibility of Hilbert’s program, Gödel and Turing created\nthe most powerful computing machines that can.
\nA century has passed since the times of Hilbert, Gödel and Turing.\nAgainst all odds, we are now witnessing the realization of Hilbert’s\n“proof machine” incarnated as AI agents armed with mechanized formal\nsystems found in proof assistants like Lean. This development, as it\nturned out, has had a far more devastating effect on the mathematical\ncommunity compared to the fall of Hilbert’s program. I am not sure if\nHilbert himself had considered the consequences had his program\nsucceeded, but von Neumann showed incredible prescience1:
\n\nWhen undecidability fails, then mathematics as it is understood today\nceases to exist; in its place there would be an absolutely mechanical\nprescription with whose help one could decide whether any given sentence\nis provable or not.
I am not a mathematician, but a computer scientist. In computing, the\nimpact of AI has been less violent, with the majority even cheering it\non, churning out code at an ever-increasing speed. What I sense, though,\nis an air of abandonment: it is now becoming standard practice to stop\nreading AI-generated code. This is a great tragedy for computer science.\nWe are one of the very few disciplines where it is possible to get to\nthe very bottom of things—we can understand exactly what a program does\nas long as we have its source code, yet we are now giving this up! We\nnow have machines that can do everything Hilbert dreamed of, but we have\nabandoned what he considered the very soul of science:
\n\nWe must not believe those, who today, with philosophical bearing and\ndeliberative tone, prophesy the fall of culture and accept the\nignorabimus. For us there is no ignorabimus, and in my\nopinion none whatever in natural science. In opposition to the foolish\nignorabimus our slogan shall be *Wir müssen wissen – wir werden\nwissen* ("We must know – we will know").
As computer scientists, we should consider what’s happening in math:\nrefusing to read the code for a program that passes all tests—even\nformal verification—is akin to ignoring the proof as soon as AI solves a\ntheorem in Lean. In fact, they are the same in the literal sense, as a\nprogram is a proof via the Church-Howard correspondence, and that is\nexactly how theorem provers like Lean operate. When an AI generated\nproof is too long to read, mathematicians don’t give up understanding\nit, but take great pains to simplify the proof until it’s digestible. We\nmust take the same attitude in computing: use abstractions, refactor,\nrefine scope, invent and adopt higher-level languages, until we can hold\nthe code in our head.
\nI don’t know if AI will eventually exceed humans at all activities—I\nbelieve we think with our brains which are just biological computers\nwith a different architecture—but I know we will end up badly if we give\nup thinking to the machines. Consider the growing cases where people\nlose their lives by relying on AI for medical advice: the more we take\nthe machine’s words for granted, the less we are in control of our own\ndestiny. We must know – we will know.
\n[*Zur
Hilbertschen Beweistheorie*](https://eudml.org/doc/167910), translation found in the Turing Centenary\n Lecture by Philip Welch.↩︎