作者近期完成了计算理论教材中的一道习题：利用有限自动机证明某语言的一个性质。这个非形式化证明属于构造性证明——先构建一个自动机，再证明它能识别该语言。由于这与程序验证颇为相似，作者决定尝试用Lean对该证明进行形式化。Lean是理想的选择，因为其数学库Mathlib已包含解决问题所需的全部定理。完成形式化证明后，作者撰文分享，旨在帮助软件工程师理解对系统属性进行形式化证明需要付出什么。文章面向熟悉现代静态类型语言（如TypeScript或Rust）、二进制运算、基本命题逻辑和归纳证明的读者，力求通俗易懂。文章首先介绍了确定有限自动机（DFA）与正则语言的背景知识：有限自动机是具有固定内存的计算理论模型，除理论价值外还有重要实践应用，如解析器和正则表达式引擎，曾有一个相关缺陷导致互联网大面积瘫痪。DFA是一种拥有固定有限状态集的机器，从左到右逐个读取输入符号，并根据确定性的转移函数更新状态；处理完输入后，若处于接受状态则接受输入，否则拒绝。作者以匹配整数字面量的正则表达式为例，构建了一个包含起始、符号、数字和死状态四种状态的DFA，并逐一解释各状态的行为逻辑与接受、拒绝条件。
事件分析
技术看点：本文展示了形式化方法平民化的趋势——借助Lean及其社区维护的Mathlib数学库，具备静态类型语言经验的工程师即可上手定理证明，上手门槛明显低于Coq、Isabelle等早期证明助手。产业层面，随着AI生成代码规模激增，传统测试手段难以充分保证正确性，形式化验证的价值正被重估；DeepMind的AlphaProof等系统已证明大模型可以在Lean中完成数学证明，AI生成、形式化验证可能成为高可信软件的新范式。自动驾驶、芯片设计等安全攸关领域对可证明正确的软件需求持续增长，Lean正从学术圈走向工业界。后续值得关注：Lean生态的商业化进展、AI辅助定理证明工具的成熟度，以及形式化验证融入主流软件工程流程的速度。
核心观点：形式化证明正从学术象牙塔走向工程实践，AI时代代码可信性将越来越依赖Lean这类证明工具。
原文链接：Hacker News
