AI 求解 ETH 难题：形式化证明与文本不匹配引质疑

针对近期 AI 宣称解决指数时间假设（ETH）难题，有分析指出其文本证明与 Lean 形式化证明不匹配。评论者认为，这不等于解法完全错误或失败，但验证与“清理”工作可能耗时极长、需要大量数学家参与，也为数学家创造了新的工作机会。