你有没有想过，如果有一天，计算机自己就能证明那些困扰人类几百年的数学难题，那数学家们接下来还能做些什么？在伦敦市中心一家酒店的会议室里，一群学者正在直面这个问题。窗外是热浪中的观光客，餐厅服务员正麻利地收拾着早餐台，而这间没有窗户的屋子里，气氛却有些微妙——既茫然，又兴奋，还隐隐夹着一丝不安。因为如今，AI已经能独立证明定理了，这让他们不得不重新掂量自己在数学未来的位置。
这次闭门工作坊召集了来自多个国家、不同领域的二十五位研究者，目标听起来有些疯狂：用最前沿的AI模型，把费马大定理“翻译”成计算机可以读懂的代码，让它彻底走出纸笔的范畴，变成一段段可被严格检验的程序。而牵头这个项目的，是伦敦帝国理工学院的凯文·巴扎德。他正在执行一项五年计划，要把安德鲁·怀尔斯1993年给出的那套一百多页的证明，塞进一个叫Lean的形式化系统里，好让计算机一点一点啃完，确认其正确无误，并以此为地基搭建更高的数学建筑。
费马大定理本身，就像数学世界里一座极尽蛊惑的迷宫。它表述起来简单得不像话：对于任何大于2的整数n，方程 aⁿ + bⁿ = cⁿ 绝不可能有全为正整数的解。你拿n等于2试试，那就是我们熟悉的勾股定理，像3²+4²=5²这样的例子随手就能写出一堆。可一旦指数跳到3、4、5……整个事情就变得截然不同。这个谜题从十七世纪被皮埃尔·德·费马潦草地注记在书边开始，足足让世上最聪明的头脑们空转了几个世纪，直到怀尔斯在1993年交出自己的解答，才算是尘埃落定。但问题并没有彻底结束：这份证明太过庞大复杂，人脑要审阅它，就像用肉眼检查一座摩天大楼的每一颗螺丝，谁也不敢拍胸脯说万无一失。
于是巴扎德想做一件只有我们这个时代才能做到的事——把这份证明全部“驯化”成计算机代码，让机器来当那个一丝不苟的检查官。这个过程，术语叫“形式化”。说人话就是，以前数学家们靠纸笔推理，每一步逻辑跳跃，读的人得靠默契和理解去填补那些“显然可得”的缝隙；而形式化之后，就相当于把一套老派的手写食谱，录成一台自动烹饪机接受的精确指令，没有“适量”，没有“翻炒至金黄”，只有克数和秒数。你得把每一步推理都拆解到计算机无法挑刺的程度，连最不起眼的桥段也要交代清楚，否则机器就会卡在那里，死心眼儿地报错。Lean就是这种证明助手之一，它像一个极度较真的助手，可以逐行逻辑推导，验算你说的每一个字，绝不通融。
更吸引人的是，形式化的数学还能“攒”起来共享。现在，一个叫Mathlib的中心仓库里已经沉积了超过两百万行这样严谨到牙齿的数学代码，涵盖了从基础算术到高等分析的诸多模块。而巴扎德的雄心，就是要把费马大定理这个巅峰之作也加进去，让它成为所有未来探索者可以直接调用的可靠积木。这个名叫“形式化费马”的项目在2024年拿到了资助，起步时巴扎德自己一行一行地手工编写代码，进展缓慢，像一只耐心啃穿厚木的蛀虫。
但拐点出现在去年十二月前后。他说，AI模型处理高深数学的能力仿佛忽然提速，整个节奏被一下子拽了起来。到了今年五月，又一件让学界措手不及的事情发生了：一个由数学家保罗·埃尔德什在八十年前提出的老问题，被机器彻底解决了。那意味着，计算机不仅能帮着检查证明，甚至能自己找出证明路径。这件事像一块巨石坠入平静的湖面，让坐在那间无窗会议室里的每一个人都重新掂量起了自己的角色。
工作坊里的景象由此变得格外生动。一群人分作几组，趴在笔记本电脑前，每台屏幕上亮着某种领先AI模型稍微不同的交互界面。机器提供可能的方向或代码块，人类则像导演一样不断抛出提示、拆分子问题，再把AI吐出的片段拼接、校正、验证。巴扎德透露，在这之前，整个项目已经累积了约两万行代码——这已经是相当可观的量了。但就在工作坊开始后的第一天结束时，这个数字就翻了一倍。空气里弥漫着一种嗡嗡作响的紧张感，以至于主办方原本为偏爱安静的人额外预订的第二间会议室，始终空空荡荡，没有一个人愿意离开这股集体冲刺的热度。
工作方式也很能说明问题。人们不再是从头到尾一行行码代码，而是把整个定理拆成层层叠叠的子目标，分发下去，每一颗人类大脑都在和AI模型协作敲凿，一点点啃掉那些顽固的步骤。有人负责将怀尔斯证明里的某个中间引理转写成Lean可以识别的逻辑，有人负责调试AI生成的代码片段里微妙的脱节，还有人专门思考怎么用一种更聪明的方式把问题“喂”给模型，好让它输出更靠近目标的结果。这种局面对人类数学家的要求其实更高了：你不仅得懂数学，还得懂得怎么和机器对话，怎么把一个深邃的想法掰开揉碎成机器能消化的颗粒，还要有足够的判断力
热门跟贴