什么是数学形式化证明?

数学论文里，一句“由此显然可得”可能省略了读者能够补全的推理；计算机却不能凭直觉接受这一步。数学形式化证明，就是在明确的形式语言、公理和推理规则下，把一个命题的成立写成可以逐步核查的逻辑推导。借助 Lean 等证明助手，这种核查可以交给计算机执行。

形式化究竟要明确什么

首先是命题本身：讨论的对象是什么，符号如何定义，需要哪些前提，最终要得到什么结论。其次是推理依据：每一步用了哪个定义、已有定理或逻辑规则，其适用条件是否满足。自然语言中依赖上下文理解的内容，在形式化时必须得到明确表达。

这不意味着所有基础细节都要反复手写。已经验证的定理可以复用，自动化程序也可以帮助补全推导。关键不在于人写出了多少步骤，而在于最终提交的证明能否通过检查。寻找证明可以依靠探索和猜测，接受证明则必须依据规则。

机器检查保证了什么

形式化证明不同于对大量输入进行计算测试。测试只能说明已检查的情形没有发现反例；证明则要说明，在给定前提下，结论为何对命题涵盖的全部情形成立。它也不同于让 AI 判断一段论证“看起来是否正确”：生成过程可以出错，检查器负责核验提交的推导是否合规。

但“通过检查”并不等于不附条件的绝对正确。它确认的是：在所采用的逻辑基础与假设下，形式化命题能够被推出。人仍需审查这个命题是否准确表达了原本的问题、是否遗漏关键条件或引入了不恰当的假设；检查软件本身的可靠性也属于信任基础。

形式化最费力的地方，往往不是把文字换成符号，而是补齐隐含条件、统一概念定义，并建立可复用的定理依赖。因此，阅读一项形式化成果时，比代码规模更重要的问题是：它究竟证明了什么，依赖什么，以及完整证明是否真正通过了机器检查。