AI 解鎖哥德爾筆記本，揭示數百個已證明定理

芬蘭邏輯學家 Jan von Plato 使用 Claude 消化 Kurt Gödel 1940 年代以 Gabelsberger 速記寫成的 1,009 頁工作筆記，這項工作原本以每週約一頁的速度進行。Claude 產出了一份 650 頁的說明，並辨識出 Gödel 已證明、勾勒或構思的 663 個定理；透過 Coq 證明助理執行後，約 400 個經證實與所述相符，約 200 個需要修正，約 50 個為假。Von Plato 表示，Claude 對選擇公理獨立性證明的重建通過了 Coq，這暗示 Gödel 在 1940 年代就已掌握該結果，且這些筆記本包含十多個尚未探索的邏輯主題。