报告简介

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

分享大纲

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

核心概念

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

主讲人介绍

主讲人：李晓凯，北师大系统科学学院在读博士，研究方向为复杂网络、科学学、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.

时间信息

报名读书会：AI for Math

报名方式

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

加入社区可享核心资源

特色退费与激励机制

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

推荐推荐

1. 「AI for Math」读书会第二季推荐阅读材料

1. 往期公众号相关内容推荐