用Lean形式化验证One-Time Pad
Introduction to Formal Verification with Lean Part 1
形式化验证让数学证明从纸笔走向代码，通过机器检查确保绝对正确。本文以Lean为工具，手把手带你从零开始，将Dan Boneh和Victor Shoup的经典密码学教材中的One-Time Pad协议进行形式化验证。我们将定义BitString和XOR运算，证明其交换律、结合律等关键性质，并最终验证One-Time Pad符合Shannon Cipher的正确性要求。无论是对形式化验证好奇的密码学工程师，还是想重温基础的新手，这篇教程都能让你在编码中体验数学证明的严谨与乐趣。
形式化验证是一种工具，用于验证（数学）陈述的正确性；就像我们用纸笔写数学证明一样，我们实际上可以用形式化验证工具将证明写成代码并进行机器检查，从而确信证明是正确的。
HN 评论区
52- danabramov
Lean 超级酷。如果你好奇证明检查是如何工作的（在类型系统层面），我写过一篇相关文章：https://overreacted.io/beyond-booleans/
这里还有我写的另一篇文章，解释了公理在 Lean 中的作用：https://overreacted.io/the-math-is-haunted/
另外，这里有一篇关于 Lean 语法的长篇入门指南：https://overreacted.io/a-lean-syntax-primer/
最后，如果这些内容让你产生了一点兴趣，我强烈建议你玩玩 Natural Number Game：https://adam.math.hhu.de/#/g/leanprover-community/nng4
这是我见过的最好的 Lean 入门教程，而且它还能教你为什么 a + b = b + a。
- kccqzy
（作为一个感兴趣的小白提问）——这和 Python 里的 'assert' 语句有什么区别？
- mkw5053
https://www.amazon.com/Maths-Proofs-Lean-First-Steps-ebook/d... 我喜欢这位作者，之前发现他出了一本关于 Lean 的书！
不过最后我没法在电子书阅读器上读它，在电脑或手机上读又让通勤时变得很麻烦。所以我只读了前两章左右，但感觉挺有趣的。现在大家都在讨论用 Lean 做 AI 辅助证明，这让我很想重新捡起来学学。