用Lean证明加法器：软件工程师指南

Anatomy of a Lean proof for software engineers

我最近尝试将计算理论教材中关于有限自动机的经典问题，用Lean语言进行了形式化证明。文章从DFA和正则语言的基础讲起，展示了如何构建一个加法器DFA来验证二进制加法性质。关键在于利用语言反转的闭包性质，将难以直接处理的从左到右读取问题，转化为从低位到高位处理的加法逻辑。通过拆解Lean证明的每一步，包括不变量、归纳步骤和状态转移，希望能帮助软件工程师理解形式化验证的核心思路，让抽象的数学证明变得像编写代码一样直观。