Altman談AI科學，數學怎驗證？

（媒角抵加／林承志綜合報導）OpenAI 執行長 Sam Altman 在 8 月 23 日的 David Senra 訪談中，把 AI 協助科學發現列為重要方向。此前的 8 月 1 日，OpenAI 公布內部 Astra 模型取得的 10 項數學與理論電腦科學結果。這些成果要走進研究共同體，必須同時留下公開論文、可重跑的形式化檔案與領域研究者逐項閱讀的紀錄；模型產生答案只是起點。

Altman談科學，OpenAI先端出10項數學結果

Altman 在訪談中談到新物理、疾病研究與數學時，把 AI 看成擴大人類理解能力的工具。這個說法在 8 月有了可攤開檢查的材料：OpenAI 8 月 1 日公布，內部版本的 Astra 對高維球體堆積、編碼理論、非 sofic 群、量子複讀與格點密碼等 10 個問題提出解答或重要進展。

公司同時公開論文、模型的推理說明與 ten-proofs GitHub 專案。專案列出 10 份 Lean 4 形式化檔案，並提供建置與獨立檢查的操作說明。OpenAI 表示，找到這批解答所需的 token，若以 Sol API 費率換算約為 2,000 美元；這是公司對推理 token 的換算，沒有涵蓋模型訓練、失敗嘗試、人類整理論文與研究者審閱的完整成本。

Astra 仍是內部模型。公開材料沒有 API、公開售價或台灣提供時程，研究者眼前可取得的是論文與形式化檔案，不是同一個可直接操作的模型。

80年猜想的反例，讓人看見驗證怎麼接手

在這 10 項成果前，OpenAI 5 月已公開一個平面單位距離猜想的反例。這道題由數學家 Paul Erdős 在 1946 年提出：平面上放置 n 個點時，距離恰為 1 的點對最多能有多少個？原先廣泛相信的上界，被模型提出的構造推翻。

接下來發生的事，比「模型解題」更接近科學工作的實況。Noga Alon、Thomas Bloom、Tim Gowers、Will Sawin、Victor Wang 等 9 位數學家在 arXiv 發表〈Remarks on the disproof of the unit distance conjecture〉，把模型輸出的論證整理為人類驗證、簡化且部分推廣的版本。這份稿件清楚列出原問題、定理、既有上界與新構造，讀者可以追到論證採用的數論工具與每一段條件。

Victor Y. Wang 也是該稿作者之一；其個人頁面列出他自 2025 年起任職中央研究院數學研究所。台灣研究者在這個案例中的位置，不是替模型背書，而是與其他數學家一起把結果轉成可閱讀、可討論的學術文本。

Lean能檢查論證，還要有人確認問題問得對不對

OpenAI 為 8 月公布的 10 項結果準備 Lean 4 形式化。Lean 是用於數學形式化與軟體驗證的定理證明器；它的核心會檢查寫成 proof term 的證明是否能成立。這能抓出長篇論證中容易漏掉的邏輯斷點，也讓外部人能用同一組檔案重跑檢查。

形式檢查仍要從第一行開始讀。研究者得確認 Lean 裡的命題是否真的對應自然語言的原題、假設有沒有少寫、結果是否早已存在於文獻，以及新界線到底改變了什麼。這些工作決定一個結論在學科中的位置，不會由編譯成功自動產生。

OpenAI 2 月公布 First Proof 題目嘗試時，就留下了一個可見的修正過程：公司起初認為第 2 題的證明可能正確，後來參考主辦方評註與社群分析，將它改判為錯誤。研究結果能被外部意見推翻或修正，才有機會累積成其他人能使用的知識。

研究團隊使用生成式AI，先留下四種紀錄

台灣實驗室、研究中心與研究所使用生成式 AI 做文獻梳理、程式協助或假說探索時，可以先把一個問題切成四份可交接的紀錄。

第一份是問題版本：研究題目、使用的定義、排除條件與已知結果。第二份是輸入與工具版本：資料來源、提示內容、模型名稱、外掛、程式庫與執行日期。第三份是可重跑產物：程式、計算步驟、圖表原始資料、形式化檔案或實驗設定。第四份是人類覆核：由哪位研究者讀過哪些段落、比對了哪些先行研究、修改了什麼，以及最後由誰對論文結論負責。

這四份紀錄能把「模型提出一個方向」轉成同事可以接手的研究流程。模型可能找到跨領域的線索，研究者仍要決定這條線索是否值得耗用實驗、運算與同行審閱的時間。

台灣要跟上的，不是未公開模型的傳聞

OpenAI 公布的 Astra 結果，讓數學研究第一次同時看到模型論證、公開論文與形式化驗證的大型組合；平面單位距離猜想的案例又補上了人類數學家整理與署名的環節。這套公開鏈條，才是研究團隊能實際檢查的部分。

對台灣團隊來說，眼前的問題不是何時能取得 Astra，而是下一個使用 AI 的研究結果是否留得下問題版本、輸入來源、可重跑產物與人類覆核。資料和程式能被另一位研究者重新執行、結論能被另一個領域的人追問，AI 才可能從加快產出，走到加快知識累積。

FAQ：AI數學成果怎麼看？

Lean 檢查通過，是否等於成果已獲數學界認可？

Lean 檢查的是形式化後的命題與證明。研究者仍會比對原題、假設、先前文獻與成果的重要性；這些環節決定結果會如何被學界引用與延伸。

平面單位距離猜想的案例完成同儕審查了嗎？

9 位數學家的〈Remarks on the disproof of the unit distance conjecture〉是公開 arXiv 預印本，文中描述為人類驗證、整理與推廣的版本。預印本與期刊同儕審查是不同程序，閱讀時應分開看待。

台灣研究者現在能使用 Astra 嗎？

OpenAI 將 Astra 描述為內部模型，8 月 1 日公開頁未列出 API、價格或台灣提供時程。研究團隊可先採用公開論文、可重跑程式與人類覆核的作法，建立自己的驗證流程。

資料來源

• David Senra，〈Sam Altman〉，2026-08-23，官方節目頁與完整訪談：https://www.davidsenra.com/episode/sam-altman
• OpenAI，〈Ten advances in mathematics and theoretical computer science〉，2026-08-01：https://openai.com/index/ten-advances-in-mathematics/
• OpenAI，ten-proofs，Lean 4 形式化與獨立檢查說明：https://github.com/openai/ten-proofs
• Noga Alon 等人，〈Remarks on the disproof of the unit distance conjecture〉，arXiv:2605.20695，2026-05-20：https://arxiv.org/abs/2605.20695
• Science News，〈An AI math breakthrough sparks calls for new guardrails〉，2026-08-01：https://www.sciencenews.org/article/ai-guardrails-erdos-math-problem
• Lean Language Reference，形式驗證工具說明：https://lean-lang.org/doc/reference/latest/
• Victor Y. Wang，個人頁與論文列表：https://web.math.princeton.edu/~vywang/
• OpenAI，〈Our First Proof submissions〉，2026-02-20：https://openai.com/index/first-proof-submissions/