Axiom 在 Lean 中完成经典 Weil 猜想的机器验证形式化

Axiom 已在 Lean 中形式化了经典的 Weil 猜想。Lean 是一个逐步检查数学论证的证明助手。Alexander Grothendieck 和 Pierre Deligne 的标志性证明展示了几何如何支配有限域上多项式方程的解数。这些计数被编码在 zeta 函数中，其零点和极点决定了计数，正如 Riemann zeta 函数的零点支配素数的分布一样。在有限域的情形下，该证明解释了这些零点和极点的几何意义，并建立了 Riemann 猜想的类比。[2, 5, 10] 我们的工作使这些定理成为可由计算机检查的结果，供未来的形式化证明使用。它建立在 Mathlib（Lean 社区的数学库）以及 Axiom 对 Stacks Project 的形式化之上。[1]

这一成就体现了 Grothendieck 的“涨潮”数学方法：理解通过周围理论的发展而推进，逐渐将一个看似不可及的问题纳入可及范围。[9] Stacks Project 通过其组织与阐述展示了这种方法的力量。它将海量的代数几何内容统一为一个连贯的理论，进一步的结果从中涌现。我们的形式化映照了这一进程。深刻的数学并未消失；它变得可供复用，使下一个证明能够从先前工作的终点开始。

代数簇是由多项式方程定义的几何对象；它的点是这些方程的解。Weil 猜想关注的是有限域上的簇。对于素数 p，模 p 的整数构成一个有限域：两个整数表示同一元素当且仅当它们的差能被 p 整除。这个域有 p 个元素，允许加法、减法、乘法以及除以非零元素。更一般地，每个有限域都有 $q = p^m$ 个元素，其中 p 为某个素数，m 为正整数。将点的坐标限制在所选域中，就把寻找解的问题变成了一个有限计数问题。

令人惊讶的发现是，几何约束了可能解的数量。Emil Artin 和 F. K. Schmidt 的工作将曲线的算术与 zeta 函数（Riemann zeta 函数的有限域类比）联系起来。20 世纪 30 年代，Helmut Hasse 对椭圆曲线证明了一个引人注目的估计。椭圆曲线可以由非奇异三次方程表示，并包含一个无穷远点。若 N 表示某个有 q 个元素的域上的点数，则 当 q = 997 时，Hasse 界将点数限制在 935 到 1061 之间。20 世纪 40 年代，André Weil 将此结果推广到任意亏格的平滑射影曲线（亏格是类似于曲面柄数的的不变量），为这些曲线建立了 Riemann 猜想的类比。他的对应理论（曲线上的点之间的代数关系）将该估计归结为证明由这些关系构造的二次型是非负的。[2, 11]

1949 年，Weil 提出，一个远为宏大的模式支配着任意维数簇上的点数。固定一个有 q 个元素的域上的簇 X。对每个正整数 $r$，令 $N_X(q,r)$ 计数 X 在 r 次扩域上的点数，该扩域有 qʳ 个元素，同样的方程在其中可能有额外的解。以 T 为形式变量，这些计数定义了 zeta 函数： $$Z(X,q,T)=\exp\left(\sum_{r=1}^{\infty}\frac{N_X(q,r)T^r}{r}\right)$$ 对于有 p 个元素（p 为素数）的域上的椭圆曲线 E，zeta 函数具有特别简单的形式： $$Z(E,p,T)=\frac{1-a_pT+pT^2}{(1-T)(1-pT)}=\frac{(1-\alpha_pT)(1-\beta_pT)}{(1-T)(1-pT)}$$ 这里 $a_p=p+1-N_E(p,1)=\alpha_p+\beta_p$，且 $\alpha_p\beta_p=p$。Hasse 定理等价于 $|\alpha_p|=|\beta_p|=\sqrt{p}$：两个 zeta 零点的倒数位于半径为 p 的圆上。它们的和度量了点数对 $p + 1$ 的偏离；三角不等式恢复了 Hasse 界。这就是 Weil 在高维中寻求的模式。[11]

Weil 预测，对于平滑射影簇 X，zeta 函数 $Z(X,q,T)$ 是有理函数（多项式的商）。粗略地说，平滑意味着簇没有奇点；射影意味着它是射影空间的闭子空间，其中包含无穷远点。 令 $d=\dim(X)$，Weil 还预测了一个函数方程，将 $Z\left(X,q,\frac{1}{q^dT}\right)$ 与 $Z(X,q,T)$ 联系起来。通过变量替换 $T=q^{-s}$，在一个显式因子之外，这成为 s 与 $d − s$ 之间的对称性；对于曲线，它就是 Riemann zeta 函数熟悉的 $s\leftrightarrow 1-s$ 对称性。[11]

Weil 进一步预测，zeta 函数的多项式因子应反映相应复簇的拓扑，当两者通过良好归约相联系时：即在不引入奇点的情况下过渡到有限特征。最后，这些因子的根的倒数应具有精确规定的模。有理性、函数方程、拓扑比较和 Riemann 猜想构成了四个经典的 Weil 猜想。[2]

拓扑预测是非凡的。有限域上的点数应当恢复 Betti 数，后者计数不同维数中独立的拓扑特征。有限集上的算术正在探测连续几何空间的结构。

1959 年，Bernard Dwork 证明了无穷多个点数确实可以由两个有限多项式的商来编码。这就是有理性，是 Weil 猜想上的第一个一般性突破；他的论文于 1960 年发表。他的定理甚至允许奇点和非射影的簇。[3]

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）