研究者已在 OpenAI 最新数学成果基础上取得显著改进，并经 Lean 形式化验证

Reddit r/artificial 新闻
lean formal-verification ai-math openai research

摘要

研究者正迅速超越 OpenAI 近期由 AI 生成的数学成果，改进后的证明已通过 Lean 进行形式化验证，凸显了 AI 辅助定理证明领域的飞速进展。

至于「我们从这些粗制滥造的证明里学不到任何东西！」这个借口，现在可以不攻自破了 https://github.com/CrocSwap/integer-mult-bounds
查看原文

相似文章

数学家们对OpenAI大批新成果既惊叹又抱怨

Reddit r/ArtificialInteligence

OpenAI所谓的“倾倒式发布”——一次性公开数百个由AI生成的数学和计算机科学开放难题的成果——让数学家们既印象深刻又持怀疑态度：一方面出现了突破性的证明，另一方面关于这些成果如何产出的疑问依然存在。

OpenAI 的数学解答尚未达到该领域的标准

TechCrunch AI

OpenAI 发布了数百个由 AI 生成的高难度数学问题解答，但这些解答未能达到数学与人工智能咨询小组的标准，在形式化、思维链披露和人类可理解性方面存在不足。剑桥大学和国王学院的一篇论文指出，自然语言证明与 Lean 代码之间存在差异。