用 Lean 4 形式化推导加法器：从行波进位到超前进位
satnam6502 · x · 2026-10-15
作者 satnam6502 发布了一份用 Lean 4 完成的推导：从行波进位加法器（ripple-carry）系统地推导出基于 Sklansky 并行前缀网络的超前进位加法器（carry-lookahead），所有变换均经形式化验证，代码与证明开源。
- 规格极简：第 i 列进位就是低 i 位加进位输入溢出 i 位
- 推导链条：full-adder 律 → scan 引理 → scan 融合 → scan1 → 并行前缀网络，深度从 n 降到 ⌈log₂(n+1)⌉
- gp(a,b) = (a∧b, a⊕b) 编码每列的 generate/propagate 位
- 附三张图逐步展示 carry chain → generate/propagate → (g,p) 扫描的结构演化
「研究」频道最新
- IFM 开源 RL360:8192 并发沙箱、130 万 rollouts 的 RL 基建 — rupspace · 2026-10-23
- 号称匹敌 GPT-6.1 的 DNA 模型遭实测打脸：10 例 8 例不如随机 — anshulkundaje · 2026-10-23
- AI 揭穿阴谋论研究风波落幕：Science 撤回关注声明，结论不变 — DG_Rand · 2026-10-23
- Embodied First Exam：一行代码在 44 台机器人上考你的 Agent — ManlingLi_ · 2026-10-23
- Anima Anandkumar 演讲：AI 气象模型胜超算，但不会取代科学家 — AnimaAnandkumar · 2026-10-23
- GLM-5.3-Flash 实现 1M token 上下文训练，较基线提升 64 倍 — AndrewLBeam · 2026-10-23