Claude AI 耗時 11 天驗證費馬最後定理，寫下最長數學證明

費馬最後定理由皮耶・德・費馬於1637年提出，主張當n大於2時，正整數無法滿足aⁿ+bⁿ=cⁿ；安德魯・懷爾斯與理查・泰勒於1995年完成首個公認證明。此次突破並非另解難題，而是把既有論證形式化為Lean可逐步核驗的程式，降低複雜數學成果仰賴人工審查的風險。

Anthropic於2026年9月4日宣布，Claude透過哥倫比亞大學團隊開發的Prove2Me，在11天內大致自主產出1,300萬行Lean程式碼，證明30,300項定理，其中29,500項用於最終證明。倫敦帝國學院專案負責人Kevin Buzzard審閱後確認，該證明僅依賴Lean三項標準公理，可由電腦完整核驗。