GitHub
Lean 4：把硬件不变量草稿机械化
仓库做什么
Lean 4 是现代定理证明器与依赖类型编程语言。本站用它练习「先写清楚不变量，再填 sorry」的工作流。
推荐用法
- 从本站
/notes里的伪代码定理搬进真实.lean文件。 - 小步语义先在纸面/笔记定稿，再编码，避免边写边改规范。
- AI 可草拟 tactic 脚本；kernel 打勾前不算完成。
与课题的关系
协议级与算术数据通路中，有些性质更适合定理证明而非纯 BMC。Lean 4 是个人可维护的机械核对器选项之一。