Lean4 形式化验证的实现 文章介绍了如何借助 Lean 对密码学论文进行形式化验证，以降低对“专家口碑”的依赖。作者以 FRI 的简化分步健全性证明为例，说明论文已被转写为 Lean 代码，并由类型检查器保证定理可证。文中还分享了使用 Aristotle 与 Claude Code 协同完成形式化的过程、遇到的差异与后续计划，包括对接 Arklib、验证具体实现以及推动端到端正确性证明。 Lean形式化 FRI 零知识证明 定理证明 密码学论文 自动形式化 zksecurity 发布于 2026-01-27 188 0 0
