标签
一篇由形式化领域顶尖研究者（Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash、Adam Topaz）撰写的客座文章，反思了人工智能在定理证明方面的飞速进展，对仓促开展的大规模形式化项目（如 Math, Inc. 的球体填充项目以及 Anthropic 对费马大定理的验证）提出警示，并勾勒了一个由社区驱动、追求高质量的数学形式化愿景。
Thomas Hales 为 Terence Tao 的博客撰写客座文章，介绍了数学家应该了解的 Lean 定理证明器相关知识，涵盖形式化证明的可靠性、mathlib 库的发展，以及 AI 驱动的自动形式化如何在 2026 年成为现实。
这是一篇面向软件工程师的教程式指南，在 Lean 定理证明器中形式化关于正则语言的一个构造性证明，逐步讲解规约、实现、归纳以及形式化证明的构成要素。文中展示了如何借助 Mathlib 中已有的定理，让开发者也能轻松形式化教科书中的自动机理论。
本文介绍了AViD Journal，一个使用Lean 4进行数学定理自动新颖性验证的管道，在撤回的arXiv论文上进行评估，并强调形式验证中的挑战。
PriorProof 提出了一种方法，通过分析 Lean 证明项相对于更早 Mathlib 快照构建的依赖足迹，来衡量形式化数学中证明技术的新颖性。该方法在 69.7% 的配对上与人类评分者达成一致，并提供可解释的分数差距。
本文展示了选择公理在证明空间中存在可测量的几何对应物，利用 Lean 4 的内核级追踪揭示了一个单参数混合律及其对神经定理证明器的操作意义。
陶哲轩演示如何使用 Claude Code 作为红队工具，将 Lean 代码风格对齐 Mathlib 官方风格指南，并以 Riemann–Stieltjes 积分的形式化项目为例，展示了 AI 在代码审计和风格对齐中的实用价值。