精选理由
陶哲轩的观察揭示了 AI 在数学研究中的新应用方向——将证明转化为可规模化的搜索问题，做数学研究或 AI 推理的开发者值得关注这一思路。
著名数学家陶哲轩（Terry Tao）指出，AI 正在推动数学证明的规模化生产。他将证明写作转化为搜索问题：AI 从目标出发生成数千个小引理，然后通过廉价验证器淘汰大部分，只保留少数有效的。这种方法使得大规模数学生产成为可能，改变了传统数学研究的范式。
AI 翻译 · 中文
著名数学家陶哲轩（Terry Tao）指出，AI 正在推动数学证明的规模化生产。他将证明写作转化为搜索问题：AI 从目标出发生成数千个小引理，然后通过廉价验证器淘汰大部分，只保留少数有效的。这种方法使得大规模数学生产成为可能，改变了传统数学研究的范式。
“I do see more and more mass-produced mathematics at scale." ~ Terry Tao AI makes this scalable. Will turns proof-writing into search problem: it generates 1000s of mini-lemmas from a goal, then cheap checkers kill most…