Claudeがヘルシンキの論理学者によるゲーデルの速記ノート解読を支援、数百の定理が明らかに

The Guardianによると、クルト・ゲーデルが1940年代初頭に記した16冊の「ノート」（全1,009ページで、多くが現在は使われていないガベルスベルガー式速記で書かれている）を研究するヘルシンキ大学のプロジェクトを2017年から率いてきたJan von Platoは、9月に自分の翻刻、ゲーデルに関する過去の著書、関連する二次文献をClaudeに与えた。von Platoによれば、Claudeは数日でノートの解説を650ページ分作成したが、ページごとの確認が必要だったという。

von Platoが発見したと述べる内容。 ノートに選択公理の独立性を示す証明が含まれているか尋ねたところ、Claudeはvon Platoが「ほぼ」完成しているとする証明を再構成した。ただし、2年前にはゲーデル自身が正しく定義していた定義を一つ誤っていたという。再構成された証明はCoq証明支援系で検証に通ったと、von Platoは述べている。ゲーデルが証明した、概略を示した、または着想を得ていた定理をすべて抽出するよう求めたところ、Claudeは663件を挙げた。von Platoによると、約400件は記述どおりCoqで検証でき、約200件には修正が必要で、約50件は誤りだった。また、Claudeはこれまで追究されていない論理学上のテーマを十数件以上見つけたという。

留意点。 再構成をまだ見ていないノートルダム大学のJoel David HamkinsはThe Guardianに対し、これが正しければ「驚くべきことで、歴史的にも興味深い」と語った。一方で、どこまでがClaudeによるもので、どこまでがゲーデルによるものなのかは歴史家が判断すべき問題であり、コーエンの証明に似ているからといって、ゲーデルがその証明を得ていたとは限らないとも述べた。