**Weil 猜想被形式化：Axiom 在 Lean 中完成可复用证明**

_The Weil conjectures formalized in Lean_

> Axiom 项目利用 Lean 证明助手，成功将 Grothendieck 和 Deligne 关于 Weil 猜想的经典证明形式化为计算机可验证的结果。该工作基于 Mathlib 和 Stacks Project，实现了代数几何理论的逐步构建与复用，使这一深奥数学成果成为未来形式化证明的可靠基石。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：ai-models
- **发布时间**：2026-11-07 21:56（北京时间）
- **原文**：[打开原文](https://axiommath.ai/research/the-weil-conjectures-formalized-in-lean)