工程师视角拆解 Lean 形式化证明：从正则语言说起
bibryam · x · 2026-10-12
作者将一本计算理论教材中的一道经典题目——用有限自动机证明某语言的性质——在 Lean + Mathlib 中完整形式化，并写成面向软件工程师的教程。
- 为什么选 Lean：Mathlib 已内置该问题所需的全部定理，是最省力的选择。
- 预备知识：文章先讲解 DFA（确定性有限自动机）与正则语言的背景，指出写正则表达式本质上就是在构造 DFA，并提到一个正则引擎 bug 曾搞垮大半个互联网的经典事故。
- 写作定位：作者刻意写得亲民，只要熟悉 TypeScript/Rust 这类静态类型语言、二进制算术、命题逻辑和归纳证明即可跟上，目的是让工程师体会「把一个非形式的构造性证明形式化」到底要付出什么。
- 与程序验证的关系：这类构造证明与日常的程序验证思路相似，全文展示了从非形式证明到 Lean 形式证明的完整转化过程。
「编程与Agent」频道最新
- TestSuiteBench:前沿编码 Agent 生成的测试套件抓不住一半以上逻辑缺陷 — OfirPress · 2026-10-12
- 观点：看不懂 agent 在干嘛，你会在产出前先破产 — noahsolomon · 2026-10-12
- Mole 1.16 发布：可一键清理 Claude Code、Codex 等 AI 工具缓存 — sujingshen · 2026-10-12
- 用 Codex 搭建照片筛选工具：按人脸与场景智能挑片 — banteg · 2026-10-12
- 只能让 AI Agent 提问的 AMA：一场 24 小时的 agent 交互实验 — metehan777 · 2026-10-12
- 哨兵agent拦截失控GLM，给agent上监控很有必要 — wunderwuzzi23 · 2026-10-12