Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866918534655770624 |
|---|---|
| author | Coquand, Thierry |
| author_facet | Coquand, Thierry |
| contents | We report an experiment in autoformalisation of Gödel's second incompleteness
theorem in Agda using Claude. The theorem is formalised for Church's Basic Recursive
Arithmetic (BRA), following the proof outline given in Guard's 1963 lecture notes. The
entire Agda development, comprising approximately 50,000 lines and containing no
postulates, was produced through interaction with Claude; the author did not write
any Agda code.
Beyond the formalisation itself, the project provides a case study of the strengths
and limitations of current large language models in mathematics. An initial
autonomous attempt based on a theorem of Rose failed because the theorem is false;
the resulting formal development produced by Claude established a statement
superficially resembling Gödel's theorem but mathematically unrelated to it. This
failure was traced to an insufficient specification of the internal provability
predicate, illustrating how an LLM may reason correctly from an incorrect formal
specification.
The final development follows Guard's proof and required the reconstruction of several
implicit mathematical arguments, including the role of the internal numeral-encoding
operation and the
interaction between substitution and numeral closure. The
resulting formalisation clarifies a number of details left implicit in the original
presentation and provides a fully machine-checked proof of Gödel's second
incompleteness theorem for BRA. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2606_01898 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic Coquand, Thierry Logic in Computer Science F.4.1 We report an experiment in autoformalisation of Gödel's second incompleteness theorem in Agda using Claude. The theorem is formalised for Church's Basic Recursive Arithmetic (BRA), following the proof outline given in Guard's 1963 lecture notes. The entire Agda development, comprising approximately 50,000 lines and containing no postulates, was produced through interaction with Claude; the author did not write any Agda code. Beyond the formalisation itself, the project provides a case study of the strengths and limitations of current large language models in mathematics. An initial autonomous attempt based on a theorem of Rose failed because the theorem is false; the resulting formal development produced by Claude established a statement superficially resembling Gödel's theorem but mathematically unrelated to it. This failure was traced to an insufficient specification of the internal provability predicate, illustrating how an LLM may reason correctly from an incorrect formal specification. The final development follows Guard's proof and required the reconstruction of several implicit mathematical arguments, including the role of the internal numeral-encoding operation and the interaction between substitution and numeral closure. The resulting formalisation clarifies a number of details left implicit in the original presentation and provides a fully machine-checked proof of Gödel's second incompleteness theorem for BRA. |
| title | Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2606.01898 |