当前位置： 首页  >> 智能环球  >> 查看详情

国内首次实现AI自主解决数学开放问题

来源： 科技日报   日期：2026-04-07  责编： 殷绪江  
分享:
   4月6日，记者从北京大学北京国际数学研究中心了解到，该中心董彬教授课题组与合作者组建的AI4Math团队用自主构建的自动化AI框架解决了交换代数中一个开放问题——安德森猜想，并在用于形式化验证数学定理正确性的编程语言和定理证明器——Lean中完成了约19000行的形式化验证。这是国内首次以AI框架攻克交换代数开放问题并实现大规模形式化验证，开辟了数学与AI深度融合的更多可能。
  安德森猜想由美国数学家安德森于2014年提出，它关注的是“准完备局部环”的一类性质——这类环旨在用代数工具刻画几何对象局部（如某点附近）的无穷小结构与变形。该猜想提出后十余年始终无人突破。
  此次解决安德森猜想，北京大学AI4Math团队搭建的双智能体协作框架功不可没。该框架由自然语言推理智能体Rethlas和形式化验证智能体Archon组成。研究中，Rethlas通过团队自研的Matlas自然语言语义检索系统，从上千万条数学陈述中精准定位到与猜想看似无关的整环完备化理论成果，以此构造反例。随后，Archon将证明转化为约19000行Lean代码，并在过程中自主发现初始方案存在隐含的逻辑漏洞，重新设计了形式化证明的整体技术路线，还在所需数学概念于Lean形式化数学库中尚未收录时，自主找到等价替代路径，最终完成的代码覆盖6篇外部论文关键结果，完成同等规模形式化工作的效率较经验丰富的Lean专家提升至少10倍。
  该成果的背后是团队三年的技术积累与跨学科协作。2023年，北京大学AI4Math团队正式组建，它由一群对这个方向有共同判断的人逐步自然汇聚而成，团队成员来自代数与数论、优化、机器学习与人工智能等方向。
  董彬告诉科技日报记者，团队认为，让AI做严肃数学推理，检索最为关键。他们打造了双引擎检索架构——LeanSearch和Matlas。LeanSearch用自然语言描述需求即可语义检索出相关定理，现已被Lean官方社区广泛使用。Matlas则覆盖上千万条数学陈述，支持命题级语义检索。在这些基础设施之上，他们搭建了前述两个AI智能体。
  北京大学数学科学学院院长、中国科学院院士刘若川指出，此次探索不仅解决了具体数学问题，更验证了AI与数学融合的新研究范式。中国科学院院士田刚由此呼吁，应鼓励和支持青年学者大胆创新，进一步推动AI与数学的深度融合，并在国家急需解决的重大科技问题中发挥关键作用。（记者张盖伦）




 
标签：具身智能科技机器人人工智能


手机端 点一点或扫一扫
咨询、采访、合作、投稿等请致电：13911566744（含微信）
        
【免责声明】
凡注明 “环球科技网” 字样的图片或文字内容均属于本网站专稿，如需转载图片请保留 “环球科技网” 水印，转载文字内容请注明来源“环球科技网”；凡本网注明“来源：XXX(非环球科技网)”的作品，均转载自其它媒体，转载目的在于传递更多信息，并不代表本网赞同其观点和对其作品内容的实质真实性负责，转载信息版权属于原媒体及作者。如转载内容涉及版权或者其他问题，请投诉至邮箱；1978751725@qq.com 
 
 
本网公告：环球科技网从不发布负面新闻资讯，也绝不会发布负面信息。如发现负面信息链接请甄别是否为环球科技网所发。本网系北京伯乐传媒广告有限公司主办、所有。本网唯一域名（www.hqkjw.cn），其它域名链接均为假冒。望广大网民及企业主认真甄别。

 





     
 
 


 

相关文章

  • 从春晚舞台走入清华，魔法原子明星熊猫“原宝”首秀清华园，瞄准具身智能人才生态 从春晚舞台走入清华，魔法原子明星熊猫“原宝”首秀清华园，瞄准具身智能人才生态 2026-03-23 11:34:39

       【环球科技网】2026年总台马年春晚，魔法原子旗下机器熊猫“原宝”凭借可爱的外形和出色的动作灵活度，一出道就圈粉无数，迅速成为大众关注的明星级机器人。最近，魔法原子又带着原宝来到了中国最顶尖高等学府之一的清华大学校园内，为广大师生带来一场关于具身智能前沿科技的盛宴。作为清华校友生态企业和具身智能行业的一线品牌... [阅读]

  • 中国具身智能迈向“真人级”应用 中国具身智能迈向“真人级”应用 2026-03-20 15:33:27

       从“跌跌撞撞”机械行走，到流畅自如与人类对打网球；从实验室演示，到开放环境挑战半程马拉松……近期，中国人形机器人接连上演震撼科技秀，刷新具身智能新高度。3月19日，科技日报记者走进北京人形机器人创新中心（国家地方共建具身智能机器人创新中心），探访实训现场与数据基地，对话业内专家，解... [阅读]

  • 车企为何扎堆进军人形机器人？ 车企为何扎堆进军人形机器人？ 2026-03-18 10:29:08

       丙午马年春晚的炫酷表演，让人形机器人成为百姓茶余饭后津津乐道的话题。值得关注的是，该领域正成为汽车企业前瞻性战略布局的焦点。据不完全统计，截至目前，以自研、投资入股、合作等方式进军人形机器人赛道的全球主流车企已近20家。 　　车企为何扎堆入局人形机器人？首先，是战略突围的紧迫性。尽管汽车产业抓住电动化、智能化转型机遇，在过去10年... [阅读]

  • 中国人形机器人频频“破圈”具身智能迈入应用时代 中国人形机器人频频“破圈”具身智能迈入应用时代 2026-02-27 20:48:45

       2026年伊始，从美国拉斯维加斯消费电子展（CES）到中国春晚，中国自主研发的人形机器人频频“破圈”，多家中国企业的产品和应用不仅在海外业界引发热议，更是在全球社交媒体平台和国际媒体不断“刷屏”。 　　这印证着业界的普遍观点：在当前这个技术爆发与产业重构的关键节点，人工智能（AI）正... [阅读]

新闻排行榜

热门新闻

推荐新闻