印度天才数学家拉马努金，1887-1920

近年来，从 AlphaProof、AlphaGeometry 到 OpenAI、Gemini 在 IMO 竞赛中达到金牌水平，再到 Aristotle 系统在 Lean 形式化证明上的突破——AI 在数学推理领域的迅猛推进，给数学界乃至教育界带来了极其深刻的冲击。

非常自然，人们开始困惑：如果机器比人类更能算、甚至能证明困难的竞赛题，数学家的生存空间是否被压缩了？数学专业又该如何变革？

思考这些问题时，我脑海里浮现出两个具体的疑问。这得从一百五十年前的大天才数学家拉马努金（Srinivasa Ramanujan）说起。拉马努金一生留下了三四千个数学结果，多以公式、恒等式或方程的形式呈现。然而他的数学论断似乎是依赖神迹般的直觉，极少给出严密的证明，这些结论便以“猜想”的形式散落在他的手稿与笔记本中。

破解拉马努金遗稿，AI 能否大显身手？

我对拉马努金的认知十分有限，深度也就比电影《知无涯者》（The Man Who Knew Infinity）的情节稍多一点。但我“猜想”，如果将 AI 运用得体，在拉马努金猜想这个领域极可能大有所为。理由有三：

第一， 破译“私人密码”

拉马努金的手稿充斥着他的独特表达，对我们而言犹如远古代码。他习惯用一套只有自己懂的“私人符号”来表达极度深邃的结论。后人破译表明，他绝大多数看似荒诞不经的猜想，居然都是繁复而极其精准的真命题。AI 出场的第一重价值，就是扮演“译码员”，去解析和重构拉马努金的符号语言。

第二，海量算力与“暴力”验证

AI 能够不惜代价地运用暴力搜索（brute force），进行高精度的数值验证或寻找反例。这极其适合批量检验猜想公式，并在浩瀚的符号推演树中，自动寻找缺失的推导环节。

第三，形式化证明工具的技术赋能

拉马努金遗稿中充斥着大量复杂的级数、无穷连分数与模形式恒等式。上百年间全靠 Bruce Berndt 等学者，倾尽数十载心血逐一补齐逻辑证明。如今，借助 Lean 形式化证明系统（如 Mathlib 库），AI 能将这些颇为繁复的公式转化为严密的形式化逻辑代码；再结合符号计算（CAS）与自动策略搜索（Tactics），AI 能够在严格的逻辑公理框架下，自动补全恒等式两端复杂的代数变换与收敛性证明，大幅缩短人类学者人工校核的周期。

在以上这三件事上，AI 应该有用武之地。尤其在“破译密码”与“海量试错”上，AI 确实展现出了无与伦比的辅助威力。

宝山耶？无底洞耶？挖掘拉马努金，不适合所有人

这便引出了我的第二个思考。

大约十几年前，我的一位专攻解析数论的学生对拉马努金迷得不行，临近博士论文选题时跑来问我：“老师，我想以研究拉马努金的某个遗留问题作为博士论文，行吗？”

我看着他，沉吟了足足五分钟。答案在我心里清清楚楚，我只是在琢磨怎么才能不把冷水浇得太狠。最后我直率地告诉他：

第一，我不懂拉马努金，提不出高明意见；

第二，你若真能解出其中一个问题，水平绝对够得上博士论文；

第三，至于该不该把它当论文做？坦白说：不！设身处地，将心比心，我自己就不愿把大把青春耗在上面。我更希望你去做主流数学界关注的、活跃而有生命力的新课题。

幸运的是，我的这位学生情商也不低，与其论文导师相处融洽；那位导师非常尽责，在他进退两难时拉了他一把，将他引向密码学领域。方向正确，此人后来大有作为。

无独有偶，我还有个熟人也是读解析数论的，把拉马努金遗稿当成现成的“题库”，以为择一攻之即可。但他远没有我那位学生幸运，他的导师给足了自由，却没有给他认真的指导。虽然他最后拿到了博士学位，却没能解决任何真正的拉马努金猜想，只做了点外围的铺垫工作。这直接导致了他后来的学术困境——宛如孤身流落荒野，找不到像样的学术切入点。大问题啃不动，小问题发不出，高不成低不就，大半辈子都陷入了极其尴尬的境地。

事实上，拉马努金遗稿绝非无人问津的偏门古董，而是现代数论、模形式、组合数学乃至于量子物理学共同的“超级矿山”。在拉马努金这座宝山里挖出名堂的也大有人在，如 George Andrews、Bruce Berndt、Don Zagier，个个名震一方。

这就应了那句俗话：“没有金刚钻，别揽瓷器活。”拉马努金是“神仙”一般的存在，即使如今有了 AI 辅助，想要研究他的遗留问题，依然需要自知之明与量力而行。

结语

回到开篇的困惑。AI 的崛起带来了前所未有的算力与推演效率，能帮我们开采荒野中的宝山；但它终究无法代替人类做出战略性的学术抉择。

在 AI 能够轻松搞定‘计算’与‘补全推导’的时代，对年轻数学家而言，最核心的品质绝不再是‘做题家’式的硬啃孤题，而是在浩瀚的数学大海中，能够审时度势地选择真正具有生命力的方向。

工具越是强大，人的选题眼光与战略定力，反而越发成了不可替代的决定性力量。