陶哲轩：AI 让证明变廉价，数学家的新工作是想象力

陶哲轩提出，AI 让证明变得廉价，数学家的角色需要转变，真正的瓶颈不再是证明，而是想象力。他给出五个方向：建设 Mathlib 这类数学形式化库，用 AI 探索新方法而不只是找证明，把定理拆解精简、检验是否仍然成立并探索相邻领域，撰写把各结果串联起来的教材，以及研究 AI 在何处失败。