Papers With

← All papers
First page of Mechanizing Gödel's Incompleteness Theorems and Provability Logic

Mechanizing Gödel's Incompleteness Theorems and Provability Logic

Shogo Saitou, Mashu Noguchi

cs.LO Sep 12, 2026 · v2 math.LO
formalization logic
Read PDF arXiv abstract Code
TL;DR
Mechanizes Gödel's first and second incompleteness theorems and Solovay's arithmetical completeness of GL in Lean 4.
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.
Problem

Gödel's incompleteness theorems and provability logic (GL) are foundational metamathematical results that had not been fully mechanized in Lean 4.

Approach

The authors formalize the first and second incompleteness theorems in the Lean 4 theorem prover. They also mechanize Solovay's arithmetical completeness theorem for the modal logic GL and related provability-logic results.

Results

Machine-checked proofs of Gödel's first and second incompleteness theorems and Solovay's arithmetical completeness theorem for GL were produced in Lean 4.