Cristian S. Calude
Gödel Incompleteness and Proof Assistants
Gödel’s first incompleteness theorem states that in every consistent system of axioms which contains a modicum of arithmetic and its theorems can be listed by an algorithm, there exist true statements about natural numbers that are unprovable in the system. The second incompleteness theorem states that such a system cannot demonstrate its own consistency. J. von Neumann called them “a landmark which will remain visible far in space and time.”
The talk will briefly show that both incompleteness results follow from the undecidability of the Halting problem. Then we will discuss theoretically whether the incompleteness results give a “coup de grâce” to Hilbert’s Programme. Finally, we will argue that the current practice of mathematics, which uses extensively proof-assistants, is changing the theoretical views about the impact of incompleteness.