写给软件工程师的Lean证明解剖：从有限自动机到形式化验证

作者近期完成了计算理论教材中的一道习题：利用有限自动机证明某语言的一个性质。这个非形式化证明属于构造性证明——先构建一个自动机，再证明它能识别该语言。由于这与程序验证颇为相似，作者决定尝试用Lean对该证明进行形式化。Lean是理想的选择，因为其数学库Mathlib已包含解决问题所需的全部定理。完成形式化证明后，作者撰文分享，旨在帮助软件工程师理解对系统属性进行形式化证明需要付出什么。文章面向熟悉现代静态类型语言（如TypeScript或Rust）、二进制运算、基本命题逻辑和归纳证明的读者，力求通俗易懂。文章首先介绍了确定有限自动机（DFA）与正则语言的背景知识：有限自动机是具有固定内存的计算理论模型，除理论价值外还有重要实践应用，如解析器和正则表达式引擎，曾有一个相关缺陷导致互联网大面积瘫痪。DFA是一种拥有固定有限状态集的机器，从左到右逐个读取输入符号，并根据确定性的转移函数更新状态；处理完输入后，若处于接受状态则接受输入，否则拒绝。作者以匹配整数字面量的正则表达式为例，构建了一个包含起始、符号、数字和死状态四种状态的DFA，并逐一解释各状态的行为逻辑与接受、拒绝条件。

事件分析

核心观点：形式化证明正从学术象牙塔走向工程实践，AI时代代码可信性将越来越依赖Lean这类证明工具。