陶哲轩让ChatGPT把复杂的数学论文翻译成Lean代码，与AI合作完成形式化证明。AI能理解论文、写出正确命题，却常在关键处卡壳。经过人机配合，终于生成1125行被验证的证明。这种「vibe coding」式合作，也让数学家重新思考：AI或许不是独立的解题者，却正在深刻改变数学研究的工作方式。 ...
