Astra 解决 10 个长期未解数学问题的推理成本约为 2,000 美元。Lean 证明已发布在 GitHub 上。

迄今为止，大部分讨论都集中在这些证明是否真实。这些证明已用 Lean 4 形式化，并附带机器可检查的证书，发布在 GitHub 上，同时还有一份 249 页的手稿。Lean 的内核会给出二元判定：证明能编译，或者不能。你不需要信任模型。你只需要 Lean 工具链和一台笔记本电脑。我一直反复思考的是成本。非 sofic 群的构造自 Gromov 于 1999 年引入 soficity 以来一直悬而未决。群论核心开放问题之一存在了二十七年，而按照当前 API 费率，找到证明的推理成本大约为两千美元。Connes 刚性猜想被推翻，Ehrhart 体积猜想被证明，用算术电路计算永久式的新下界，跨六个数学领域的结果，全部只需约 2,000 美元的算力。曼彻斯特数学家 Thomas Bloom 维护着 erdosproblems.com 上的 Erdős 问题目录，他称这些结果“重大新闻”。他评价这些结果比五月的单位距离反例更重要。Bloom 正是去年十月将 OpenAI 此前的一项数学声明称为“戏剧性误述”的同一个人，所以他并非不加思考地给予赞扬。明显的反驳是：2,000 美元是一个误导性的数字。它只涵盖推理。它不包括训练算力、将问题陈述形式化的研究人员，也不包括 Astra 尝试过并失败的无数猜想。Ernie Davis 直接提出了这一点：进行这项实验的数学家和计算机科学家的薪资成本很可能比 2,000 美元高出几个数量级。如果一千个猜想进入，十个出来，那么每次成功的成本看起来就大不相同了。有道理。但训练是一项固定成本，可以分摊到模型运行的每一项任务上。再尝试一个猜想的边际成本正在趋近于零。如果真正制约硬数学进展的因素是以足够规模搜索证明空间，而每次尝试的搜索现在基本上免费，那么制约因素就转移了：选择哪些问题去形式化、正确编码，以及判断一个编译通过的证明是否有意义。这十项结果都没有经过同行评审。Lean 证书验证的是形式正确性，而非数学意义。如果定理陈述被编码得不精确，一个证明即使能编译也可能是平凡的。这正是同行评审所要弥合的差距。Astra 尚未发布。我们拥有证明。我们还没有这个系统。