Wir müssen wissen – wir werden wissen

A century after David Hilbert proposed his program for a complete, consistent axiomatic foundation for mathematics, AI agents paired with formal proof assistants such as Lean are realizing his vision of a "proof machine," a development the article argues is disrupting the mathematical community more profoundly than the program's original collapse. The piece recounts how Russell's paradox exposed inconsistencies in naive set theory, triggering a foundational crisis, and how Kurt Gödel's incompleteness theorems and Alan Turing's proof of the undecidability of the Halting problem later showed that both Hilbert's axiomatic and algorithmic goals were impossible. Despite these impossibility results, mathematicians moved on to systems like Russell's type theory, which matured into the basis for interactive theorem provers that let computers verify proofs automatically. The article notes the irony that Gödel and Turing, in proving Hilbert's program unachievable, laid the groundwork for the computing machines now fulfilling it. It cites John von Neumann's warning that if undecidability fails, "mathematics as it is understood today ceases to exist." What to watch: whether AI-driven formalization of mathematics accelerates and how mathematicians adapt as machine-verified proofs become more widespread.