研究與評測
網友利用 Claude 耗時一個月寫出 Conway 猜想的 Lean 證明，已通過 Palomar 註冊表機械檢查
Hacker News綜合 2 家報導多家報導
尚未逐項核實
多個報導來源提及此事；未必是彼此獨立的證據。
一名自稱數學新手的網友耗費一個月時間與大量 Token，利用 Claude 輔助寫出了 Conway 猜想（Conway's refinement conjecture）的 Lean 證明。該猜想於 50 年前提出，主張超現實數（surreal numbers）中的全能整數（omnific integers）具有細化性質：若 ab = cd，則存在整數 e、f、g、h 使得 a = ef、b = gh、c = eg、d = fh。
目前該 Lean 證明已通過 Palomar 註冊表的機械檢查。作者表示，雖然證明尚未經過數學家獨立驗證，但熟悉 Lean 及該領域的人士認為陳述看似正確；若 Lean 核心沒有 Bug，該證明極可能有效。
在選題階段，Claude 建議選擇超現實數領域，並以 2026 年是 Conway 著作《ONAG》出版 50 週年為由推薦該猜想。然而作者事後發現，Claude 聲稱該問題已被 L’Innocente–Mantova 機制完美簡化的說法是錯誤的。此消息目前亦在 Reddit r/singularity 引發社群關注。
讀原始報導社群討論
社群對非數學專業人士利用 Claude 證明數學猜想感到震驚，讚賞其引導與驗證 AI 的技巧，甚至將此比喻為召喚 AI 解決問題的「巫術（sorcery）」。然而，許多人質疑作者不該將 LLM 的成果據為己有，並諷刺其在缺乏深度理解下產出定理，恰好違背了自身引用的數學社群理念。此外，也有人擔憂業餘人士會用 AI 產生的內容去信件轟炸專家，建議作者應先確認文獻是否已有相關證明並確實理解內容。
來源
- Reddit r/singularityreddit.com