北京大学的研究人员开发出一种人工智能系统，能够解决一个困扰数学界长达十余年的数学猜想。
该系统成功实现了对交换代数领域一个问题的形式化证明，该问题最初由美国数学家丹·安德森（Dan Anderson）于2014年提出。
据《南华早报》报道，该AI仅用数小时便完成了求解过程，而整个验证过程的实际运行时间约为80小时。
双智能体架构
这一突破得益于一种专门设计的“双智能体”模型，旨在弥合人类直觉与机器逻辑之间的鸿沟。
其中一个智能体负责进行非形式化推理，利用自然语言探索各种策略并构建潜在证明；第二个智能体则负责将这些思路转化为严谨的数学格式，从而使机器能够进行绝对可靠的验证。
这一过程实现了从假设到形式化证明的自动化转换，而这类任务在传统上需要人类专家进行长达数年的协作才能完成。
开发团队指出，人工干预仅限于为系统提供AI无法自主获取的受限文档，而在求解过程本身的数学逻辑引导方面，无需任何人工干预。
尽管研究结果令人振奋，但作者在arXiv预印本平台发表的初步论文中提到，相关研究成果尚未经过同行评审。
随着研究人员在缺乏独立外部验证的情况下难以验证AI生成的证明，可靠性仍是该领域面临的主要障碍。研究团队建议，将自然语言推理与形式化验证相结合，最终有望提升人们对自动化数学发现的信心。
继阿里巴巴、字节跳动和DeepSeek等公司近期取得一系列备受瞩目的进展后，这一成就再次彰显了中国在全球AI竞赛中不断扩大的影响力。