（媒角抵加／林承志綜合報導）OpenAI於2026年10月6日公開內部AI模型產生的數學手稿與證明程式。數學與人工智慧諮詢小組AGMAI同日說明，成果公開後，仍由數學社群評估其影響並建立人類理解；它的諮詢不代表認可取得成果的過程。這批資料讓台灣研究者能閱讀手稿、檢查形式化證明與追蹤修訂，使用的模型則尚未公開，後續開放時程未公布。

關鍵資訊

  • 公開內容：目錄列出722份手稿，分成372組相關成果，另附部分形式化證明與10份推理摘要。
  • 電腦檢查：部分證明已轉成Lean程式；各篇形式化狀態不同。
  • 人類評議：AGMAI提出發布與理解成果的建議，個別成果的影響由數學社群評估。
  • 台灣可取得資料：GitHub公開手稿、來源檔案及證明材料；產生成果的內部模型尚未釋出。

722份手稿公開，相關結果分成372組

OpenAI在10月6日公告中表示，這批數學結果由內部前沿模型產生，發布前曾向高等研究院（IAS）的AGMAI徵詢建議。公司將材料放上GitHub，並公開部分推理摘要，讓外界能檢視結果與產生過程。

公開研究目錄涵蓋數論、幾何、分析、理論電腦科學等領域。依儲存庫說明，722份手稿分成372組，每組可能包含主結果、補充論證、推論或另一種證明。讀者可先從目錄找研究主題，再由手稿索引取得PDF及相關材料。

OpenAI在儲存庫說明中表示，各項成果目前處於不同的驗證階段，並將持續更新形式化材料。

Lean檢查形式化推理，學者接著研究證明的意義

Lean官方說明將它介紹為開源程式語言與證明輔助工具。數學定義、假設及推理可寫成程式，由系統檢查形式化證明。對研究者而言，除了閱讀文字論證，還多了一份可以交由電腦核對的材料。

OpenAI提供的形式化目錄列出證明與手稿的對應及驗證設定；Lean文件建議一次編譯較小部分，並另附驗證工具Comparator的操作說明。儲存庫明載，部分手稿尚無Lean形式化證明，未形式化的結果可能有問題，公司將修正並持續補上材料。

把證明整理成可解釋、可教學與可延伸使用的方法，是數學研究的另一部分。此前25位數學家的共同聲明與球體堆積形式化案例，也討論了電腦檢查之後，研究者如何繼續理解與整理成果。

AI生成概念圖，依公開文件及AGMAI建議整理。形式驗證檢查寫成程式的推理；AGMAI依是否有人理解並負責，提出期刊審查、同行討論或支持研讀與解說的建議。

AGMAI區分有人理解與尚無人理解的成果

AGMAI在9月29日發布原則中，提出兩種路徑：有數學家完整理解並負責的成果，建議依學術慣例公開預印本、投交期刊同儕審查，並向同行解釋工作。

若操作AI的人尚未理解論證，小組建議實驗室整理引用、定理與證明，公開產生過程及形式化狀態，再提供經費支持工作坊、研究小組或解說文章。理解成果的工作由社群主導。

小組也反對實驗室用學界無法取得的專有模型測試進階數學問題，並要求停止這項做法。發布原則是在這類模型仍被使用的現況下，提出對成果釋出的建議。

10月6日聲明：諮詢身分不等於成果背書

AGMAI在10月6日對OpenAI發布的回應中表示，小組獨立於AI公司，成員不因這項工作收取報酬；它提供諮詢，沒有公司內部決策權。

小組說明，諮詢角色不代表對這批成果的影響作出判斷，也不代表認可OpenAI取得成果的過程。公開資料是數學社群開始評估、理解及吸收成果的起點。小組並關注研究工具與算力的公平取得，讓數學家保有提出自身問題、發展研究方向的空間。

台灣研究者可讀手稿，使用模型仍待開放

台灣研究與教學團隊可從公開目錄選定主題，核對手稿與形式化材料，再以具體論證安排研讀與討論。參與程式驗證需要Lean及相關數學知識；OpenAI的文件也提醒，整個證明程式庫規模大，編譯全部內容可能遇到系統資源設定問題。

引用時，OpenAI的版本規則提供各手稿目錄內的BibTeX引用資料；更正與修訂將記為新版本，舊版仍保留。研究者因而能追蹤某項論證在哪一版改動，並引用特定手稿。

產生成果的內部模型尚未公開。OpenAI表示正準備負責任地釋出，公告未列開放日期、方案或地區。台灣讀者目前可取得的是研究材料；若在教學或研究中安排AI工作流程，可先從選定一份手稿、確認版本與由具備相關專業的人解釋論證開始。模型輸出的驗收問題，也可延伸閱讀Goodfire追查模型取巧交差的研究。

資料來源與更新紀錄