
导语
人工智能如何改变数学研究的方式与范式。本期为AI for Math读书会第二季第6期,北京大学生物医学前沿创新中心博士朱韬宇将梳理大模型、强化学习与数学智能体的技术基础,看AI如何从辅助解题走向研究级探索,再以Navier-Stokes方程为例讨论形式化与语义一致性,最后谈人机协作与责任边界。
为系统梳理 AI 在科学与数学领域的最新进展,集智俱乐部联合同济大学数学科学学院长聘副教授陈小杨、北京工业大学数学统计学与力学学院副研究员诸葛昌靖共同发起「人工智能与数学」读书会第二季。组织对该主题感兴趣的研究者与探索者共同研读前沿文献、交流研究思路。
读书会将于2026年9月22日起,每周二19:30-21:30线上开展,持续8-10周,包含主讲分享与讨论交流,并提供会后视频回放,诚邀相关领域研究者及跨学科兴趣者参与。

报告简介
本次分享围绕“AI时代的数学发展”展开,探讨人工智能如何改变数学研究的方式与范式。首先介绍数学AI的技术基础,包括大语言模型、强化学习、形式化证明及数学智能体的工作机制;其次结合陶哲轩的研究观点、First Proof及OpenAI数学成果集,分析AI从辅助解题向研究级数学探索的转变;随后以Navier–Stokes方程为核心案例,讨论数学命题形式化、证明验证与语义一致性之间的关系;进一步介绍丘成桐相关研究案例及国内外数学Agent的发展;最后总结AI时代数学研究的新流程、人机协作模式、责任边界与未来发展方向。
分享大纲
数学AI技术基础:大模型、强化学习与数学智能体
AI从辅助解题到研究级探索:陶哲轩等观点
N-S方程:形式化、验证与语义一致性关系
丘成桐研究案例与国内外数学Agent发展
总结AI数学新流程、人机协作与责任边界
核心概念
数学Agent(数学智能体):能够围绕数学任务自主规划、调用工具、执行搜索、检查结果并迭代修正的系统。
符号推理(Symbolic Reasoning):基于明确的数学规则和逻辑关系进行推导,具有严格的规则约束。
形式化证明(Formal Proof):将数学命题和证明转化为严格的形式语言,使其能够由计算机进行逻辑检查。
Lean:一种交互式定理证明系统,通过类型检查验证形式化命题及其证明对象。
证明搜索(Proof Search):在已有假设、引理和目标之间探索不同推导路径,寻找完整证明。
命题即类型(Curry–Howard Correspondence):将数学命题与类型对应,将命题的证明视为该类型的一个具体对象。
语义一致性(Semantic Fidelity):检查形式化表达是否忠实对应原始数学问题,包括对象、假设、量词和结论。
反模型(Countermodel):构造一个满足前提但不满足结论的数学结构,用于否定普遍性命题。
证明依赖图(Proof Dependency Graph):记录定理、引理之间的依赖关系,帮助追踪证明错误及其影响范围。
可验证性(Verifiability):数学结果能否通过形式检查、计算证书或独立审查获得可靠证据。
可复现性(Reproducibility):通过固定代码、工具版本、依赖和运行记录,使研究结果能够被重新检查。
Goodhart定律:当一个指标成为优化目标时,它可能逐渐失去原本衡量真实价值的能力。报告借此讨论不能简单用AI解题数量衡量数学研究价值。
主讲人介绍

主讲人:朱韬宇,北京大学生物医学前沿创新中心博士,本科毕业于浙江大学。研究方向:计算生物学,代数拓扑,黎曼几何。我的研究兴趣主要是聚焦通过数据整合建模发掘生物靶以及解析生物数据中的几何结构进行相关建模与理论证明。主要研究方向之外,我喜欢研究形变量子化以及韩国流行音乐,是11年的Buddy (GFRIEND粉丝)和4年的Na.V (VIVIZ)粉丝,并且是半程马拉松大众精英跑者,半马PB 1:22:39。
参考文献
[1] Tao, T. (2026). Mathematics in the Age of AI. arXiv:2608.16753.
从“AI能否做数学”转向“AI时代数学真正珍视什么”,强调理解、结构与知识组织的重要性。
[2] Klowden, T., & Tao, T. (2026). Mathematical Methods and Human Thought in the Age of AI. arXiv:2603.26524.
从认知与工具演化角度讨论AI如何扩展数学思维,并重塑人机协作方式。
[3] Abouzaid, M., Srivastava, N., Ward, R., & Williams, L. (2026). First Proof Second Batch. arXiv:2606.18119.
以真实研究问题评测AI能力,为“AI进入研究级数学”提供实证背景。
[4] Hubert, T., Mehta, R., Sartran, L., et al. (2026). Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 651, 607–613.
AlphaProof代表性工作,展示AI在形式化数学推理与自动验证方面的快速进展。
[5] Thurston, W. P. (1994). On proof and progress in mathematics. Bulletin of the American Mathematical Society, 30(2), 161–177.
经典讨论数学进步不仅在于证明,更在于形成和传播数学理解,与AI时代的讨论高度呼应。
[6] Yao, Z., & Su, J. (2026). Manifold fitting: A review of methods and applications. Harvard Data Science Review, 8(3).
系统梳理流形拟合理论,明确其与降维、嵌入和去噪的区别,是理解数据几何发现的重要综述。
[7] Fefferman, C., Ivanov, S., Kurylev, Y., Lassas, M., & Narayanan, H. (2018). Fitting a putative manifold to noisy data. Proceedings of Machine Learning Research, 75, 688–720.
奠定从有限有噪高维样本恢复潜在流形及其几何性质的重要理论基础。
[8] Yao, Z., & Xia, Y. (2025). Manifold fitting under unbounded noise. Journal of Machine Learning Research, 26(45), 1–55.
将流形拟合推广至无界噪声环境,为现实数据中的稳定几何恢复提供统计保证。
[9] Whiteley, N., Gray, A., & Rubin-Delanchy, P. (2026). Statistical exploration of the manifold hypothesis. Journal of the Royal Statistical Society Series B, 88, 353–385.
从统计生成机制解释高维数据为何自然呈现低维流形结构,为“从数据中发现数学结构”提供理论依据。
报告简介
本次分享围绕“AI时代的数学发展”展开,探讨人工智能如何改变数学研究的方式与范式。首先介绍数学AI的技术基础,包括大语言模型、强化学习、形式化证明及数学智能体的工作机制;其次结合陶哲轩的研究观点、First Proof及OpenAI数学成果集,分析AI从辅助解题向研究级数学探索的转变;随后以Navier–Stokes方程为核心案例,讨论数学命题形式化、证明验证与语义一致性之间的关系;进一步介绍丘成桐相关研究案例及国内外数学Agent的发展;最后总结AI时代数学研究的新流程、人机协作模式、责任边界与未来发展方向。
分享大纲
分享大纲
数学AI技术基础:大模型、强化学习与数学智能体
AI从辅助解题到研究级探索:陶哲轩等观点
N-S方程:形式化、验证与语义一致性关系
丘成桐研究案例与国内外数学Agent发展
总结AI数学新流程、人机协作与责任边界
核心概念
核心概念
数学Agent(数学智能体):能够围绕数学任务自主规划、调用工具、执行搜索、检查结果并迭代修正的系统。
符号推理(Symbolic Reasoning):基于明确的数学规则和逻辑关系进行推导,具有严格的规则约束。
形式化证明(Formal Proof):将数学命题和证明转化为严格的形式语言,使其能够由计算机进行逻辑检查。
Lean:一种交互式定理证明系统,通过类型检查验证形式化命题及其证明对象。
证明搜索(Proof Search):在已有假设、引理和目标之间探索不同推导路径,寻找完整证明。
命题即类型(Curry–Howard Correspondence):将数学命题与类型对应,将命题的证明视为该类型的一个具体对象。
语义一致性(Semantic Fidelity):检查形式化表达是否忠实对应原始数学问题,包括对象、假设、量词和结论。
反模型(Countermodel):构造一个满足前提但不满足结论的数学结构,用于否定普遍性命题。
证明依赖图(Proof Dependency Graph):记录定理、引理之间的依赖关系,帮助追踪证明错误及其影响范围。
可验证性(Verifiability):数学结果能否通过形式检查、计算证书或独立审查获得可靠证据。
可复现性(Reproducibility):通过固定代码、工具版本、依赖和运行记录,使研究结果能够被重新检查。
Goodhart定律:当一个指标成为优化目标时,它可能逐渐失去原本衡量真实价值的能力。报告借此讨论不能简单用AI解题数量衡量数学研究价值。
主讲人介绍
主讲人介绍

主讲人:朱韬宇,北京大学生物医学前沿创新中心博士,本科毕业于浙江大学。研究方向:计算生物学,代数拓扑,黎曼几何。我的研究兴趣主要是聚焦通过数据整合建模发掘生物靶以及解析生物数据中的几何结构进行相关建模与理论证明。主要研究方向之外,我喜欢研究形变量子化以及韩国流行音乐,是11年的Buddy (GFRIEND粉丝)和4年的Na.V (VIVIZ)粉丝,并且是半程马拉松大众精英跑者,半马PB 1:22:39。
参考文献
参考文献
[1] Tao, T. (2026). Mathematics in the Age of AI. arXiv:2608.16753.
从“AI能否做数学”转向“AI时代数学真正珍视什么”,强调理解、结构与知识组织的重要性。
[2] Klowden, T., & Tao, T. (2026). Mathematical Methods and Human Thought in the Age of AI. arXiv:2603.26524.
从认知与工具演化角度讨论AI如何扩展数学思维,并重塑人机协作方式。
[3] Abouzaid, M., Srivastava, N., Ward, R., & Williams, L. (2026). First Proof Second Batch. arXiv:2606.18119.
以真实研究问题评测AI能力,为“AI进入研究级数学”提供实证背景。
[4] Hubert, T., Mehta, R., Sartran, L., et al. (2026). Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 651, 607–613.
AlphaProof代表性工作,展示AI在形式化数学推理与自动验证方面的快速进展。
[5] Thurston, W. P. (1994). On proof and progress in mathematics. Bulletin of the American Mathematical Society, 30(2), 161–177.
经典讨论数学进步不仅在于证明,更在于形成和传播数学理解,与AI时代的讨论高度呼应。
[6] Yao, Z., & Su, J. (2026). Manifold fitting: A review of methods and applications. Harvard Data Science Review, 8(3).
系统梳理流形拟合理论,明确其与降维、嵌入和去噪的区别,是理解数据几何发现的重要综述。
[7] Fefferman, C., Ivanov, S., Kurylev, Y., Lassas, M., & Narayanan, H. (2018). Fitting a putative manifold to noisy data. Proceedings of Machine Learning Research, 75, 688–720.
奠定从有限有噪高维样本恢复潜在流形及其几何性质的重要理论基础。
[8] Yao, Z., & Xia, Y. (2025). Manifold fitting under unbounded noise. Journal of Machine Learning Research, 26(45), 1–55.
将流形拟合推广至无界噪声环境,为现实数据中的稳定几何恢复提供统计保证。
[9] Whiteley, N., Gray, A., & Rubin-Delanchy, P. (2026). Statistical exploration of the manifold hypothesis. Journal of the Royal Statistical Society Series B, 88, 353–385.
从统计生成机制解释高维数据为何自然呈现低维流形结构,为“从数据中发现数学结构”提供理论依据。
时间信息
时间信息
报名读书会:AI for Math
报名读书会:AI for Math

报名方式

加入社区可享核心资源

特色退费与激励机制
任务达标退费路径 认领并合格完成任意两期字幕任务,即可退还全额报名费,并额外获得集智专属周边奖励。 运营成长激励路径 合格完成一个字幕任务后,可申请成为运营助理。在读书会项目顺利结项后,将退还学费。表现优异者,还有机会获得额外的奖学金。
推荐推荐
推荐推荐
「AI for Math」读书会第二季推荐阅读材料

往期公众号相关内容推荐

内容中包含的图片若涉及版权问题,请及时与我们联系删除




评论
沙发等你来抢