研究與評測
據傳學者藉助 Claude 提出 Hopf problem 百頁證明，OpenAI 研究員以 Codex 轉為 25 萬行 Lean 程式碼
Reddit r/singularity單一來源
尚未逐項核實
目前依單一來源整理，這是來源數量描述，不是對消息真假的判定。
據社群消息指出，學者 Levent Alpöge 在 Claude 協助下，提出了一份長達 100 頁的 Hopf problem 證明，挑戰這道具 78 年歷史的數學難題。幾天後，OpenAI 研究員 Boris Alexeev 利用 Codex，將該證明形式化為 25 萬行的 Lean 程式碼，且初步驗證看似無誤。由於證明與程式碼規模龐大，消息稱目前可能尚無單一人類能完全理解所有細節。
讀原始報導背景
霍普夫問題（Hopf problem）是幾何學中著名的未解問題之一，最早可追溯至 1931 年。Lean 則是一種開源的證明輔助工具與函數式程式語言，常用於將數學證明轉化為可由電腦驗證的格式。