作者实测 AI 加 Lean 自动定理证明：苦涩教训再度应验

10 月 23 日,johnloeber 发布长文,回顾他今年利用多个周末尝试用 AI 加 Lean 做自动化定理证明的经历。他的结论是「苦涩的教训」再次胜出:OpenAI 的数学突破更多依靠非形式化推理而非形式化验证工具,并反思 OpenAI 数学仓库与人机协作数学的价值窗口可能十分短暂,「只有一个夏天」。

2026-10-23 ~ 2026-10-23 · 2 条相关