Lean证明助手的运作机制

Lean证明助手判断的不是一段论证“看起来是否合理”，而是形式化表达的结论能否由给定前提按逻辑规则推出。理解它的运作，需要区分两个环节：构造证明可以依赖人的洞察或自动化搜索，接受证明则必须经过严格检查。

从数学陈述到证明对象

自然语言证明常省略默认条件，例如变量属于什么集合、某个运算何时有定义。形式化时，这些信息必须明确写出，或能够由上下文无歧义地推导出来。否则，看似简单的推理也可能无法成立。

其逻辑基础可以用“命题与类型、证明与项的对应”来理解：待证命题对应一种类型，证明则是符合该类型的对象。检查证明，就是检查这个对象是否确实具有目标类型。这里的“对象”不是一句宣称，而是包含推导结构、可以接受规则检查的形式化表达。

自动化负责寻找，内核负责核验

实际交互中，用户不必手工展开所有底层细节。证明策略可以调用已有定理、拆分目标，或尝试补全推导。界面呈现的证明状态，通常包含当前可用的假设与尚未完成的目标；解决一个目标，也可能产生需要继续处理的子目标。

这些便利功能并不替代最终核验。自动化过程需要生成证明对象，再由内核按照逻辑规则检查。即使搜索过程复杂，或者证明由AI生成，也不能仅凭生成者的可信度获得接受。找不到证明，不等于命题为假；通过检查，也不等于无需审查命题本身。

后一个区别尤其重要：机器核验的是实际写下的形式化陈述。如果前提过强、定义偏离原意，或者结论被误写得更弱，正确的形式化证明仍可能没有回答原来的数学问题。复核时，应先核对定义、假设与结论，再检查证明所依赖的公理和已有结果。Lean的价值，是把推导是否合规变成可检查的问题，而不是替人决定究竟应该证明什么。