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 语言，我们得以用一种机器可处理的方式描述和构造数学定理，程序自动验证其有效性。并且这样的处理方式可以将复杂艰深的数学问题，以模块化的方式分解成更小的部分，这些部分可以在不必了解整个项目的所有方面的情况下进行探索。

他现在启动了一个叫做 Universal Algebra 的项目，构建一个巨大的程序化的数学定理集合，每个人可以贡献一小部分的定理，进行社会化的协作，形成具有广泛表达力的统一数学框架。未来能够以开源协作的方式创造新的数学知识。

这个工作极其重要，我能想到可比的例子是 20 世纪初希尔伯特提出 23 个数学问题，推动数学公理形式化的发展。