OpenAI 用 Astra 模型攻克十大数学难题
Ten advances in mathematics and theoretical computer science
OpenAI 宣布其内部模型 Astra 在数学与理论计算机科学领域取得突破性进展，成功解决了十道长期悬而未决的难题。这些成果涵盖高维几何、编码理论、群论及量子复杂性等多个核心领域，包括对 Erdős 问题的解答以及 Connes 刚性猜想的证伪。所有证明均由模型生成，并由人类整理成文，最终通过 Lean 证书完成形式化验证。OpenAI 强调，AI 生成的证明应诚实归因，同时承诺向科学界开放工具，以加速未来发现。
我们致力于通过工具赋能科学家和数学家，从而加速发现进程。
HN 评论区
322- aabhay
我主要的抱怨在于整个实验和构建过程缺乏透明度。我怀疑他们并没有仅仅把模型指向这十个特定问题并只给一次尝试的机会；因此，那个 2000 美元的数字可能完全是误导性的，类似于通过不披露完整的实验设置来进行 P 值操纵。
我想知道：
1. 总共给了模型多少道题目？在放弃之前，有多少比例的问题未解决，成本是多少？
2. 你们让模型尝试解决这些问题多少次？
3. 支撑环境的成本有多高，例如模型是否有权访问作业集群？
- robinhouston
从某种意义上说，最引人注目的事实是这件事甚至没有登上 HN 首页。即使这比我们以前看到的有所进步，但 AI 能在数学和计算机科学领域取得重大进展这一想法，已不再让我们感到惊讶。
- Chance-Device
相当酷。AI 的影响已不可否认，在这个阶段，已经没有多少立场可以移动球门了，下一步他们恐怕得把球门移到体育场外面去。
人们越早从对这一切的否认中走出来越好，这样我们才能真正开始认真对待它。
- ultimatefan1
关于 AI 起飞（takeoff）的早期前提之一是：一个能解决高级数学开放问题的系统，也会发现数学和计算机科学的新进展，从而直接解锁大幅提升的软件性能。
我们正看到前沿级别的数学突破（即如果这是人类，其表现将跻身全球前 100 或前 1000 名数学家，意味着前 0.00001% 或 800/80 亿）。
我们也看到了软件性能的惊人进步。OpenAI 宣布通过修复 GPU 内核问题实现了约 15% 的提升。
这两者显然与缩放定律和智能泛化有关：一个巨大的模型在数学和软件工程方面获得了小模型无法企及的能力。
但在我看来，数学/科学发现明确解锁更好软件性能的可能性比以前小了。在某种意义上，这符合我们的直觉。当顶级科技公司雇佣数学博士类型的员工时，他们会让他们停止纯数学研究，转而专注于软件工程。这些人往往非常擅长软件工程，但这并非因为他们在学术数学上的最新发现，而是源于他们的通用智能。
对我而言，这是模型正在变强的证据，但并不能让我认为我们正处于由前沿数学革命推动的 FOOM 式快速起飞的前夜。
（我也在 Twitter 上发布了这条内容 @mlipman13）
- kcexn
由于我不是 OpenAI 声称取得“进展”的任何领域的专家，我不想过早贬低这一贡献的重要性。然而，我担心这篇博客文章中使用的语言是为了营销而夸大其词。
确实，在此之前还没有可靠的计算方法来解决这些问题。但是，这些证明是否为数学体系贡献了新思想，还是仅仅是一种有效的方法，通过穷尽式搜索文献来找到解决该问题所需的现有工具组合？
本质上，这些问题之前是否看起来有直观答案且可行证明，只是价值不够高，不值得专家投入时间？还是说在此之前它们本质上非常困难，而 AI 似乎做了比仅仅把问题扔进一个大求解器更多的事情？
- simonw
我对这个无名内部 AI 的强大能力印象深刻，但为什么没有任何人类贡献者的名字列在其中？难道至少没人给这个模型端过一杯咖啡吗？
- maxutility
我想知道这项研究的总成本是多少，包括他们的数学家和工程师的薪水。
- randomizedalgs
当 OpenAI 等公司不再对这些事情保持开放，而是直接将其打包进训练数据中时，会发生什么？