Axiom Math 发布 Weil 猜想（I-IV）的 Lean 形式化证明

Axiom Math 宣布发布 Weil 猜想（I-IV）的 Lean 形式化证明，其中一项给出有限域上的黎曼假设。团队称这一成果是对其基础库的一次检验，用以说明基础库的可复用性——「基础库的真正考验是能在其上构建什么」，并借 Stacks 形式化展示在其之上的构建能力。