AI 生成数学反例出现在 Mathlib

littmath · x · 2026-07-15

转发内容称，Grothendieck 之前提出的一个问题——“是否每个 order 为 n 的有限局部自由 scheme 都会被 n 杀死”——现在已被证明为假。Akhil Mathew 在 Mathlib 里提交了一个反例 PR。原帖还提到，这份工作看起来是 **AI 生成** 的。