axiommath.ai 称已用 Lean 形式化代数几何参考书 Stacks Project
作者：林序
axiommath.ai 于 11 月 5 日发文，宣称把数千页的代数几何在线参考书 Stacks Project 用证明助手 Lean 形式化。目前这是单方说法：该帖在 Hacker News 只有 7 分、0 条评论，Stacks Project 官方与数学社区未见公开回应，团队背景与完成度也缺少细节。
axiommath.ai 在 11 月 5 日发文，称已把代数几何在线参考书 Stacks Project 用证明助手 Lean 形式化 。同一消息被提交到 Hacker News，目前反响冷淡。
Stacks Project 是代数几何领域一部免费在线参考书，篇幅数千页，由数学社区多年持续编写和维护，常被当作该方向的“超级教科书”使用。
“形式化”可以这样理解：把书里的证明改写成 Lean 能读的代码，再由计算机逐条核对每一步推理，而不是只靠人眼审读。若规模真有整本书那么大，这在数学界并不多见。
但现在还只是 axiommath.ai 的单方说法。Hacker News 上的相关帖子只有 7 分、0 条评论 。Stacks Project 官方和数学社区都没有公开回应，该团队的背景、形式化覆盖到哪些章节、完成到什么程度，也缺少可查的细节。
所以这条消息先当作待验证的进展看待，比当成定论稳妥。
转载说明
本文根据以下公开资料整理，原文及配图出处见下方。
0
评论 0
还没有评论，来抢沙发。