「時代を先取りしていた」：AI が数学を書き換えた人物のノートに隠された発見を明らかに

オーストリアの論理学者クルト・ゲーデルは 20 世紀で最も独創的な思想家の一人だ。1931 年に発表した 2 つの不完全性定理は数学の姿を変え、デジタル時代への道を開いた。

1930 年代にそうした画期的な成果を上げた後、ゲーデルが発表した論文はわずか数本しかない。だが未発表の草稿は数万ページに及び、科学史の研究者にとってはきわめて興味深い対象であり続けてきた。

2017 年から、フィンランドの論理学者ヤン・フォン・プラトがヘルシンキ大学でプロジェクトを率い、ゲーデルが 1940 年代初頭に書き残した 16 冊のノートを解読してきた。作業ノートと呼ばれるこの資料は計 1,009 ページに及び、数学と論理について稠密に論じている。そのかなりの部分がドイツ語の速記であるガベルスベルガー式で書かれており、この速記法はゲーデルが使っていた当時すでに時代遅れだった。

数学的な解読は週に 1 ページほどと極端に遅いペースで進んでいたが、9 月にフォン・プラトが AI モデルの Claude に助けを求めた。すると Claude は 2 日以内に全資料の完全な要約を出し、ゲーデルが誰にも知られていない数百の定理を証明していたことを明らかにした。

近代で最も名高い論理学者は、実際には誰も思っていたよりはるかに多くの発見をしていた。

アルベルト・アインシュタインがプリンストン大学でクルト・ゲーデル（右から 2 人目）に賞を授与する。二人は後に友人になった。画像提供は Bettmann/Bettmann Archive

「驚いた」とフォン・プラトは言う。「ノートには、70 年代や 80 年代に再発見された結果が数十件あるだけでなく、今も誰も研究を続けていない論理の主題が 14 個含まれていた。ゲーデルは時代をはるかに先取りしていた」

ゲーデルが論理学の流れを変えたのは、数学的知識の限界を明らかにしたからだ。不完全性定理は、あらゆる数学の体系に証明も反証もできない真の命題が存在することを示す。あらゆる真理は検証できると期待していたそれ以前の世代の論理学者にとって、これは打撃だった。だがゲーデルの仕事はこの分野を新たな方向へ押し出し、アラン・チューリングが 1936 年に現代の計算理論を打ち立てる論文を書くきっかけになった。

1940 年、ゲーデルはナチス支配下のオーストリアから逃れた。ニュージャージー州プリンストンに落ち着き、高等研究院でアルベルト・アインシュタインと親交を結んだ。晩年は疑心暗鬼が強まり、妻が手ずから作った料理以外は口にしなくなり、1978 年に餓死した。

フォン・プラトが 2017 年にゲーデル・プロジェクトを始めたのは、ヘルシンキ大学をまもなく定年退職するからだった。「何か不可欠な存在になるにはどうすればいい？そうだ、ゲーデルの謎の速記ページを読み始めよう！」と振り返る。欧州研究会議から 250 万ユーロ（約 210 万ポンド）の助成を受け、ガベルスベルガー式速記を独学した。「この速記を読めるのは世界で 6 人しかいない。私はその一人だ」と彼は言う。その後、小さなチームを組んだ。

8 月、AI と定理証明に関するフランスの会議で、フォン・プラトは数人の計算機科学者に出会い、Claude を使ってノートを解読してはどうかと勧められた。ヘルシンキに戻るとすぐに取りかかり、ノートの自分の転写稿、これまでに書いたゲーデルに関する 6 冊の本、その他の二次的な科学文献をまとめて Claude に渡した。

「数日のうちに 650 ページのノート解読が出てきた。1 ページずつ照合しなければならないが、これは基本的に人間にはできない作業だ」と彼は言う。「人間は一度に 1 ページしか読めず、すぐ忘れる。50 ページほど読むのに 1 年かかる。すべての異なる部分を同時に頭に置いておくことなど、とてもできない。

「AI は千ページに散らばる断片をすべてつなぎ合わせられる。ゲーデルの書いたすべてを一つのまとまりとして見られる」

あるノートの速記の見本を収めたマイクロフィルムの画像。画像提供は高等研究院（Institute for Advanced Study）

ゲーデルの不完全性定理は、真偽がその形式体系から独立している命題、つまり体系の中では証明も反証もできない命題が存在することを明らかにした。1966 年、アメリカの数学者ポール・コーエンは連続体仮説と選択公理という二つの著名な命題の独立性を証明し、数学界最高の栄誉であるフィールズ賞を受賞した。

コーエンのフィールズ賞受賞を知ったゲーデルは、その結果は 1940 年代に自分がすでに証明していたと言った。だが同僚が証明を示すよう求めると、ゲーデルは自分のノートからそれを再構成できなかった。

フォン・プラトが Claude に最初に与えた課題は、ゲーデルの作業ノートに選択公理の独立性の証明が存在するかどうかを突き止めることだった。あれば、ゲーデルが 1966 年に語ったことが本当だったと裏づけられる。答えはイエス、ほぼイエスだった。「あと一歩だった」とフォン・プラトは言う。「ゲーデルはある定義を間違えていたが、2 年前にはまだ正しい定義を持っていた。だから、あと数か月あれば正しい定義にたどり着いていたはずだと皆が考えている。私に言わせれば、この証明の構造は実に見事で、集合論のこれらの結果がすべて同じ一つのパターンに従うことを示している。

「とりわけ衝撃を受けたのは、彼がアイデアから出発していることだ。式をいじくり回して、どこかにたどり着くのを期待するタイプではない。アイデアが非常に明晰で、それから整然と進む。一歩ずつ前に進み、この形式化作業で自分が立てた目標を最終的に成し遂げている」

Claude が再構成した選択公理の独立性の証明を受け取ると、フォン・プラトはそれを証明支援系の Coq に渡して検証した。Coq は数学の証明が妥当かどうかを検査するプログラムで、結果は合格だった。フォン・プラトは、ゲーデルが選択公理に関する仕事を当時発表していれば、1940 年のフィールズ賞を手にしていただろうと考えている。「コーエンが賞を取ったとき、それは自分が逃したものの一部だと、どこかで思っていたのかもしれない」

後の議論で、フォン・プラトは Claude に、ゲーデルが証明を与えたか、証明を概略したか、あるいは証明の着想を示した定理をノートからすべて抽出させた。Claude は 663 件を見つけた。それを Coq に投入したところ、「約 400 件は元の記述のまま検証を通り、約 200 件は手直しが必要だった。つまり定理の記述をより正確に書くか、何らかの仮定を補う必要があるということだ。約 50 件は誤りだったが、不思議ではない。ゲーデル自身もノートを読み返すとき、ときどき欄外に「falsch!」（誤り）や「schlecht!」（ひどい）と書き添えていた」

フォン・プラトはこう付け加えた。「ゲーデルの手稿を研究し続ければ、さらに多くの宝物が見つかると信じている。Claude によれば、これらのノートには論理学と数学基礎論に関する十数個のテーマが含まれていて、書かれてから 80 年以上、誰も見つけたことがなかった。だから探求する価値のある方向だ。だが、ほかにも多くの内容がある。彼の物理学と宇宙論のノートは未踏の領域で、現在の論理学のプロジェクトを終えたら探求を始めるつもりだ」

インディアナ州ノートルダム大学の論理学教授ジョエル・デイヴィッド・ハムキンスは、ゲーデルによる選択公理の独立性証明の再構成をまだ見ていない。だが、その再構成が成り立つならば、「それは並外れたことで、歴史的にも大きな意味を持つ。ただ、そのうちどれだけが Claude の功績でどれだけがゲーデルの功績なのかは、歴史家の仕事だ」と語る。

ハムキンスは言う。「ノートに[コーエンの証明]に似た内容があるからといって、彼がそれを完成させたことにはならない。当時、彼がその道を進んでいたことを示すだけだ。誰にも伝えていない仕事は功績にならない。だが、ゲーデルには画期的な着想がそれほど多かったのだから、彼のノートが刺激的な内容に満ちているのも、おそらく不思議ではない」