一道困扰学界几十年的开放问题，需要多少成本才能取得关键突破？OpenAI给出的答案是，十道题加起来，约2000美元。

近日，OpenAI公布了一份颇为惊人的成绩单。其下一代主要模型Astra的内部版本，在高维几何、编码理论、群论、算术电路复杂性、量子复杂性、格密码学和极值组合等领域，给出了十项新的研究结果。其中一些问题至少十年没有取得核心进展，另一些已经悬而未决数十年。结果包括构造出非sofic群、推翻Connes刚性猜想、解决三个Erdos问题，以及推进与后量子密码学密切相关的最近向量问题。

更值得注意的是，OpenAI称这些论证由Astra生成。人类研究人员随后借助同一个模型将论证整理成论文，模型又把每项证明形式化为Lean证书。按照Sol API的价格计算，模型寻找全部解法所消耗的token，成本大约为2000美元。

这十项成果的具体分布如下：在高维球体堆积问题上，模型给出了新的密度上界，将现有结果推进至Cohn-Elkies阈值；在二元码与球面码方面，模型指数级改进了二元码最大规模的已知界；模型还构造出一个非sofic群，从而证明非sofic群确实存在，解决了群论一个核心开放问题；针对Connes刚性猜想，模型给出了反例，表明某些群不能由其对应的冯-诺依曼代数唯一确定；在算术电路复杂性方面，模型推进了使用算术电路计算permanent的下界；模型还证明了适用于一般双人量子博弈的指数级并行重复定理；证明了最近向量问题在多项式近似因子下的计算困难性，这直接关系到后量子密码学的安全性；此外，模型还确定了Ehrhart体积猜想中特殊凸体的最大体积，为多色三角形Ramsey数建立了超指数级下界，并在极值图论的两个猜想上取得结果。

这次公布的成果包含一套完整的研究流程。首先，Astra内部版本搜索开放问题的解法并生成数学论证。随后，人类研究人员使用同一模型将原始论证整理成可公开阅读的论文。最后，模型把每一项论证转化为Lean证明证书，这是一种交互式定理证明器，可以把证明拆解为机器能够逐步检查的形式过程。OpenAI还同步发布了模型对每项解题过程的叙述说明。

这并非OpenAI首次公布由AI参与解决数学难题。今年5月，OpenAI曾公开一项由AI发现的Erdos单位距离猜想反例，该结果此后推动了数学和理论计算机科学领域的多项后续研究。OpenAI最近还宣布推出ChatGPT for Academic Researchers，计划向10万名科学家和数学家免费开放其最强的ChatGPT模型。

这十项结果意味着大模型在数学领域的角色正在发生根本性变化——它开始尝试进入真正的研究无人区，提出此前不存在的论证，并接受形式化证明系统的逐步检查。当提出猜想、寻找证明、检查逻辑和形式化验证逐步连接起来，数学研究的瓶颈可能发生转移。研究者需要花费更多精力判断哪些问题值得解决，哪些机器生成的思想具有更深层的理论意义。