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, 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 paper of Rose failed because of a false Lemma; 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 specification of substitution. 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 Basic Recursive Arithmetic.

翻译：我们报告了一项在Agda中使用Claude自动形式化哥德尔第二不完备定理的实验。该定理针对丘奇基本递归算术进行形式化，遵循Guard 1963年讲义中给出的证明大纲。整个Agda开发工作包含约50,000行代码，且不含任何公设，是通过与Claude交互生成的；作者未编写任何Agda代码。除形式化本身外，该项目为当前大语言模型在数学中的优势与局限提供了案例研究。基于Rose论文的首次自主尝试因错误引理而失败；Claude生成的形式化开发结果表面类似于哥德尔定理，但在数学上与之无关。该失败可追溯至内部可证谓词规范不足，说明大语言模型如何从错误的形式规范中正确推理。最终开发遵循Guard的证明，需要重构若干隐含的数学论证，包括内部数字编码运算的作用以及替换的规范。所得形式化澄清了原始表述中若干隐含细节，并为基本递归算术中的哥德尔第二不完备定理提供了完全机器可检验的证明。