本文介绍了人工智能与数学交叉领域的新前沿——形式化数学推理。通过集智俱乐部发起的“人工智能与数学”读书会，探讨了AI for Math和Math for AI两个方面。形式化数学结合了数学的严谨性与AI的创造力，有望开发出能够可靠进行复杂数学推理的AI系统。随着生成式AI的崛起，形式化数学为AI在数学推理上提供严格的验证框架，而AI也有潜力帮助自动形式化，降低领域门槛，加速证明过程。北京国际数学研究中心徐天一研究员分享了形式化数学的发展现状，以及和生成式AI交叉的前沿进展。

🤖 形式化数学是将数学证明转化为计算机可验证的语言，要求每一步推理都精确到机器可验证的程度，没有跳跃和“显然”，只有严格的逻辑链条。这种严谨性使得形式化证明在传统上需要耗费大量时间和专业知识。

💡 随着生成式AI的崛起，大语言模型在准确性和可靠性方面面临挑战，而形式化数学刚好可以弥补这一短板，为AI在数学推理上提供严格的验证框架。反过来，AI也有潜力来帮助自动形式化，完成从自然语言到形式化语言的转换，降低领域门槛，加速证明过程。

📚 集智俱乐部联合同济大学、清华大学、南洋理工大学的老师们共同发起“人工智能与数学”读书会，旨在深入探讨人工智能与数学的密切联系，从 AI for Math 和 Math for AI 两个方面进行。

👨‍🏫 北京国际数学研究中心徐天一研究员分享了形式化数学的发展现状，以及和生成式AI交叉的前沿进展，涵盖形式化数学简介、形式化数学与生成式 AI 的互补短长以及目前的进展。

原创 集智俱乐部 2025-03-11 21:24 北京

人工智能能真正掌握数学吗？

导语

在2023年，由集智俱乐部联合同济大学特聘研究员陈小杨、清华大学交叉信息学院助理教授袁洋、南洋理工大学副教授夏克林三位老师共同发起“人工智能与数学”读书会，希望从 AI for Math，Math for AI 两个方面深入探讨人工智能与数学的密切联系。我们也在持续关注这个领域的发展。

形式化数学推理代表了AI for Math的新前沿，它结合了数学的严谨性与AI的创造力。这种结合有希望开发出能够可靠地进行复杂数学推理的AI系统，这不仅会推动数学本身的发展，还会为科学、工程和技术领域带来变革性影响。我们特别邀请到北京国际数学研究中心徐天一研究员在本周三（3月12日）晚在读书会上做加餐分享，关于AI+形式化数学的话题，是什么、为什么以及怎么做。

AI for formalized math: What, why, and how?

分享流程

 

19:00-20:30 主题分享，主讲人：徐天一

20:30-21:00 圆桌讨论，嘉宾：陈小杨

分享简介

形式化数学，将数学证明转化为计算机可验证的语言，长期以来一直是少数专家的领域。它要求将每一步推理都精确到机器可验证的程度，没有跳跃，没有“显然”，只有严格的逻辑链条。这种严谨性使得形式化证明在传统上需要耗费大量时间和专业知识，限制了其广泛应用。

Lean语言的形式化表述

随着生成式AI的崛起，这个领域也迎来了新的发展机遇。大语言模型有很强的推理能力，但是在准确性和可靠性方面面临挑战，形式化数学刚好可以弥补这一短板，为AI在数学推理上提供严格的验证框架。反过来，AI也有潜力来帮助自动形式化，完成从自然语言到形式化语言的转换，降低领域门槛，加速证明过程。

在本次分享中，将介绍形式化数学的发展现状，以及和生成式AI交叉的前沿进展。

分享大纲

 

形式化数学简介

形式化数学与生成式 AI：互补短长

目前的进展

主讲嘉宾简介

徐天一，北京国际数学研究中心研究员。研究方向为自动化定理证明及 Lean 语言元编程。开发了多种用于操作 Lean 语言代码的工具，涵盖数据提取、依赖关系分析和动态交互等功能。同时负责 LeanSearch 的维护。

圆桌嘉宾简介

陈小杨，同济大学特聘研究员。2014年5月获得美国圣母大学数学博士学位，2014-2016年在澳门大学从事博士后研究，并于2016年底入职同济大学。陈小杨的主要研究方向为黎曼几何，在 Geometry and Topology, Advances in Mathematics等期刊发表了多篇研究论文。近期，陈小杨与研究团队开展了大模型在基础数学的应用研究，并计划开发机器学习算法用于发现数学规律，构造数学猜想反例等。

同时陈小杨团队发起了“DeepMath开源计划”，旨在训练一个开源数学大模型，将其数学推理能力提升至数学专业博士生水平，同时探索大模型是否具有数学创造能力，以及大模型在前沿数学研究中的潜在能力。邀请数学爱好者和智能探索者共同创建数学大模型。

推荐阅读论文：

Yang, Kaiyu, et al. "Leandojo: Theorem proving with retrieval-augmented language models." Advances in Neural Information Processing Systems 36 (2023): 21573-21612. https://proceedings.neurips.cc/paper_files/paper/2023/file/4441469427094f8873d0fecb0c4e1cee-Paper-Datasets_and_Benchmarks.pdf

Gao, Guoxiong, et al. "A semantic search engine for Mathlib4." arXiv preprint arXiv:2403.13310 (2024). https://arxiv.org/abs/2403.13310v2

Gao, Guoxiong, et al. "Herald: A natural language annotated Lean 4 dataset." arXiv preprint arXiv:2410.10878 (2024). https://arxiv.org/abs/2410.10878

Lin, Yong, et al. "Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving." arXiv preprint arXiv:2502.07640 (2025). https://arxiv.org/abs/2502.07640

Ying, Huaiyuan, et al. "Lean workbook: A large-scale lean problem set formalized from natural language math problems." arXiv preprint arXiv:2406.03847 (2024). https://arxiv.org/abs/2406.03847

Xin, Huajian, et al. "Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data." arXiv preprint arXiv:2405.14333 (2024). https://arxiv.org/abs/2405.14333

扫码报名

直播信息

2025年3月12日 19:00-21:00

报名加入社群（可开发票）

集智斑图链接：https://pattern.swarma.org/study_group/32?from=wechat

扫码参与「AI+Science第三季：人工智能与数学」读书会，加入群聊，获取系列读书会回看权限，共建共享 AI for Math 科学社区，与一线科研工作者沟通交流，共同推动这一前沿领域的发展。

推荐阅读

数学推理与AI：机器学习系统能在多大程度上理解数学？

人工智能与数学前沿综述：如何借助 AI 发现数学规律？

数学探索的未来：从AI引导人类直觉到数学大语言模型

AI 驱动的纯数学和理论物理研究：自上而下、自下而上和元数学

人工智能与数学读书会启动

数十年来，人工智能的理论发展和技术实践一直与科学探索相伴而生，尤其在以大模型为代表的人工智能技术应用集中爆发的当下，人工智能正在加速物理、化学、生物等基础科学的革新，而这些学科也在反过来启发人工智能技术创新。在此过程中，数学作为兼具理论属性与工具属性的重要基础学科，与人工智能关系甚密，相辅相成。一方面，人工智能在解决数学领域的诸多工程问题、理论问题乃至圣杯难题上屡创纪录。另一方面，数学持续为人工智能构筑理论基石并拓展其未来空间。这两个关键领域的交叉融合，正在揭开下个时代的科学之幕。

为了探索数学与人工智能深度融合的可能性，集智俱乐部联合同济大学特聘研究员陈小杨、清华大学交叉信息学院助理教授袁洋、南洋理工大学副教授夏克林三位老师，共同发起“人工智能与数学”读书会，希望从 AI　for　Math，Math　for　AI 两个方面深入探讨人工智能与数学的密切联系。读书会已完结，现在报名可加入社群并解锁回放视频权限。

详情请见：

人工智能与数学读书会启动：AI for Math，Math for AI

点击“阅读原文”，报名读书会

阅读原文

跳转微信打开