数学论文需要正式验证。这通常由评审员非正式地完成。但如果我们可以依赖更强大的东西，比如自动形式化到 Lean 4，其中评审员的角色将减少到对定义和定理的表述进行细致检查呢？自动生成代码的编译将成为证明证书。这就是我与 @HarmonicMath 一起进行的更长时间的实验中发生的事情。 感谢 @PietroMonticone 和 @llllvvuu 帮助设置蓝图。在这里，我展示了我朋友 Stefan Barańczuk 关于切比雪夫可分性序列的论文的完整正确自动形式化。代码大约有 5000 行高度非平凡的 Lean。它纠正了主论文中的所有不一致和漏洞（甚至证明了一些委托命题）。 我将发布一系列这样的实验，证明在某些数学领域，包括初等数论、组合数学和分析（所有 Mathlib 涵盖的内容），我们离证明有效性文档的重大转变并不遥远。我认为这将是一个忙碌的一年！