Summary
Gödel's incompleteness theorems show fundamental limits in mathematical systems, but checking these proofs by hand is complex. The authors used a computer tool called Lean 4 to create fully verified digital versions of these theorems and related results in provability logic. This mechanization ensures the proofs are free of errors and can be reused in future formal reasoning. Their work also covers Solovay's theorem which links logic and arithmetic in a precise way.
What this means in practice
- •For formal methods engineers: Use verified formal proofs in Lean to build more reliable automated reasoning and verification tools for software and hardware correctness.
- •For programming language designers: Integrate mechanized logic results to guide design of proof assistants and logic-based language features ensuring soundness.
Authors
Shogo Saitou, Mashu Noguchi
Abstract
We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prover.