Kurt Gödelは発表したものよりはるかに多くのものを残しましたが、その大半はほとんど読めない状態でした。The Guardianが報じたヘルシンキのプロジェクトは、言語モデルが研究者なら何年もかかる作業を数日でこなしたことを示しています。1,009ページのノートの内容を整理し、数百の定理を取り出したのです。文章やコードではなく歴史研究でAIモデルが役立った、これまでで最もわかりやすい例の一つです。
対象は、Gödelが1940年代初めに書いた16冊のワークブックです。多くは当時すでに廃れていたドイツ語の速記法Gabelsbergerで書かれています。Jan von Plato氏は2017年からヘルシンキ大学でこのプロジェクトを率いており、欧州研究会議から250万ユーロの助成を受けています。同氏は、この速記を読める人は世界で6人しかおらず自分はその1人だと言います。8月にAIと定理証明に関する会議に出た後、同氏は自分の書き起こし、Gödelについての自著6冊、その他の二次文献をClaudeに渡しました。数日で650ページの解説ができあがり、1ページずつ確認する必要があったと同氏は述べています。
注目すべき結果はその先です。ノートに選択公理の独立性の証明が含まれているかを尋ねたところ、Claudeはあと一歩という議論を見つけました。この結果でPaul Cohen氏は1966年にフィールズ賞を受け、Gödelは自分が先に到達していたと主張していました。定義が一つ誤っていましたが、Gödelは2年前には正しい定義を持っていました。von Plato氏によると、再構成された証明は 証明支援系Coqの検証を通過しました。続いてClaudeは、Gödelが証明した、概略を書いた、あるいは着想を持っていた定理を663個挙げました。Coqでは約400個がそのまま検証され、約200個は命題をより正確にする、仮定を加えるといった修正が必要で、約50個は誤りでした。
長い文書でClaudeを使う人にとっての教訓は組み合わせにあります。von Plato氏の言葉では、モデルの強みは1,000ページを一度に見渡せることで、歯止めとなるのはモデルの言うことを鵜呑みにしない形式的な検証器です。数学や検証の作業向けに私たちが取り上げているLeanのツールも同じ考え方です。
疑問も残ります。再構成は公開も査読もされておらず、Notre Dame大学の論理学者Joel David Hamkins氏は、それを見ていないと断ったうえで、Cohenの証明に似ていることはそれを持っていたこととは違い、どこまでがClaudeでどこまでがGödelかは歴史家が判断すべきだと注意を促しています。十数個の未開拓のテーマがあるという主張もClaudeによるもので、まだ人間が確かめたものではありません。