https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/

这是一个难以置信的伟大开端，对于数学史，对于人类知识的探索。

当代最杰出的数学家之一，陶哲轩，这几年一直在探索定理证明器 Lean 语言，AI，以及用 AI 辅助数学定理的探索和证明，发表了很多博客。通过 Lean 语言，我们得以用一种机器可处理的方式描述和构造数学定理，程序自动验证其有效性。并且这样的处理方式可以将复杂艰深的数学问题，以模块化的方式分解成更小的部分，这些部分可以在不必了解整个项目的所有方面的情况下进行探索。

wow, this is super cool! terry tao always pushing the boundaries. can't wait to see what comes out of this project! 🚀