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 prescience1:
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.
[*Zur
Hilbertschen Beweistheorie*](https://eudml.org/doc/167910), translation found in the Turing Centenary
Lecture by Philip Welch.↩︎