20世紀を代表する数理論理学者ゲーデルの速記ノートをClaudeが解読、未公開の定理も

人間の限界を超えた長文脈処理により数十年を要する解読作業を数日に短縮

　クルト・ゲーデルが1940年代に執筆した16冊のワークブックは、ガベルスベルガーと呼ばれる古いドイツの速記法で記されており、その解読は極めて困難であった。ヘルシンキ大学のヤン・フォン・プラト教授が率いる研究チームは2017年からこの文書の解読を進めてきたが、人間の手による作業ペースは1週間に約1ページにとどまり、全容の解明には膨大な時間がかかると予想されていた。

　状況が一変したのは、2026年9月にAnthropicの生成AIモデルであるClaudeが導入されたことによる。研究チームは、専門家によってプレーンテキストに書き起こされた文書データと関連文献をモデルに読み込ませた。Claudeは1009ページに及ぶ草稿全体を一括して処理し、数日のうちに約650ページの解説書を生成するとともに、草稿内に点在する663件の定理候補を抽出した。

　抽出された結果は、形式証明検証システムであるCoqを用いて検証された。約400件がそのままの形で正しいことが確認され、約200件は前提条件の追加やより厳密な記述への修正を経て検証を通過した。一方で約50件は誤りであると判定された。ゲーデル自身も過去のノートを読み返した際に余白に誤りを指摘するメモを残しており、検証ツールの結果は本人の推敲過程を裏付けるものとなっている。

　今回抽出された成果の中で最も注目されるのが、選択公理の独立性に関する証明である。ポール・コーエンが1966年にこの独立性を証明してフィールズ賞を受賞しているが、ゲーデルはそれより四半世紀も前に正解に非常に近づいていたことが分かった。草稿内の証明には1箇所だけ定義の誤りがあったものの、Claudeはゲーデルが2年前に書いた別のノートから正しい定義を見つけ出し、それを適用して証明を再構築した。この修復された証明は検証システムを見事に通過している。

　歴史に埋もれていた数学的遺産が最新のテクノロジーによって蘇ったことは、学術界に大きな衝撃を与えた。しかしこの画期的な成果は同時に、AI時代における科学史研究や業績の帰属について極めて複雑な問いを投げかけている。再構築された証明の功績は誰に帰属するのか、次ページでその議論の深層に迫る。