AI正在改写数学研究中最稀缺的能力。
最近，AI连续为多个长期数学问题找到反例，并用Lean完成形式化验证。
反例天然适合机器搜索。一个普遍命题可能需要漫长证明，推翻它只需要找到一个满足全部条件的例外。大模型擅长生成候选结构，形式化证明器负责逐步验算。一个扩大搜索空间，一个把幻觉挡在结论之外。
这套组合改变了数学研究的成本结构。过去，稀缺的是推导能力和尝试次数；现在，机器可以生成百万行Lean代码。
新的瓶颈变成了问题有没有被准确翻译成形式语言、调用的定义是否符合数学家的原意、海量代码是否值得审查，以及一个反例背后究竟揭示了什么结构。
这也解释了为什么“代码通过编译”还不能等于“数学界已经接受”。Lean能证明某段代码没有跳步，却不能替人类判断这个形式化陈述是否抓住了原问题的全部含义，更不能自动给出可理解的新理论。
对数学家来说，真正危险的是仍把价值主要放在手工展开推导。下一阶段更重要的能力，是选问题、写规格、审机器、讲清楚。
AI可以更快找到反例，人类必须负责把反例变成知识。