Browning–Sawin 猜想被证明：随机 ±1 系数超曲面几乎必然光滑，并由 AxiomProver 做条件化 Lean 形式化

Ken Ono 与 Ashvin Swaminathan 证明 Browning–Sawin 关于随机符号系数超曲面的猜想：对固定 n，n+1 个变量、次数 d、系数独立均匀取 ±1 的齐次多项式定义奇异复超曲面的概率为 O_n(d^{-1/2})，正维奇异 locus 的概率指数小；当 n≥3 时，绝对不可约性失败也满足指数小概率。论文摘要同时说明这些结果已由 AxiomProver 在 Lean 中形式化，但形式化以已有文献为输入。