Sasha Rush 用约 3000 行 Lean 从公理推导 MNIST 训练所需数学

多伦多大学教授、Transformer 论文作者之一 Sasha Rush 发布「Deep Learning Speedrun」项目，以约 3000 行 Lean 从皮亚诺公理出发形式化推导训练 MNIST 所需数学。项目回应“训练 MNIST 最少需要多少数学”这一问题，并称相关深度学习前置数学大约只需半个学期。