图片来源:Anthropic

Anthropic一款尚未公开的AI模型,在数学难题黎曼猜想的研究中取得重要进展。该模型将黎曼猜想已验证成立范围的下界大幅提高。

据科技媒体TechCrunch 11日(当地时间)报道,黎曼猜想是一个悬而未决逾150年的经典数学难题,与素数分布密切相关。该问题设有100万美元奖金,但至今仍无人获奖。此次研究成果距离对这一猜想作出一般性证明仍有明显距离,但外界普遍认为,这一案例打破了“现阶段AI完全无法触及这一层级问题”的固有认知,也表明大模型已经能够对接近真实科研水平的数学研究产生实质性推进。

除结果本身外,此次研究的方法同样引发关注。据报道,一名并未接受系统数学专业训练的Anthropic员工要求模型认真尝试证明黎曼猜想,并让其在约一天半时间内自主调度任务。最终,模型共测试了650种不同思路,调用60个子代理,累计消耗3100万token。

论文脚注显示,在这60个子代理中,2个负责提出关键数学思路,13个用于补充和拓展相关想法;30个尝试探索新路径但未取得成果;另有13个负责核验论证的准确性,最后2个参与初稿撰写。

Anthropic表示,公司内部两名数学家已对相关结果进行了核验。与此同时,研究团队还借助开源证明辅助工具Lean,对研究过程中形成的主张和论证进行形式化整理,使其能够以机器可检验的方式呈现。

近期,大语言模型在数学研究中的进展愈发清晰。今年以来,AI模型已经解决多个Erdos问题,且随着模型能力提升,相关成果质量也在不断提高。OpenAI近日披露,其内部“Astra”模型已证明10项关键结果。此前,Anthropic另一项研究还曾反驳长期受到讨论的Jacobian猜想。

不过,这一趋势也在数学界同时引发更高期待与更多担忧。今年6月,多位知名数学家在一份公开声明中指出,AI可能影响数学的核心价值。其担忧在于,数学证明原本应遵循“发现功劳归于特定作者、准确性责任也由特定作者承担”的标准,而这一基础或将受到冲击。

另一方面,也有观点认为,AI将以更复杂的方式改写数学研究的路径。菲尔兹奖得主Timothy Gowers在相关文章中写道,即便未来真的出现“数学定理不再与数学家个人绑定”的世界,这件事未必会比“天体并不以天文学家命名”更值得忧虑。

尽管此次成果并未完成对黎曼猜想的完整证明,但它仍被视为AI通过分工协作式架构推进“提出想法—验证论证”流程的一个代表性案例。接下来的关注点在于,这种方法能否从个别定理的突破,进一步演化为数学界可以接受的一般性发现体系。

关键词

#Anthropic #黎曼猜想 #大语言模型 #子代理 #Lean #形式化证明 #OpenAI #AI数学 #token #Erdos问题
版权所有 © DigitalToday。未经授权禁止转载或传播。