科研 AI 的焦點逐漸轉向：能否在受控環境中，連續規劃、執行、檢查並修正一段工作。近期兩個案例提供不同觀察窗口：OpenAI 公開 GPT-5.6 Sol 經 Codex 連接量子實驗室軟體，協助量測與校準；Anthropic 則說明 Claude 在 Lean 證明助手與多代理環境中，完成費馬最後定理的形式化與電腦核驗。
兩個案例都與科研程式有關，任務性質卻差異很大：前者面對真實硬體與量測雜訊，後者面對形式語言與可由編譯器檢查的邏輯鏈。本文比較案例背景、工作環境、驗證迴路、總成本、任務選擇與導入條件六個面向，協助研究者與工程師按任務判斷工具，也說明單一成功案例不足以證明某一工具全面勝出。
一、兩個科研案例分別展示了什麼
Codex 展示的是在研究者設定的流程、權限與實驗環境內，協助執行部分量子位元量測與校準工作；Claude 展示的是把既有數學證明轉成 Lean 可檢查的形式，並由證明助手核驗整條邏輯鏈。
Codex 如何協助量子位元量測
OpenAI 在 2026 年 9 月描述，MIT Engineering Quantum Systems Group 研究者 Beatriz Yankelevich 將 GPT-5.6 Sol 經 Codex 接到實驗軟體，測試尚未校準的六量子位元晶片。研究者提供量測技能與設計目標，系統選擇參數、操作硬體、分析後決定細化量測或保存結果。
GPT-5.6 Sol 是模型，Codex 是承載程式與流程的產品能力，控制軟體、設備與研究者技能則是客製化整合，案例結果不能直接歸因於單一模型。
Claude 如何完成費馬最後定理的形式化
Anthropic 於 2026 年 9 月公布的案例，是把費馬最後定理的既有證明形式化。Anthropic 團隊以數十個 Claude agents、Prove2Me、Lean 與數學函式庫，在 11 天內完成形式化工作；研究者設定目標並提供高層次指引，Claude agents 產生約 1,300 萬行 Lean 程式並證明數以萬計的中間定理，最後由 Lean 進行電腦核驗。
Lean 證明助手要求定義、前提與推理連結都有形式表示；形式化工程須補齊人類數學文章常省略的中間步驟。Anthropic 案例用 Prove2Me 維持定理圖，分離定理敘述與證明檔案，搭配 Claude Code 型多代理工具處理子問題。
“Although we do not think a formalized proof should replace a human-understandable exposition.”（Anthropic 研究文章）
二、長流程規劃與工具連接，差異在工作環境
兩個案例呈現的工作重點不同：量子案例依量測結果調整下一步並操作研究設備；形式化案例管理子定理、代理協作與依賴。這是案例環境造成的差異，不是 Codex 或 Claude Code 固定的產品能力邊界。
從外部世界取得回饋
量子實驗的回饋來自儀器與樣本：系統送出控制訊號，設備回傳資料，代理分析後調整參數。量子位元漂移、訊號變弱或雜訊增加時，程式還要處理控制介面與錯誤狀態，可能需要研究者指引。
在程式與證明空間內協作
Claude 的形式化案例主要在程式與證明空間內運作：代理依定理圖產生 Lean 程式，交由證明環境檢查，再共享通過的中間定理。團隊以有向無環圖與可搜尋的定理敘述，改善初期的狀態遺失問題。
Codex 與 Claude Code 的產品邊界
就本文兩個案例的工作環境觀察，Codex 案例接入既有軟硬體控制流程。Anthropic 文章描述的是 Claude Code-based multi-agent harness，搭配 Prove2Me、Lean 與數學函式庫處理形式化工作；第 3 條 v2.1.265 版本頁僅是產品說明，不足以證明該版本是這項工作的實際版本或必要元件，也不是效能測試。不能以這些個案界定產品能力或推論其他環境必然有相同分工。
三、驗證可靠性要看證據迴路
實驗代理要以原始資料、重複量測、設備狀態與研究者判讀共同驗證；形式化證明雖可交由證明助手檢查，仍須確認定理敘述、假設與形式化內容符合研究問題。
實驗資料的驗證方式
量子實驗中，程式通過測試不等於科學結論成立。即使程式與儀器正常，結果仍可能受校準品質、樣本差異、雜訊與未知物理現象影響。研究者要檢查原始紀錄、重現性、參數範圍、異常值與研究假設；代理不能單靠一次執行決定物理意義。
形式化證明的驗證方式
Lean 提供較明確的機械驗證迴路，但範圍是已形式化的定理敘述、假設、依賴與 Lean 環境，不涵蓋人類原始證明的全部語意與研究解釋。證明程式通過指定版本與依賴環境的編譯，可將部分審查轉成可重跑檢查。
然而，定理敘述寫錯或假設被省略時，程式即使通過也無法補救。形式化證明提供較強的邏輯檢查，不是對所有研究判斷的全面背書。
兩種驗證迴路不能互換，因為它們回答的問題不同。實驗迴路判斷外部世界的量測是否可靠，需看原始訊號、重複性、設備狀態與樣本條件；Lean 迴路判斷已翻譯成形式語言的推理是否符合規則，需看定義、依賴與編譯結果。
實驗回饋含有連續數值與未建模因素，形式化核驗則受定義範圍約束。把通過編譯當成實驗有效，或把一次量測成功當成數學證明完成，都會把驗證對象換掉。
研究者應該留下哪些紀錄
不論使用哪個 AI 程式工具，都應保存任務定義、版本、權限、輸入資料、日誌、測試結果與人工介入點；量子實驗另存設備設定與原始訊號，形式化證明另存 Lean 與定理依賴。
資料治理還要回答資料能不能被代理看見、修改與帶出環境。量子資料可能包含未公開的實驗條件，形式化專案則可能包含尚未發表的定理、授權函式庫或研究者身分資訊。導入前應把輸入、暫存檔、日誌和輸出分開定義權限，設定保存期限與可追溯的版本標記；需要外部服務時，也要依機構資安、個資與研究倫理規範，確認哪些內容可離開研究環境。
“Experienced researchers may still be able to identify the best calibration settings faster than current AI models.”（OpenAI 量子計算案例）
四、使用成本不能只看模型價格
科研 AI 的總成本，應計算模型輸出、執行時間、算力、工具整合、設備占用、人工監督、錯誤修正與重跑成本，不能只看訂閱或 API 單價。
模型與執行環境成本
量子量測案例需要實驗室軟體、設備權限與長時間環境。若量測占用稀缺設備，代理失敗的代價可能高於重試；建立量測技能、資料格式、停止條件與安全權限，也是模型價格表不會呈現的導入成本。
形式化證明也會消耗輸出 token、編譯時間與平行代理資源；約 60 億輸出 token 是 Anthropic 案例的個案實測，不是固定預算。導入前應估計子任務數量、失敗率、編譯資源與儲存需求。
人工監督與錯誤修正成本
成本還包括審查、錯誤接手與清理無效產出的時間。可用「完成一次可重現的晶片校準」或「通過版本固定的形式化檢查」作為任務單位，估算一次成功所需的模型、工具與人工成本。
以下表格整理兩個案例的工作流差異，不是產品基準測試、成本排名，也不能視為直接比價。
| 比較面向 | Codex 量子實驗案例 | Claude 形式化證明案例 |
|---|---|---|
| 主要環境 | 實驗室控制軟體、量子晶片與量測資料 | Lean、定理函式庫、Prove2Me 與多代理環境 |
| 回饋來源 | 儀器訊號、校準結果與物理狀態 | 編譯器、證明助手與定理依賴 |
| 長流程工作 | 依量測結果調整參數與下一步 | 拆解子定理、平行證明並維持狀態 |
| 主要不確定性 | 雜訊、漂移與非預期物理現象 | 定理敘述、依賴管理與形式化落差 |
| 人工責任 | 實驗設計、異常判讀與結果解釋 | 目標定義、假設檢查與可讀性審查 |
| 適合的驗證 | 重複量測、原始資料與設備紀錄 | 可重跑編譯、形式系統檢查與依賴鎖定 |
五、研究者與工程師如何按任務選擇
需要連接控制軟體、反覆量測或模擬，可評估具備相應工具鏈的 Codex 工作流；需要大型程式庫重構、長程式任務或形式系統檢查，則可評估具備相應工具鏈的 Claude Code 工作流。
任務選擇也要看錯誤的可逆性與證據成本。若錯誤會改變設備狀態、覆寫原始資料或影響未公開成果，應先限制代理只讀，或在沙盒中產生建議；結果可在隔離環境重跑，才適合逐步增加自主範圍。科研 AI 程式工具的適用條件是明確輸入、可觀測回饋、可回復操作和獨立審核者。
適合交給 Codex 評估的任務
可先評估流程邊界清楚的量測、校準、模擬與資料處理，例如讀取設備、掃描參數、產生圖表並檢查品質門檻，再把結果交給研究者。共同點是程式、工具與設備介面明確。
適合交給 Claude Code 評估的任務
Claude Code 類型的流程可評估程式庫理解、測試補齊、跨檔案重構、長時間除錯與多子任務交接；若已有測試、版本控制與審查流程，代理可把大任務拆成可驗證的小步驟。
形式化數學則依賴 Lean、定理函式庫、Prove2Me、代理編排與研究者指引；複製成果須能維護環境，並承擔大型程式碼、長時間編譯與人工閱讀。
高風險科研流程的人工檢查清單
- 先寫出任務的成功條件、不可碰觸的資源與必須交回人工的例外情況。
- 固定模型、產品、函式庫、設備設定與輸入資料版本，建立可重跑的執行紀錄。
- 將代理輸出分成程式正確性、資料品質、研究解釋三層檢查，不把其中一層通過當成全部通過。
- 先以低風險、可回復的子任務測試，再逐步放大權限與執行時間。
- 對正式研究結論、實驗設備操作與關鍵程式碼保留具名人工審核。
六、結論：選擇適合的驗證迴路
沒有足夠證據判定誰全面勝出；應先看任務需連接設備或管理形式化邏輯，再看成果能否由量測、測試或證明助手驗證。實務上可先以可回復、可重跑的低風險子任務做小規模評估。
目前證據來自供應商案例與媒體報導，缺乏同基準的獨立測試。量子案例遇異常仍可能需人工；形式化案例不等於發現新定理或適用所有科研程式。
- Codex 案例的重點是把代理接進真實實驗流程，Claude 案例的重點是把數學推理轉成可機械核驗的形式程式。
- 可靠性要看驗證迴路、資料與環境紀錄，不能只看模型名稱或單次成功結果。
- 成本應包含模型、工具整合、設備或算力、執行時間、人工監督與錯誤修正。
- 對高風險科研流程，人工仍要負責問題定義、異常判讀與正式結論。
常見問題
Q1: Codex真的能獨立完成量子計算實驗嗎？
它是在研究者設定的流程、權限與環境內，協助部分量子位元量測與校準；遇到弱訊號、雜訊或非預期現象仍可能需要指引。
Q2: Claude重新證明了費馬最後定理嗎？
案例核心是把既有數學證明形式化，產生 Lean 程式並由電腦核驗，不應寫成 Claude 發現或重新證明定理。
Q3: Claude Code v2.1.265就是完成形式化證明的工具嗎？
不能直接推論。Anthropic 案例搭配 Claude Code 型多代理工具、Prove2Me、Lean 與數學函式庫；v2.1.265 頁面只是產品版本說明。
Q4: 研究團隊要先導入哪一種 AI 程式工具？
先依任務環境選擇：量測與資料分析可評估具備相應工具鏈的 Codex 工作流；長程協作、重構或形式化檢查可評估具備相應工具鏈的 Claude Code 工作流。導入前先定義權限、驗證方式與人工接手條件。
參考來源
- OpenAI (2026). How GPT-5.6 Sol helps run quantum computing experiments. *OpenAI
- Anthropic (2026). Formalizing Fermat's Last Theorem. *Anthropic Research
- Anthropic (2026). Release v2.1.265. *GitHub: anthropics/claude-code
- Emma stein (2026). 5 年學術計畫被 AI 模型 11 天搞定！Claude 完成《費馬最後定理》形式化證明. *TechNews 科技新報
