证明

以BenderSuzuki定理为证明终点为例，FormaTheoria形成了包含30298个数学声明、186187条依赖关系的证明网络，最长依赖链达458层，单次最长运行9.17天，历经数百次信息压缩维护庞大证明网络。

周源表示，可以说，近百万行代码背后是一张盘根错节、紧密链接的证明网络。

FormaTheoria则是直接从原始数学文献出发，自动梳理知识依赖关系，整合分散的数学知识，最终生成可由证明助手核验的形式化代码。

近日，在清华大学讲席教授丘成桐的倡导下，清华大学求真书院领军班聂天骄、张傲、汤瑀森，丘成桐数学科学中心副教授周源、智能产业研究院副研究员李鹏以及华威大学副教授DamianoTesta组成团队，提出了AI辅助形式化证明工作流FormaTheoria，这套工具直接从原始零散文献切入，自动梳理知识点依赖关系、整合碎片化数学体系，再通过形式化证明助手完成严谨核验。