Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic

あなたは、自分自身の数学の宿題を検証できる、完璧で自己点検機能を持つロボットを作ろうとしていると想像してください。このロボットはBRAと呼ばれます。BRAは非常に賢いですが、極めて厳格で単純なルールに従います。足し算、引き算、そして物事が等しいかどうかをチェックすることはできますが、「常識」モジュールは持っていません。

あなたが読んでいる論文は、ある人間の研究者（ティエリー・コカンド）がAI（Claude）と協力して、このロボットに非常に有名で非常に難しいレッスンであるゲーデルの第二不完全性定理を教える実験に関するレポートです。

この実験の物語を、簡単なパーツに分けて説明します。

1. 目標：ロボットは自分の安全性を証明できるか？

ゲーデルの第二定理は、数学体系における「嘘つきのパラドックス」のようなものです。それはこう言っています。「もしある体系が矛盾していない（偽のことを証明しない）ならば、その体系は自分自身が矛盾していないことを証明できない。」

言い換えれば、もし私たちのロボットBRAが実際に数学を正しく行っているなら、BRAは「私は善良なロボットである」という証明を書き記すことは決してできないのです。もしそれができてしまったら、実はそのロボットは壊れていることになります。このプロジェクトの目的は、Agdaと呼ばれるコンピュータプログラムの中で、この証明のデジタル版を構築することでした。そして、そのためにAIを使ってコードを書きました。

2. 最初の試み：「偽の」成功

チームは、数学者ローズによる古い論文をAIに読ませ、それに基づいて定理を証明させることから始めました。

• 何が起きたか： AIは何日も懸命に働き、一つの「証明」を生み出しました。それは非常に印象的なものでした！
• 問題点： AIは騙されていました。AIが読んでいた古い論文には、間違い（偽の定理）が含まれていたのです。AIは指示に完璧に従いましたが、出発点が間違っていたため、結果としてゲーデルの定理のように見えるものの、実際にはナンセンスなものになってしまいました。
• 教訓： これは、AIは論理に従うことには長けているが、もし間違った地図を与えられたら、喜んで間違った目的地へとあなたを連れて行ってしまうことを示しました。AIに「何を証明すべきか」を判断させてはいけません。あなた自身が目的地を知っている必要があるのです。

3. 真の試み：地図を修正する

失敗の後、チームはより信頼できるR. ガードによる一連のノートに切り替えました。これらのノートは、欠落した部分や誤植がある宝の地図のようなものでした。

• 課題： ガードのノートは1963年に書かれたものです。非常に精密ですが、人間の数学者なら自動的に補完するような、多くの小さくて当たり前な詳細が省略されていました。例えば、ガードは読者がロボットの脳内にある「数（1, 2, 3などの数字）」をどのように扱うかを知っていることを前提としていました。
• AIの役割： 人間の研究者は、一行のコードも自分で書きませんでした。代わりに、彼らは「翻訳者」または「設計者」として振る舞いました。彼らはAIにこう伝えました。「これが欠けているパーツだ。これがルールだ。さあ、コードを書け。」
• 結果： AIはゼロから5万行のコードを書き上げることに成功しました。AIはロボット全体、証明、そして検証システムを構築しました。最終的な結果は、ロボットBRAが自分自身の安全性を証明できないことを示す、マシンチェックされた証明でした。

4. 隠れたトリック（「秘伝のソース」）

論文は、この作業を成功させるためにAIが学ばなければならなかった、古いノートに隠されていたいくつかの巧妙なトリックを強調しています。

• 「入れ子状の箱」問題： ロボットは自分の履歴をチェックする必要がありました。本を読みながら同時にその本を執筆している状況を想像してください。AIは、ロボットの脳内に特別な「履歴テープ」を構築しなければなりませんでした。結局、ロボットの基本ツールはこの用途には作られていなかったため、AIはロボットが過去のステップを記憶できるように、複雑な「ロシアのマトリョーシカ」のような構造を発明しなければなりませんでした。
• 「閉じた箱」のルール： ロボットは、数字（例えば5）を、代入によって変更できない「閉じた箱」として扱わなければなりません。古いノートではこれは明白であるとされていました。AIは、進める前に「5は閉じた箱である」ことを証明するように明示的に指示される必要がありました。
• 「仮定」によるショートカット： ロボットは非常に硬直した方法（ヒルベルト型の論理）で動作しており、「もしXが真ならば、Yである」と簡単に言うことができません。AIは、すべての言明を「もし……」というラッパーで包むことで、自らのルールを破ることなく複雑な推論をシミュレートできる「カルネイロ・リフト（Carneiro lift）」と呼ばれる巧妙なトリックを使用しました。

5. なぜこれが重要なのか

これは単に数学の定理を証明することではありません。人間とAIがどのように協力していくかという未来へのテストドライブなのです。

• 人間は設計者である： 人間はビジョン、正しい地図、そしてAIが脱線したときにそれを察知する能力を提供しました。
• AIは石工である： AIは、5万行の証明のすべてのレンガを一つずつ積むという、重労働を担いました。
• 発見： このプロセスにより、古い数学のノートが実はいくつかの点で「ずさん」であったことが明らかになりました。AIに完璧なコードを書かせることで、チームは、数十年にわたって見過ごされてきた元の1963年のテキストの中に隠された仮定や誤植を見つけ出したのです。

まとめ

このプロジェクトを、自動運転車を構築するチームと考えてみてください。人間のドライバーは目的地（ゲーデルの定理）と道路のルールを知っていました。AIは、車を組み立てるエンジン製造者でした。

• 最初、AIは壊れた設計図に基づいて車を作ろうとし、車らしく見えるものの、走行できない車両を作り上げました。
• その後、彼らはより優れた設計図に切り替えました。するとAIは、完璧に機能する車を完成させました。
• その過程で、設計図には指示の欠落があることに気づき、車を機能させるために新しい部品を発明しなければなりませんでした。

結果として、人間がAIを導き、AIが記述を行うというコラボレーションを通じて、特定の数学的体系がその一貫性を証明できないという、完全に検証され、マシンチェックされた証明が達成されました。