面向软件工程师的 Lean 证明剖析：用 Lean 形式化验证 DFA 加法器识别二进制加法语言

一位软件工程师用 Lean 及其 Mathlib 形式化验证了 Sipser《计算理论导引》习题 1.32：证明由三比特列组成的语言 B（底行等于上两行之和）是正则语言。作者通过构造加法器 DFA 并证明其恰好接受 B 的逆 BR，再借助正则语言反转封闭性完成证明，旨在向软件工程师展示形式化验证系统属性的完整过程。