AI 写 Lean 证明的速度已快于 Lean 自身的检查速度

作者实测 OpenAI 公开的 AI 生成数学库，发现 AI 写 Lean 证明的速度已快于 Lean 能检查的速度。模型以每秒 1000 token 输出时在 95% 的文件上先于 Lean 完成，其中最贵的一个 450 行文件 Lean 单核检查需 2.6 小时、模型一分钟内即可写完。