作者用 AI+Lean 做定理证明遇挫：OpenAI 数学突破靠非形式化推理
Singularitarian · x · 2026-10-23
johnloeber 发布新长文，回顾今年多个周末用 AI + Lean 做自动化定理证明的经历，结论是「苦涩教训」再度胜出，并反思 OpenAI 数学仓库与人机协作数学的短暂窗口期。转发者 adibaradwaj 强调文中最大冲击点：AI 数学能力的近期进展似乎主要来自非形式化推理而非 Lean 这类形式化工具——证明先用明文生成，约一半事后才形式化。这更新了他对模型能力的判断：模型可能比表面看起来聪明得多，其智能的「尖峰性」可能被严重低估。
「漫话AGI」频道最新
- 单人预训练吓坏年轻研究员,资深学者撰文驳「技能已过时」恐慌 — RexDouglass · 2026-10-23
- NBER 出版《变革性 AI 的经济学》，Agrawal 与 Brynjolfsson 主编 — JMateosGarcia · 2026-10-23
- Pedro Domingos:AI 是智力杠杆,越聪明的人用它越强 — pmddomingos · 2026-10-23
- 意识科学家 Anil Seth 撰文:意识是生命的属性而非计算,造有意识 AI 是坏主意 — anilkseth · 2026-10-23
- Pedro Domingos 预测：2027 年将是史上修复安全漏洞最多的一年 — pmddomingos · 2026-10-23
- Beff Jezos：需要一套持续自适应智能体组成的「网络免疫系统」 — beffjezos · 2026-10-23