Stacks 项目,用 Lean 形式化
The Stacks Project, Formalized in Lean

原始链接: https://axiommath.ai/research/the-stacks-project-formalized/

然而随着该学科的发展,其基础文献变得浩繁,散见于成千上万页密集的专著与讨论班记录,其中大量以法文写成。该学科的大量实际知识也以不成文的传统知识形式,由导师传给学生。即使要定义代数叠——一种能够记住其所参数化对象的内部对称性的几何空间——也需要一整套涵盖交换代数、拓扑、层与上同调的艰巨先修知识。数学家们需要一部统一、自包含的参考书,将这些先修知识完整地写下来。

Hacker News 讨论了一个在 Lean 中形式化 Stacks Project 的项目。评论者将其与有限单群分类形式化作比较,指出 Stacks Project 广泛且组织严谨,而非聚焦于单个定理。一些人称赞其有用性,说 Stacks Project 在自然语言上类似 Lean,而另一些人质疑 AI 的作用、人类理解以及形式化细节。还有人混淆代数/几何 stacks 与软件 stacks。若干评论批评公告的 AI 生成措辞草率,而另一些人捍卫这一成就。总体而言,该讨论串反映了对 AI 辅助形式数学的兴奋、怀疑与辩论。
相关文章

原文

Yet as the subject expanded, its foundational literature grew vast, scattered across thousands of pages of dense monographs and seminars, much of it written in French. A great deal of the subject's working knowledge also lived as unwritten folklore passed down from advisor to student. Even defining an algebraic stack, a geometric space capable of remembering the internal symmetries of the objects it parametrizes, requires a formidable tower of prerequisites spanning commutative algebra, topologies, sheaves, and cohomology. Mathematicians needed a unified, self-contained reference where those prerequisites were written down in full detail.

联系我们 contact @ memedata.com