srush 用 3000 行 Lean 从公理推导 MNIST，深学习前置数学只需半个学期
srush_nlp · x · 2026-10-29
Chollet 之外另一位知名研究者 srush（Sasha Rush）发布「Deep Learning Speedrun」项目：用 Lean 定理证明器从皮亚诺公理出发形式化推导出 MNIST 训练，回答「速通深度学习最少需要多少数学」。
- 结论：前置知识约为半个大一学期的高强度数学——取自哈佛 Math 55 教材并删去无用部分（积分等），线性代数完全不需要。
- 全程约 3000 行 Lean 代码，形式化对齐 Baby Rudin《数学分析原理》，从度量空间、拓扑一路推到「朝梯度反方向移动」。
- 起点是 Terence Tao 的说法「任何数学本科生都具备 LLM 数学前置」，作者戏称这就像说任何生物学家都有当短跑运动员的前置。
- 作者自嘲这篇博客是 AI slop，并好奇是否有人能用更短的证明完成同样推导。
所属事件:srush 用 3000 行 Lean 从公理推导 MNIST 所需数学(2 条相关)→
「研究」频道最新
- Signal65 新基准：一模型样本正确率 97%，完整任务却全军覆没 — ryanshrout · 2026-10-30
- TEM 问世：能量模型首次可扩展，声称多项能力超越扩散模型 — du_yilun · 2026-10-30
- VisualForce：从软夹爪形变推断力度，机器人无需力传感器也能捏莓果 — du_yilun · 2026-10-30
- CMU 团队 HALO 论文:人形机器人学会与不可预测的人类协作 — Scobleizer · 2026-10-30
- Apple 实习成果:视觉定位任务暴露视觉语言模型安全漏洞 — Cohere_Labs · 2026-10-30
- FreeView：无需干净参考图，自动过滤干扰视图做稳健 3D 重建 — zhenjun_zhao · 2026-10-30