Lean 4 形式化验证实战：从定理证明到可验证软件

课程简介

本课程深入讲解 Lean 4 定理证明器的核心用法，从基础语法到密码学协议的形式化验证。你将学会用数学证明而非测试来保证代码正确性——这是安全关键系统开发的核心能力。

学习目标

• 掌握 Lean 4 的依赖类型系统和函数式编程范式
• 能够编写和验证基础数学定理（交换律、结合律等）
• 理解策略系统的工作原理，使用 tactic 自动化证明搜索
• 完成一个完整的密码学协议形式化验证项目

章节概览

1. 第一章：Lean 环境搭建与基础语法
2. 第二章：依赖类型与类型驱动开发
3. 第三章：命题即类型——Curry-Howard 对应
4. 第四章：策略系统与自动化证明
5. 第五章：结构体与类型类
6. 第六章：密码学协议形式化：从定义到验证
7. 第七章：实战项目——一次性密码本（OTP）的正确性证明

适合人群

有编程基础的开发者，对函数式编程或形式化方法感兴趣。区块链开发者、密码学工程师和安全系统开发者将获得最大收益。