据报道，人工智能首次“形式化”证明了费马大定理——这一困扰人类358年的世纪难题，如今被AI转换成了计算机可验证的代码。但报道同时指出，“AI给出关键步骤，但尚无法逾越猜想的根本障碍”。

　　传统意义上，数学家的工作是“提出猜想—证明猜想”。怀尔斯1995年用150页论文证明费马大定理，靠的是人类独有的数学直觉和创造力。而AI做的，是把这份人类证明“翻译”成计算机可验证的形式化语言，生成上千万行代码，确保每一步推理都严密无误。换句话说，AI擅长的是“验证”，而非“发现”。

　　这就引出一个值得深思的问题：当AI越来越擅长验证和推导，数学家的核心价值在哪里？爱因斯坦说过，“提出一个问题往往比解决一个问题更重要”。AI可以在已知的框架内高效推理，但它无法像人类数学家那样，在纷繁复杂的现象中洞察出深刻的数学结构，提出全新的猜想和理论。

　　因此，数学家的角色正在从“证明者”转向“提出问题+验证者”。他们不再需要把大量时间花在繁琐的推导和验证上，而是可以专注于最具创造性的部分——提出新猜想、开辟新领域。而AI则成为强大的“数学工程师”，负责把数学家的直觉转化为严密的证明。

　　这种分工不是削弱数学家，而是解放数学家。正如计算器没有取代数学家，而是让他们从计算中解放出来去思考更深刻的问题；AI形式化证明也不会取代数学家，而是让他们从繁琐的验证中解放出来，去探索更前沿的未知。

　　未来的数学研究，可能是“人类提出猜想—AI辅助证明—人类审核验证”的新模式。当“数学家”变成“数学工程师”的指挥者，数学研究的效率和深度都将达到新的高度。（i科学）