USTC Lean 讨论班入门指南 从零开始把数学定理敲给计算机看 Posted on 2026-05-13 每周固定时间，我们会在 USTC 数学楼里围坐一桌，盯着投影上一行行红蓝相间的语法 —— 这就是 Lean 形式化讨论班的日常。本文写给想加入但还不知从哪里下手的同学，也作为我自己的备忘录。 [Read More] Tags: Lean 形式化 讨论班