面向密码分析者的 Lean 形式化证明教程：从 Feistel 轮到线性求和恒等式
jedisct1 · x · 2026-10-30
Hosein Hadipour 发布教程《Lean for Cryptanalysts》，讲解如何用 Lean 4（配 Mathlib）为对称密码分析中的短数学论证编写机器可检的形式化证明。
要点：
- 动机：对称密码分析中的许多结论依赖简短数学论证（如连接两个区分器的恒等式、S-box 的性质），通常靠人工核查，归一化笔误或遗漏假设可能逃过作者与审稿人。
- 内容路径：从 Feistel 轮可逆性热身，再到形式化连接线性求和与积分求和的恒等式，读者可在编辑器里运行并改编到自己研究中的命题。
- 无需 Lean 背景，只需熟悉比特、分组密码与有限求和；含可下载的可运行教程（Lean 4.35.0、Mathlib v4.35.0）。
- 介绍了 Lean 三要素：定义、定理陈述、证明，以及 tactic 模式与 Infoview 面板的工作方式。
「研究」频道最新
- 一张图拆解 Mistral Large 4 等 9 个大 MoE 架构差异 — eliebakouch · 2026-10-30
- AI 科学发现算力成本原始出处补充，Navier-Stokes 花千万美元 — kimmonismus · 2026-10-30
- AI 科学发现算力账单曝光：Navier-Stokes 花掉上千万美元 — kimmonismus · 2026-10-30
- E2E-SWE 基准:186 个任务测 coding agent 从零构建可运行仓库,最好 pass@1 仅 67.7% — jyangballin · 2026-10-30
- LeRoPE 论文：把 RoPE 频率改为可学习参数，省 3.4% 算力 — eliebakouch · 2026-10-30
- ML Commons 推出「基准即服务」，试图终结刷榜时代 — RexDouglass · 2026-10-30