近日，我院邱东教授团队基于自主搭建的 Lean 自动化验证系统 Canto，完成了 Gauss–Bonnet–Chern 定理的完整形式化验证，并在开源平台 GitHub 发布。这一成果为形式化社区贡献了规范、可复用的微分几何基础代码，也为经典几何定理的机器验证提供了新的实践。
Gauss–Bonnet–Chern 定理由著名数学大师陈省身先生于1944年证明，揭示了微分几何中一个深刻事实：闭黎曼流形的 Euler 示性数（拓扑不变量）恰等于其曲率形式的积分（几何量）。这一定理开创了示性类理论与 Chern–Weil 理论，是其后 Calabi–Yau 几何、指标定理乃至整个现代几何学的语言，被誉为微分几何的枢纽定理。
形式化验证，简单说就是对数学证明使用计算机进行精准的验证。传统数学证明的验证依靠人工进行，周期较长、难免疏漏；形式化验证能做到逐逻辑推演核对证明过程，让数学结论在短时间内得到更广泛的认可，也为人工智能辅助数学发现提供可计算的知识底座。
此次形式化工作的代码依赖闭包总规模约 250 万行，横跨分析与几何两大板块。定理的证明涉及流形论、向量丛、联络与曲率形式等多层理论，此前在 Mathlib 中缺乏完整对应。团队新增的约 5 万行证明代码由系统 Canto 自动生成，并全部经 Lean 内核逐行检查通过，不含任何未完成的证明——规模之下，唯质量是求。全部代码按 Mathlib 社区规范组织：命名遵循社区约定，通用性强的构造（如曲率形式与陈类的基础理论）单独模块化，以便后续向上游贡献、被同行直接复用。
值得一提的是，团队还基于同一系统完成了 Hilbert 第17个问题的形式化工作。该工作的代码依赖闭包总规模约 97 万行，团队新增约 26,000 行证明代码，同样由系统生成并通过内核验证。该问题由数学家E. Artin于1927年运用实闭域与模型论方法解决，团队的这一工作也为模型论与实代数方向补充了相应基础。
当前，数智交叉融合已成为前沿科技攻关的核心方向之一。我院始终紧跟这一趋势：本学期开学首日，学院举办"人工智能与科学研究"专题研讨会，院长郭真华教授作《AI与科研新范式》专题报告；在学院"开学第一课"之"院长面对面"活动中，郭真华院长亦曾以"AI时代的学习变革与思维重塑"为主题与新生交流。邱东教授团队的这项工作，正是学院布局数学与人工智能交叉研究结出的具体成果——以规范、扎实、可复用的形式化基础设施，为人工智能时代的数学研究筑牢根基。
成果链接
GBC 项目仓库：https://github.com/pd4st8hb95-hub/gauss-bonnet-chern-lean
Hilbert 17 项目仓库：https://github.com/pd4st8hb95-hub/hilbert17-lean
项目主页： https://cantomath.cn/#research
排 版 | 桂美玲
一审一校 | 邱 东
二审二校 | 袁功林
三审三校 | 郭真华
