OpenAI 10月6日把自家模型的成果放到GitHub上公开，一次放出722篇数学论文，约42%配上了能用机器核查的Lean正式证明，发布对象是数学界整条战线。

数学界没接招。美国数学家组织AHM当天发声明，说一口气放出七百多份不是学术能力的展示，是权力的展示，并号召数学家停止和OpenAI合作，陶哲轩第二天就把这份声明转上了自己的博客。

我看了一下仓库里的说明，他们自己写没正式化的那部分可能有错，上线第二天就撤了139和140两篇，还改了47号论文里的符号错误。论文现在成了跟软件一个待遇，挂着版本号，还留着撤稿记录。

AI能自己写数学了是真，可它写出来的第一批够不够硬，得数学界自己给说法。