OpenAI用AI攻克难解数学猜想
Ten advances in mathematics and theoretical computer science
OpenAI宣布其内部模型Astra在数学和理论计算机科学领域取得了十项重大突破，解决了包括高维几何、群论和量子复杂性在内的多个长期悬而未决的问题。这些成果不仅推翻了Connes的刚性猜想，还为非sofic群的存在提供了构造证明，并显著改进了二进制码和球面码的界限。OpenAI强调，虽然数学论证完全由AI生成，但人类负责了手稿的整理和Lean证书的形式化验证，并承诺对结果的正确性负责。这一进展标志着AI作为科研合作伙伴的新阶段，同时也引发了关于学术归属和AI在数学研究中角色的深刻讨论。
我们坚信，归属权应诚实地反映成果的生成方式：将完全由AI系统生成的证明归功于人类作者，既歪曲了系统的贡献，也曲解了真正人类智力工作的本质。
HN 评论区
908- sothatsit
人们争论我们处于 y-5、y 还是 y+5 的位置，与此同时，我们似乎正处于一条 y=2^x 的指数曲线上，不断产出越来越令人印象深刻的结果。
对我而言最有趣的问题是：像数学这样正在经历指数级变化的领域，哪些会被这种指数增长所吞噬，而哪些不会？写作领域一直相当顽固，但我注意到 Fable 在这方面确实迈出了一大步。那政治领域呢？我们会发展出新的方式，让人们在民主制度中表达自己的价值观，还是仅仅变得更擅长操纵？那些以实验驱动的领域，比如生物学，又会怎样？
- written-beyond
HN 再次用伪造的提交时间把这篇帖子推到了首页，这很有趣。里面已经有两天前的评论了，他们为什么偏偏想让这篇帖子获得更多流量，这看起来很奇怪。
- DrBazza
把哲学家换成数学家，道格拉斯·亚当斯（Douglas Adams）又一次精准预言了。
虽然目前的模型无法“直觉”地提出猜想，但它们确实能通过人类无法完成的繁琐计算，非常迅速地证伪其中一些猜想。我想，今天确实有一些数学家，他们过去几年的研究心血，就这样被推翻了。
——
“是的，我们就是，”Majikthise 坚持道，“我们明确是联合哲学家、智者、发光体及其他思考者工会的代表，我们要关掉这台机器，而且现在就要关！”
“有什么问题吗？”Lunkwill 问道。
“我来告诉你问题在哪，伙计，”Majikthise 说，“界限划分，这就是问题所在！”
“我们要求，”Vroomfondel 喊道，“界限划分可能不是问题！”
“你们就让机器去算数吧，”Majikthise 警告道，“永恒真理的事我们会自己搞定，谢了。如果你想确认法律地位，最好去查查，伙计。根据法律，追求终极真理显然是你们这些职业思考者不可剥夺的特权。要是哪台该死的机器真把它找到了，我们不就失业了吗？我是指，如果我们半夜还在争论上帝是否存在，结果这台机器第二天早上就给了我们上帝的电话号码，那我们要有什么用？”
- plaidfuji
任何可计算的问题，最终都会向计算机屈服。
LLM 让数学证明变得更加可计算，因为计算机既能生成潜在解，又能自行验证解的有效性，并且有合理的概率收敛到正确答案。我想这在某种程度上以前就已经能做到了，但现在似乎变得呈指数级容易。但这并不意味着所有数学问题都能自动解决。
这在某种程度上类似于分子动力学、蛋白质折叠或有限元模拟等。一些以前通过计算无法解决的问题变得可解了。而另一些——绝大多数其他问题——仍然无法通过这些计算技术解决，因为所需的计算规模超出了想象。这些只是简单的事情，比如模拟一立方毫米水分子在 1 秒内的动力学。这远远超出了当前的能力范围（而且 LLM 也不会改变这一点）。
我觉得 LLM 很棒，我每天都在用，认为它们价值巨大。但如果这些东西真像人们宣传或恐惧的那样具有革命性，你应该立刻把它们指向最高价值的数学问题，看看进展如何。比如千禧年大奖难题。我没看到那些问题的解决方案。
所以是有局限的——但我们即将学到很多关于“新常态”的东西：什么样的数学证明属于简单题（layup），什么样的才是真正困难的。
- Chance-Device
相当酷。AI 的影响已不可否认，在这个阶段，已经没多少空间可以移动球门柱了，下次他们恐怕得把球门柱移到体育场外面去。
人们越早从对这一切的否认中走出来越好，这样我们才能真正开始认真对待它。
- muchmirulys
问题 1 和 9 意外地非常直观。
请查看这里：
1. 高维球体堆积
https://muchmirul.github.io/conjectures/sphere-packing/
2. 多色拉姆齐数
- kcexn
既然我对 OpenAI 有所“推进”的任何领域都不是专家，我不想过早贬低这项贡献的重要性。然而，我担心这篇博客文章中的措辞是为了营销而夸大其词。
确实，以前没有可靠的计算方法来解决这些问题。但这些证明是否为数学体系贡献了新思想，还是仅仅是一种有效的方法，用于在文献中穷举搜索现有工具的正确组合来解决该问题？
本质上，这些问题在之前是否看起来就有直观答案且可行证明，只是价值不够高，不值得专家投入时间？或者它们在之前从根本上就是困难的，而 AI 似乎做了比仅仅把问题扔进一个大求解器更多的事情？
- gpm
Henry Yuen（问题 6 的研究基于他的工作）对此的评论值得一读，IMO：https://bsky.app/profile/henryyuen.bsky.social/post/3ms2jpch...
- simonw
包含 Lean 形式化证明的 GitHub 仓库就在几个小时前刚发布：https://github.com/openai/ten-proofs
它还链接到一篇由 LLM 撰写的论文，该模型根据未公开的推理轨迹“重构了证明是如何形成的”：https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf
我希望他们能发布提示词（prompts）！
- ultimatefan1
关于 AI 起飞的一个早期前提是：一个能够解决高级数学开放问题的系统，也会发现数学和计算机科学的新进展，从而直接解锁大幅更好的软件性能。
我们正看到前沿级别的数学突破（即如果这是人类，其表现将跻身世界前 100 或前 1000 位数学家，意味着前 0.00001% 或 800/80 亿）。
我们也看到了软件性能的惊人进步。OpenAI 宣布通过修复 GPU 内核问题实现了约 15% 的提升。
这两者显然在缩放定律和智能泛化的意义上是相关的：一个巨大的模型在数学和软件工程方面都具备了小模型无法实现的能力。
但在我看来，数学/科学发现明确解锁更好软件性能的可能性，比以前似乎更低了。在某种意义上，这符合我们的直觉。当顶级科技公司雇佣数学博士类型的员工时，他们会让他们停止纯数学研究，转而专注于软件工程。这些人通常非常擅长软件工程，但这并非源于学术数学的最新发现，而是源于他们的通用智能。
对我来说，这是模型正在变好的证据，但这并不让我认为我们正处于由前沿数学革命引发的 FOOM 式快速起飞的前夜。
（我也在 Twitter 上发布了这条内容 @mlipman13）