Jan von Plato氏が率いる研究プロジェクトは、歴史上最も影響力のある論理学者の一人であるクルト・ゲーデルの私的なノートを解読するために人工知能を活用しています。ゲーデルは自身の著作を比較的少なく公開していたため、ほぼ廃れた速記法で書かれたこれらのノートには、数十年間隠されたままの数百の証明済み定理が含まれていると考えられています。
論理学者の私的なノートを解き明かす
このプロジェクトは、数学と論理学を根本的に変貌させた人物であるクルト・ゲーデルのノートに焦点を当てています。ゲーデルはその貢献で知られていますが、出版には時間がかかることで知られ、Dialectica解釈のような複雑な主題に関する最初のアイデアを公開するまでに、時には数十年も待つことがありました。
これらのノートは、彼の思考プロセスを捉えた希少で未整理の視点を提供します。これらを解読することで、研究者たちはゲーデルが生前に公に共有しなかった膨大な数学的内容を回収することを期待しています。
「AIが、数百の証明済み定理が含まれているとされるゲーデルのノートを解き明かす」
— AI unlocks Gödel's notebooks, said to contain hundreds of proved theorems
Gabelsberger速記法の課題
これらのノートにアクセスする際の主な技術的障壁は、ゲーデルがGabelsberger速記法を使用していることです。この速記システムは1920年頃に学校で教えられていましたが、技術的に廃れ、現在では世界でもそれを読める人はごくわずかです。
ゲーデルの主要な専門家であるJan von Plato氏は、2017年にプロジェクトを開始するためにこの速記法を独学で習得したと報告されています。この取り組みを拡大するため、彼のチームは欧州研究会議（ERC）から250万ユーロの助成金を受け取り、既存の速記法の書き起こしデータを用いてAIモデルを訓練し、解読プロセスを自動化しました。
Hacker Newsでの議論と視点
この進展に関するHacker Newsでの議論では、AIと歴史的な数学の交差点について様々な視点が示されました。あるコメント投稿者（'semolinapudding'）は、ゲーデルの著作は非常に重要であるため、わずかな新しい成果であっても「非常に大きな出来事」になるだろうと、プロジェクトへの興奮を表現しました。
他の参加者は速記法の実用性について議論しました。例えば、'hobo123'という名前のコメント投稿者は、Gabelsberger速記法はしばしば廃れたものと見なされるものの、2020年代に入っても一部の個人によってまだ使用されていたことを指摘しました。別のコメント投稿者'2aFds'は、AIの有効性は、依然として広く利用可能な既存の速記法の書き起こしデータで訓練されたことに起因する可能性が高いと指摘しました。
議論ではプロジェクトの社会的影響についても触れられました。'alterom'という名前のコメント投稿者は、これが「出版か死か（publish or perish）」の文化を変える可能性があると示唆しました。それは、たとえ作品が未完成であっても、問題に対する思考の記録を早期に確立する手段を提供するためです。逆に、別のコメント投稿者'cyanydeez'は、ノート内の論理に関する最も複雑な批判は、最終的に現在の大規模言語モデルの「もどかしい限界」に達する可能性があると推測しました。
限界と不確実性
このプロジェクトは数百の定理を明らかにすることを約束していますが、具体的な数学的内容や、正常に「解読」された定理の正確な数はまだ完全には詳述されていません。また、AIが、標準的な数学的証明と比較して、ゲーデルが知られていたニュアンスに富んだ高度な論理的批判をどの程度捉えることができるかという継続的な疑問も残っています。