数学定理网络相关研究｜AI for Math读书会第二季第3期

集智俱乐部 · 2026-10-11 14:34 · 32 阅读

集智俱乐部 2026-10-11 14:34 浙江

2026年10月13日（周二）19:30-21:30分享

导语

数学定理的依赖网络，能否帮助AI更快寻找证明路径？本期为AI for Math读书会第二季第3期，北师大系统科学学院在读博士李晓凯将从复杂网络的视角看待数学证明，介绍以定理和公理为节点、证明中的引用为边形成的数学定理网络，梳理从《几何原本》到形式化定理库的网络构建与分析进展，并探讨利用网络结构加速AI数学证明的可能性。

为系统梳理 AI 在科学与数学领域的最新进展，集智俱乐部联合同济大学数学科学学院长聘副教授陈小杨、北京工业大学数学统计学与力学学院副研究员诸葛昌靖共同发起「人工智能与数学」读书会第二季。组织对该主题感兴趣的研究者与探索者共同研读前沿文献、交流研究思路。

读书会将于2026年9月22日起，每周二19:30-21:30线上开展，持续8-10周，包含主讲分享与讨论交流，并提供会后视频回放，诚邀相关领域研究者及跨学科兴趣者参与。

报告简介
公理系统构成一个有向无环图——把定理/公理视为节点，证明过程中的引用视为边，我们便能从图/复杂网络的角度来理解公理系统。Stephen Wolfram最早将数学定理之间的关系建模为复杂网络。在其著作《A New Kind of Science》中，他以复杂网络的形式展示了欧几里得《几何原本》如何从五条公理推导出全部 465 条定理。随着交互式定理证明器的兴起——如Lean、Coq、HOL、Isabelle 和Metamath——大量经过形式化验证的定理及其证明过程被系统地记录在各项目的定理库中，近年来大语言模型与交互式定理证明器的结合更是进一步加速了定理库的发展，为更大规模地构建和分析数学定理网络提供了数据基础。本报告将梳理从复杂网络角度看待数学证明的相关研究进展，并探讨从这一角度出发加速AI数学证明的可能性。

分享大纲

沃尔夫勒姆的开创性想法：数学定理网络
有向无环图：拓扑代与拓扑排序
Lean与Mathlib：大型数学定理库
利用大语言模型进行形式化证明
应用：通过考虑依赖关系来加速前提选择

核心概念

有向无环图
依赖树
形式化证明
前提选择

主讲人介绍

主讲人：李晓凯，北师大系统科学学院在读博士，研究方向为复杂网络、科学学、AI for Math和量化思想史。强调从网络结构和历史演化的视角来理解新知识的产生、科学的长期发展和科学家行为。两篇对学术史和思想史的定量化分析的工作曾发表在PNAS Nexus和Scienmetrics上。目前关注人类数学家和大语言模型在数学定理证明上的差异。

参考文献

[1] S. Wolfram, The Empirical Metamathematics of Euclid and Beyond, writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/ , 2021.

[2] K. Yang et al., LeanDojo: Theorem Proving with Retrieval-Augmented Language Models, in: Advances in Neural Information Processing Systems, Curran Associates, Inc., 2023, pp. 21573–21612.

[3] P. Song, K. Yang, A. Anandkumar, Towards Large Language Models as Copilots for Theorem Proving in Lean, 2024. arXiv:2404.12534.

[4] X. Li, N. Peng, S. Severini, The Network Structure of Mathlib, 2026. arXiv:2604.24797.

[5] S. Kurgan et al., TheoremGraph: Bridging Formal and Informal Mathematics, 2026. arXiv:2606.25363.

时间信息

⏰ 时间：2026年10月13日（周二）19:30-21:30

📍 线上：腾讯会议

📍 直播：微信视频号 + 集智俱乐部B站号同步放送

感兴趣的朋友请扫码报名加入读书会，报名后可进入学员群参与交流讨论。

直播信息

报名读书会：AI for Math

为厘清 AI 在科学与数学领域的机遇与局限，集智俱乐部联合同济大学数学科学学院长聘副教授陈小杨、北京工业大学数学统计学与力学学院副研究员诸葛昌靖共同发起「人工智能与数学」读书会第二季。组织对该主题感兴趣的研究者与探索者共同研读前沿文献、交流研究思路。

读书会自2026年9月22日起，每周二19:30-21:30线上开展，持续8-10周，包含主讲分享与讨论交流，并提供会后视频回放，诚邀相关领域研究者及跨学科兴趣者参与。

扫描海报中二维码报名参加读书会

报名方式

第一步：微信扫码填写报名信息。

（扫码报名）

第二步：填写信息后，付费报名。如需用支付宝支付，请在PC端进入读书会页面报名支付：

https://pattern.swarma.org/mobile/study_group/91?from=wechat

第三步：添加运营助理微信，拉入对应主题的读书会社区（微信群）。

PS：

为维护学术交流的专业性与聚焦度，本读书会对讨论内容作如下约定：

我们鼓励围绕数学、人工智能、复杂科学及相关具体问题的深入探讨。为保证讨论质量，请避免发表脱离本期读书会主题、缺乏实证基础或过于空泛的哲学思辨类内容。

若讨论内容明显偏离主题，经主持人提醒后仍未调整，为维护整体学习环境，我们将不得不将该成员请出讨论群，并根据其实际参与进度，对未参与部分按比例办理退费。

感谢您的理解与配合，让我们共同营造一个专注、深入、有收获的共学空间。

加入社区可享核心资源

成为会员即可解锁完整学习生态，包括：线上实时问答、全部课程录播回看、独家资料共享、高质量社群交流、第一手信息同步，以及通过参与共创任务获取积分等权益。

特色退费与激励机制

我们提供以下两种途径，让您的投入获得实际回馈：

任务达标退费路径
认领并合格完成任意两期字幕任务，即可退还全额报名费，并额外获得集智专属周边奖励。
运营成长激励路径
合格完成一个字幕任务后，可申请成为运营助理。在读书会项目顺利结项后，将退还学费。表现优异者，还有机会获得额外的奖学金。