Anthropic 用 Claude 自動化證明費馬最後定理，13 萬行 Lean 程式碼寫成史上最大形式化證明
Anthropic Research · 2026-09-04
Anthropic 於 2026 年 9 月 4 日發布研究報告，宣布完成費馬最後定理（Fermat's Last Theorem）史上第一個電腦可驗證的形式化證明，全程以 Lean 4 定理證明語言寫成，程式碼與證明路徑同步開源於 github.com/anthropics/fermats-last-theorem。這個證明把 Andrew Wiles 1995 年的原始數學證明，逐步轉換成機器可逐行檢查的形式化陳述。整個過程由多個 Claude agent 自動完成，而非人工逐行形式化。
核心內容
專案採用 Frey-Serre-Ribet-Wiles-Taylor 證明路徑的簡化版本（依 Darmon、Diamond、Taylor 的闡述），耗時 11 天、產出約 1300 萬行 Lean 程式碼，總計證明 30,300 個定理（其中 29,500 個實際用於最終證明），規模超過社群數學函式庫 Mathlib 的 5 倍。多個 Claude agent 透過一個定理陳述的有向無環圖（DAG）協同作業，並改用「陳述與證明分離存檔」的架構以加速平行編譯；初期約有 7% 的非樣板程式碼來自失敗嘗試，後續切換到協作平台 Prove2Me 後效率提升。整體運算成本約 60 億個輸出 token。
證明僅依賴 Lean 的三個標準公理（propext、Classical.choice、Quot.sound），不含任何 sorry、axiom、native_decide 或 unsafe 宣告。正確性由三種獨立方法交叉驗證：Lean 4.33.1 核心編譯（96 個平行工作、耗時約 5.5 小時、峰值記憶體 153GB）、leanprover/comparator 工具比對官方定理陳述、以及獨立 Rust 實作的 Nanoda 核心檢查全部 1,052,234 條宣告且零錯誤。專案採 Apache 2.0 授權，部分內容衍生自 Kevin Buzzard 的 Imperial College FLT 專案與 flt-regular 函式庫。
原始來源：Anthropic Research、GitHub: anthropics/fermats-last-theorem
工程師單人分解 RSA-260，刷新 35 年來最大整數分解紀錄
John D. Cook Blog · 2026-09-03
2026 年 9 月 3 日，Cognition 工程師 Eric Lu（@penlume）在 X 上發布一則貼文，只列出一個 130 位數的整數並附註「divides RSA-260」，等於宣告分解了 RSA-260——這是 1991 年 RSA Factoring Challenge 留下的一個 260 位十進位（862-bit）合成數，35 年來無人分解成功。消息發布數分鐘內，維基百科的 RSA numbers 頁面隨即更新。RSA-260 目前是通用演算法分解過最大的整數，取代了 2020 年由團隊合作分解的 829-bit RSA-250。
核心內容
兩個質因數 p、q 皆為 131 位數（431 bits），皆已通過質數驗證。技術文章 lilting.ch 指出，截至 9 月 4 日，Lu 並未公開所用演算法、軟體、硬體或運算耗時；文中推測最可能的方法是一般數體篩選法（General Number Field Sieve, GNFS），因為對於沒有小因數的一般合成數，GNFS 仍是已知最佳的古典演算法。以 RSA-250 已知耗費約 2,700 core-years 推算，RSA-260 的運算量估計約需 7,000 core-years，換算成 1 萬核心的叢集約需數月，但實際耗時仍取決於未公開的實作細節。文章也明確排除了量子運算涉入的可能。
RSA-260 的安全強度約為 74 bits，遠低於目前建議的最小金鑰長度 2048-bit（安全強度 107 bits）。破解 2048-bit RSA 金鑰所需運算量，約為分解 RSA-260 的 2^34 倍，因此這次分解不影響現行 RSA 部署的安全性，但反映出舊金鑰長度已不再具備安全餘裕。
原始來源：John D. Cook: New RSA number factored、lilting.ch: How was RSA-260 computed
除錯 ARM64 Hypervisor 當機才發現：NX bit 還能擋掉推測式指令擷取
purplesyringa.moe（客座作者 sleirsgoevy）· 2026-09-04
開發者 sleirsgoevy 在 purplesyringa.moe 的客座文章中，記錄了他開發 ARM64 裸機（bare-metal）hypervisor 時遇到的離奇當機：只要啟用 CTR_EL0 攔截，系統就會隨機掛起，必須靠 watchdog 重置。追查後發現問題根源不在軟體邏輯，而在記憶體屬性設定，測試環境為搭載 Cortex-A53 核心的 MediaTek MT6735。這揭示了 NX bit（不可執行位元）除了大家熟知的安全用途外，還有另一層微架構意義。
背景
NX bit 通常用來標記記憶體區域「不可執行」，是 W^X、DEP 等安全機制的基礎，目的是防止攻擊者把資料當程式碼執行。但文章指出，ARM 處理器會對任何標記為 Normal 且可執行的記憶體，進行推測式指令擷取（speculative instruction fetch）——即便該指令實際上永遠不會被執行到。
核心內容
作者的 hypervisor 採 1:1 位址映射，其中包含一段已鎖定、不可存取的 bootrom（位於位址 0x0）。當處理器對這段區域做推測性指令擷取時，就觸發了系統失敗。文章以組合語言對照示範：動態分支指令 blr x0 會啟動分支預測與推測執行，靜態分支 bl get_ctr_el0 則不會觸發同樣的推測行為。ARM 文件對此有明確區分：「標記為 Device 只能防止推測式資料存取；標記為不可執行才能防止推測式指令存取。」換言之，要完全阻擋推測存取，必須同時把區域標記為 Device 記憶體且不可執行，缺一都可能讓推測式指令擷取打到不該碰的位址。
原始來源：purplesyringa.moe: The NX bit is not just about security