研究者用Claude整理哥德爾筆記　形式證明還要查什麼？

（媒角抵加／林承志綜合報導）數學家哥德爾留下的手寫筆記，正透過人工轉錄與AI整理，成為研究者重新檢視的材料。赫爾辛基大學邏輯學者馮普拉托（Jan von Plato）表示，他將筆記轉錄稿交給Claude分析，再以形式證明工具Coq檢查部分推導。研究者提出的重建與驗證結果仍待外界取得相關材料，才能進一步評估。

關鍵資訊

• 原始材料：哥德爾的16冊工作筆記共1,009頁，許多內容使用德文速記。
• 人工與AI：馮普拉托先轉錄筆記，再提供轉錄稿與相關著作給Claude整理。
• 候選結果：馮普拉托表示，Claude列出663項包含證明、草稿或證明構想的候選結果。
• 形式檢查：馮普拉托稱，部分結果經Coq檢查；各項證明的形式化內容仍有待外界檢視。
• 歷史判斷：筆記的解讀及哥德爾與後來數學家各自的貢獻，仍需研究者比較原始資料。

從速記轉錄到AI整理：研究者先提供文字材料

赫爾辛基大學「哥德爾之謎」研究計畫說明，哥德爾留下大量尚未充分研究的筆記，其中使用一種如今少人熟悉的德文速記法。計畫目的是研究未發表材料，讓後來的邏輯學者與哲學研究者能夠使用。

馮普拉托向《衛報》表示，他把自己整理的筆記轉錄稿、相關著作及其他研究文獻提供給Claude，幾天後取得一份約650頁的筆記說明，仍需要逐頁檢查。奧地利《標準報》先前對他的訪問也記錄，他提供給AI的是英文轉錄內容。

馮普拉托進一步要求Claude列出筆記中具有證明、證明草稿或構想的數學結果。他向《衛報》表示，系統列出663項；這份清單包含不同完成程度的內容。

Coq檢查推導，仍須對照手稿與假設

馮普拉托表示，這些結果交由證明助理Coq檢查後，約400項按原有陳述通過，約200項需要修正，例如補充假設或讓敘述更精確；約50項則被判定有錯。這些數字來自他的訪談說明。

Coq的作用是檢查形式化後的推導，讓研究者能檢視結論是否依照設定的定義與假設成立。要理解它與歷史手稿的關係，還要看研究者如何把速記、轉錄與數學主張轉換成形式化內容，以及修正時加入了哪些條件。

選擇公理的重建，數學與歷史問題分開看

馮普拉托另向《衛報》表示，Claude根據筆記重建了關於「選擇公理獨立性」的推導，他將結果交給Coq檢查並通過。他的解讀是，哥德爾當年的筆記接近一個證明，但其中有定義需要修正。

這項研究也涉及數學史。美國數學家柯恩（Paul Cohen）因相關獨立性成果獲得1966年菲爾茲獎；哥德爾曾表示自己更早想出證明，但未能從筆記重建。《衛報》訪問的邏輯學者哈姆金斯（Joel David Hamkins）當時尚未看過這份重建。他認為，若推導經得起檢驗，將具有歷史意義；哥德爾原有想法與Claude補充的部分，仍需要歷史學者釐清。

對處理跨語古文書或研究筆記的台灣讀者而言，這個案例呈現的工作鏈包括人工辨讀、文字整理、推導重建與形式檢查。未來公開的手稿選段、轉錄對照、證明假設與Coq檔案，將有助研究者追查每一步的依據。

資料來源與更新紀錄

• 赫爾辛基大學：Gödel Enigma研究計畫。
• The Guardian：馮普拉托與哈姆金斯訪談，2026年11月13日。
• Der Standard：馮普拉托與哥德爾筆記研究，2026年10月19日。
• 2026年11月15日：初稿。