Auto formalisation of Chaitin and of the surprise incompleteness Theorem

大局的な視点：ロボットに数学を教える

非常に賢いロボット（Claudeという名前のAI）と、非常に厳格でルールに縛られた数学の教科書「基本再帰算術（Basic Recursive Arithmetic）」を想像してみてください。この教科書は、非常に特定のルールを持つゲームのようなものです。基本的な数え上げと単純な論理のみを使用でき、凝ったショートカットや「魔法」のようなトリックは一切禁止されています。

この論文の目的は、このロボットが、数学の限界に関する有名な複雑な証明を読み取り、人間が一行のコードも書くことなく、その教科書の厳格な言語へと完全に書き換えることができるかどうかを検証することです。

答えは**「イエス」**です。ロボットは、これら2つの深い数学的概念をこの厳格な言語へと翻訳することに成功し、コンピュータが100%正しいとチェックできる証明を作成しました。

2つの主要な概念

この論文は、2つの有名な概念に焦点を当てています。それは、シャイティンの証明（第一不完全性定理に関連するもの）と、驚きの試験パラドックス（第二不完全性定理の一種）です。

1. 「短い記述」ゲーム（シャティンの証明）

限られた文字セットを使って書ける、あらゆる可能な物語のライブラリがあると想像してください。

• ルール： いくつかの物語は非常に短く、説明が簡単です。しかし、他の物語は非常に複雑で、それらを説明する最短の方法は、物語そのものをそのまま書き出すことだけになります。
• 問題： シャティンの証明は、短いプログラムでは説明できないほど「非常に複雑な」物語を見つけ出そうとする試みです。
• ロボットの挑戦： この証明を行うために、ロボットは数学の教科書の中に、物語を読み込み、実行し、それが何をするかを確認できる「機械」を構築しなければなりませんでした。
• 障害： 数学の教科書はあまりに単純であるため、「プログラムを実行する」という動作を自然に扱うことができません。なぜなら、実行には通常、教科書が許可していない複雑な関数（アッカーマン関数など）が必要だからです。
• 解決策： 人間の著者は「ギャンディ／ハワードの主要化（Gandy/Howard majorisation）」と呼ばれるトリックを提案しました。これは、ロボットに燃料タンクを与えるようなものです。機械に永遠に走り続けるよう求める代わりに、ロボットはプログラムが終了するためにどれだけの「燃料」（ステップ数）が必要かを正確に計算します。ロボットは、タンクが空になる前にプログラムが必ず停止することを保証する、特別な「燃料計」を構築します。
• 結果： ロボットはこの燃料計を自力で構築しました。もし「単純に記述するには複雑すぎる」数値を記述しようとすれば、論理的な矛盾（例えば、0が1に等しいという証明）が生じることを、ロボットは証明しました。

2. 「驚きの試験」と砂の山

第二の部分は、有名なパラドックスを扱っています。「教師が来週、抜き打ちテストを行うと発表しました。生徒たちは、もし木曜日までにテストが行われなければ金曜日だと分かってしまうため、金曜日はあり得ないと推論し、同様に木曜日もあり得ないと結論づけ、最終的にテスト自体が存在しないと結論づけます。しかし、水曜日にテストが行われ、それはサプライズとなりました。」

この論文は、この論理の一種（クリッチマンとラズによるもの）を用いて、数学体系が自身の整合性（矛盾を含まないこと）を証明できないことを証明しています。

• 従来の方法： 以前の証明では、矛盾を見つけるために日数や数値の数を数えていました。
• 新しい方法（ソリテス／砂の山）： 著者らはこれを**「砂の山のパラドックス」**と比較しています。
  • 砂の山から一粒の砂を取り除いても、まだ砂の山です。
  • もう一粒取り除いても、まだ砂の山です。
  • 一粒ずつ取り除き続けると、最終的に砂がゼロになります。しかし、一体どの時点で「砂の山」ではなくなったのでしょうか？
• 応用：
  • 0から非常に大きな数 $N$ までの数値のリストを想像してください。
  • この論理は次のように証明しようとします。「これらすべての数値が短い記述を持つことは不可能である」。
  • ロボットはこれをステップ・バイ・ステップで証明します。「もし0から $N$ までの数値がすべて短い記述を持つと仮定すると、矛盾が生じる」と言います。
  • 次に、0を取り除きます。「なるほど、もし1から $N$ までの数値が短い記述を持つとしても、依然として矛盾が生じる」。
  • ロボットは、一つずつ数を取り除くように、数字を消し続けます（砂の山から粒を取り除くように）。
  • 最終的に、リストが空になった地点に到達しますが、それでも論理は矛盾を強要します。
• ひねり： 本論文は、これが自己参照による「悪循環」ではなく、むしろ砂の山のようなものであると主張しています。一粒（一つの数値）を取り除くことは安全ですが、それを繰り返せば構造全体が崩壊します。この崩壊こそが、数学体系が自身を壊すことなく、自身が安全（整合している）であることを証明できないことを証明しているのです。

なぜこれが重要なのか（論文による説明）

1. 数学のアシスタントとしてのAI： この論文は、現在のAI（Claudeなど）が、複雑な数学的証明の極めて細かく退屈な詳細を扱うのに十分な能力を持っていることを示しています。AIはパーサーを構築し、機械を評価し、人間が通常手動で行う論理ステップを処理することができます。
2. 構成的数学： 「構成的数学（何かを実際に構築しなければならない数学）」において、「部分関数（実行が止まるかどうかわからないプログラム）」という概念は非常に扱いにくいものです。ロボットは、永遠に走り続ける可能性のあるプログラムを使用しましたが、証明はそのプログラムが停止することを保証しています。これは、AIが正しく対処した、微妙かつ極めて重要な区別です。
3. 魔法のトリックなし： ロボットは「タクティクス（戦術）」や豪華なライブラリを使用しませんでした。数学システムの基本ルールのみを使用して、すべてをゼロから構築しました。これにより、証明は非常に堅牢になり、コンピュータによる検証が容易になります。

結論

この論文は、AIが形式的な数学において強力なパートナーになり得ることを示すケーススタディです。AIは高レベルのアイデア（例：「数学には限界がある」）を取り込み、それを厳格でマシン検証可能な形式へと翻訳することができます。

著者らは、AIには人間のガイド（「燃料タンク」のトリックを提案するなど）が必要であるものの、AIはその後、コードを自律的に書き、論理を構築し、プロセス全体を文書化できると述べています。その結果、これらの深い論理的パラドックスがどのように機能するかを明確にし、曖昧さを取り除いて、硬い論理的事実のみを残した、完全に検証された証明が得られるのです。