Lean1 篇实战文章

前几天刷到陶哲轩 8 月 18 日的博客，说 Palomar 登记处正式开始接受 Lean 验证数学成果的提交了。这个东西由 Lean FRO 和 ICARM 孵化，定位类似一个面向 Lean 证明的预印本服务器，登记的是外部 GitHub 仓库的特定提交快照，不替你保管代码。