直播预约 | 从数学金牌到科学发现，AI 正在跨越什么

如果一个 AI 来到你的课题组，申请成为研究搭档，你会问它什么？

能不能解决复杂数学问题？能不能独立提出猜想？能不能持续推进一个尚无答案的研究课题？

以及，当它告诉你「我证明了」，你该如何确认？

过去一段时间，AI 在数学领域的进展，正让这些问题从想象逐渐走向现实。

从 IMO 银牌到金牌，从自然语言推理到形式化证明，再到对开放性数学问题的探索，AI 的能力边界不断向前延伸。

但解出一道难题，与真正开展数学研究之间，仍有距离。

当解题能力不再是唯一瓶颈，原创性、研究价值与可信验证，正在成为新的考题。

10 月 27 日 19:00，机器之心联合黄大年茶思屋科技网站，邀请李鹏、张驰、李嘉三位嘉宾，从数学推理、自动定理证明到研究级数学探索，共同讨论 AI 如何成为新型研究协作者。

嘉宾阵容（按分享顺序排列）:

• 李鹏，清华大学智能产业研究院副研究员
• 张驰，北京大学智能学院助理教授
• 李嘉，Project Numina 创始人

主题与嘉宾

当自然语言遇见数学：从推理、发现到创造

李鹏 | 清华大学智能产业研究院（AIR），副研究员

李鹏，清华大学智能产业研究院副研究员，主要研究方向包括大模型、智能体、AI4Math 与 AI 驱动的科学发现，在人工智能重要国际会议和期刊发表论文 100 余篇。曾获 ACL 2023 Outstanding Paper Award、ICAIS 2025 Responsible AI Research Award、中国中文信息学会钱伟长中文信息处理科学技术奖一等奖等荣誉，主持科技创新 2030 重大项目课题、国家自然科学基金面上项目等科研项目，曾担任 ICLR、ACL、EMNLP、NAACL 等国际会议领域主席。其研究成果在腾讯微信、百度等千万级日活产品中获得应用并取得显著成效。

报告摘要

自然语言是人类思想交流与知识创造的重要载体，数学则以严谨的逻辑与抽象的结构探索世界的深层规律。二者看似分属文理两端，却始终在人类的科学探索中紧密交织。近年来，大语言模型与智能体技术的突破，正在推动人工智能从数学解题走向开放性数学研究，甚至开始参与新问题的提出、理论的构建与科学发现。这不仅拓展了机器智能的能力边界，也引发了关于数学理解、科学创造与知识可信性的新思考。本报告将从自然语言与数学推理的内在联系出发，回顾人工智能数学能力的发展历程及最新进展，探讨从数学解题走向真正的数学研究所面临的核心挑战。在此基础上，介绍本团队研发的 AI 数学家系统 AIM，展示其如何依托自然语言与智能体协作机制，开展长期探索、研究路线拓展、定理形成与可信验证。进一步地，报告将结合科研品味学习与大规模数学形式化等探索，讨论人工智能如何从追求解题能力，走向兼顾科学价值、创造性与可信性的知识发现，并思考智能体时代数学研究的新机遇与挑战。

从零到金牌，再到更远：AI如何学会解决与发现数学

张驰 | 北京大学智能学院助理教授

张驰，北京大学智能学院助理教授、研究员（博士生导师），ARIA实验室负责人。他于浙江大学获计算机科学学士学位，于加州大学洛杉矶分校（UCLA）获计算机科学硕士、博士学位，师从朱松纯教授。加入北京大学前，曾任北京通用人工智能研究院（BIGAI）研究科学家，并在字节跳动 Seed 团队从事AI for Math研究，参与Seed-Prover自动定理证明工作。其研究聚焦于大模型高效推理、智能体与能动性、抽象推理与主动推理，致力于构建能够高效推理、自主行动的机器智能。代表性工作发表于 Science Advances、Nature Machine Intelligence（封面文章）及 NeurIPS、ICLR、CVPR、ICCV、ICML 等国际顶级期刊与会议；其提出的RAVEN数据集是视觉抽象推理领域的代表性基准，奥数几何命题与求解工作受到新华社、人民日报等媒体报道。团队工作获CogSci 2026马尔奖（Marr Prize，最佳论文）。

报告摘要

短短两年，AI在国际数学奥林匹克（IMO）上的表现从银牌水平提升到满分。2024年，AlphaProof与AlphaGeometry 2以形式化、重搜索的方式拿到银牌。2025年，基于Lean的形式化证明器（Seed-Prover、Aristotle）和自然语言推理模型（Gemini Deep Think、OpenAI）都达到了金牌水平。据报道，2026年已有多个系统拿到42/42满分。我们首先介绍我们在奥赛几何上的工作。我们把几何看作在有限构造空间上的树搜索，由符号推理引擎驱动；在这个框架下，命题与解题是对偶的两面。在LLM策略与价值估计的引导下，我们的系统只用32个CPU加一块消费级显卡，就超过了AlphaGeometry。2026年，AI推翻了Erdős关于单位距离问题的长期猜想；Claude完成了费马大定理的完整Lean形式化；OpenAI发布了涉及Navier–Stokes等公开问题的结果。未来，我们如何大规模验证结果？AI的成果是真正的原创还是重组？LLM想法多样性不足怎么办？创造力是否仍是人类的优势？这些问题仍然值得我们去深入思考。

大模型的数学能力：智能充沛时代的下一个瓶颈

李嘉 | Project Numina 创始人

李嘉，Project Numina 联合创始人兼科学负责人，曲速智擎创始人兼 CEO，前 Mistral AI 研究员。

长期从事人工智能、数学推理与科学智能研究。联合创立开源数学人工智能研究组织 Project Numina，领导开发 NuminaMath 数学推理数据集及 Kimina-Prover 形式化数学推理模型，团队获得 2024 年 AI Math Olympiad 首届进度奖。

此前联合创办医疗人工智能公司 Cardiologs 并担任 CTO，公司于 2022 年被飞利浦收购。

报告摘要

大语言模型最初通过预测下一个词学习语言，却在过去几年中迅速获得了求解数学问题、生成复杂推理乃至构造形式化证明的能力。这一进展并非单纯来自模型规模的增长，而是由高质量数学数据、思维链监督、过程奖励、强化学习和测试时计算等方法共同推动。

本报告将回顾大模型数学能力的发展历程，从 MATH、Minerva 等早期工作，到 o1、DeepSeek-R1 所代表的长程推理与强化学习范式。结合 Project Numina 的实践，介绍 NuminaMath 数据集、开放数学推理模型，以及 Kimina Prover 如何结合自然语言推理、Lean 形式化证明与强化学习提升数学能力。

最后，报告将探讨数学 AI 从解题走向数学发现的新挑战。当推理能力日益充沛，研究数据与可靠验证正成为新的瓶颈。我们将以模张量范畴（MTC）分类研究为例，介绍 Numina 如何探索从数据生成、结构发现、猜想提出到形式化证明的研究闭环，推动 AI 从解决已知问题走向前沿数学研究。

*分享顺序

此次分享将在机器之心视频号以及黄大年茶思屋科技网站双平台进行直播，欢迎大家关注、预约。

直播主题：从数学金牌到科学发现，AI 正在跨越什么

直播时间：10月27日 19:00 - 20:30

独家联合主办

黄大年茶思屋科技网站是致力于推动科学与技术交流的开放平台。我们汇聚全球科学家、研究人员和技术专家，共同探讨最前沿的学术话题，分享最新的科研成果，激发创新思维的火花。在这里，您可以看到学术热点、精选论文、学术峰会、技术难题、专利、开源和科技赛事等内容。茶思屋科技网站，汇聚全球科研智慧，推动科技创新，让科技百花园更加繁荣。

网址：https://www.chaspark.com