Mathhall系列讲座回顾丨AI遇上形式化：数学定理证明的未来已来

9月26日下午，北京大学北京国际数学研究中心文再文教授在光华楼东主楼2001带来了一场题为《智能数学推理：形式化与定理证明》的前沿报告，带领在场师生走进AI与数学深度融合的全新世界。

图丨讲座前文教授与同学们热情互动

本次讲座围绕“人工智能如何变革数学定理的发现与证明”展开，文再文教授从AI在数学证明中的最新进展出发，系统介绍了形式化数学的核心价值、技术路径与未来愿景。他指出，随着AI能力的飞跃，数学研究正从“人为主、机为辅”走向“人机协同”的新阶段，而形式化正是实现这一转变的关键桥梁。

图丨同学们聚精会神

“让机器像数学家一样思考，第一步是把‘显然’变成‘可检’。”文再文教授从一道本科不等式题切入：传统手写证明几行得证，Lean却需要 140多行形式化代码推导。正是这 140多行，把“灵感”拆成“公理”，也拉开了智能数学推理的序幕。

图丨文教授介绍Lean

报告上半程，文再文教授聚焦“数学优化形式化”。他给出团队最新成果：已将一部分数学优化理论分析，包括凸函数基本性质、最优性条件、梯度法和Nesterov 加速梯度法等算法的收敛性形式化，部分Lean代码已经被Mathlib4接收；一旦调用，即可零成本复用。“形式化不是炫技，是把脚手架留在建筑里，让后人继续往上盖房。”

文再文教授强调，形式化证明的最大优势在于其可验证性——每一步推理都可被计算机严格检验，杜绝人为疏漏。他展示了Lean等交互式定理证明器在“完美空间理论”“多项式Freiman-Ruzsa猜想”等前沿数学研究中的应用成果，令人耳目一新。

提问环节，老师、同学们围绕“对于AI for Math来说，自然语言推理和形式化推理，您更相信哪个会赢？”“Lean 如何入门”“AI 能否自动生成定理”等话题与文再文教授展开热烈讨论。文教授一一作答，并邀请大家会后试用在线形式化ReasLab IDE(https://prove.reaslab.io)，共同打磨下一代智能证明工具。气氛热烈，掌声不断。

图丨提问环节教授与同学热情交流

图丨合影留念

当“AI 的灵感”遇见“形式化的严谨”，数学不再是纸笔上的孤军奋战，而成了人与机器并肩的远征。文再文教授用一场报告提醒我们：定理的正确性可以被 Lean 一丝不苟地检验，猜想的火花也能被算法提前点燃。未来，谁拥有庞大而可信的形式化知识库，谁就握住了推动数学前沿、训练下一代大模型的“燃料”。也许不远的某一天，打开 ReasLab 提交的不只是作业，而是人类与 AI 共同署名的“下一页数学史”。