皮埃尔·德·费马是一位17世纪的数学家。Lebrecht Music&Arts，YAY Media AS/Alamy 在伦敦市中心的一家酒店大堂，游客们正在为炎热天气中的观光做好准备。同时，工作人员正在为早餐后重新布置餐厅。在一个没有窗户的会议室里，聚集的学者们正在思考人类在数学未来中是否还有角色，因为人工智能现在可以自己证明定理。房间里的整体气氛是对计算机智能近年来的飞跃感到困惑，对其所解锁的潜力感到兴奋——也可能对他们个人未来的形势感到微微的不安。来自不同领域和国家的25位研究人员汇聚于此，花一周的时间利用最先进的人工智能模型来形式化费马最后定理。费马最后定理困扰了数学家们几个世纪，直到1993年安德鲁·怀尔斯证明了它。它声明没有整数 a、b 和 c 满足方程 aⁿ + bⁿ = cⁿ，其中 n 是大于2的整数。这个定理的表述极其简单，但证明却非常困难。现在，伦敦帝国学院的凯文·巴扎德正在进行一项五年项目，将怀尔斯的100页数学转化为名为 Lean 的计算机代码，以便能够正式检查其正确性，并作为进一步研究的基础。形式化数学定理将其从纸笔领域移出，并放入一个允许计算机处理的配置中，从而有条理地推理逻辑，暴露任何缺陷。目前，已经在一个名为 Mathlib 的中央库中存储了200万行形式化的数学内容。本次研讨会汇聚了数学家、计算机科学家和人工智能专家，希望他们能够推动巴扎德的项目，通过获取最新的人工智能模型来为费马最后定理的形式化做一些繁重的工作。小组围坐在笔记本电脑周围，每台电脑上显示着人工智能行业领先模型的不同界面。气氛热烈。预订了第二个房间，以便人们可以在安静的环境中工作，但该房间是空的。问题和子问题被分解、分发并由人类大脑引导和调控人工智能逐步解决。在研讨会之前，项目总共有20000行代码，巴扎德说，经过第一天的工作，这个数字已经翻倍。形式化费马项目于2024年获得资金，起初缓慢，巴扎德凭借手写代码缓慢推进。他说，自去年12月以来，人工智能模型与高级数学的结合能力似乎迅速提高，整个节奏大幅加快。然后在5月，由保罗·厄尔德什提出的一个80年老问题被机器解决，完全出乎该领域的意料。整个事件迫使巴扎德重新思考。他说：“我一直对成功充满信心。但是现在我们已经进行两年，人工智能的能力如此出色，现在我的本能是，这太荒谬了——我所说的事情太荒谬了。让我们做一些更好的事情。”怀尔斯的证明可能长达100页，但它依赖于20世纪60年代、70年代和80年代的约2000页数学。巴扎德的最初项目是形式化仅最后的论文——或者至少是其较新改进——但假设其基础上的一切都是正确的。如果整个定理集是一座金字塔，巴扎德本打算仅从90%的高度开始攀登，那里是最有趣的问题。但他现在认为可以从顶到底处理整个问题，以求完整。他极为自信，到他五年项目的结束时，他会完成他最初设定的目标。未来几年人工智能的进展、获取的成本以及本次研讨会的进展将决定他在金字塔其他部分的进展。帝国学院的苏航露是参与研讨会的研究人员之一。她在六个月前使用 ChatGPT 自学 Lean，现在在最前沿工作。她认识的大多数数学家仍然使用纸笔，因此这里展示的人工智能和形式化的应用完全不代表现在的领域，但她相信，这可能是其未来的一个缩影。苏说：“我觉得智力过程正在工业化。”她说：“如果说有什么的话，这些人工智能工具工作得如此优秀，感觉就像是：‘好吧，我们就让 [人工智能模型] Claude 工作，然后我们该做什么？’”这里使用各种工具，从免费的开源工具到来自美国初创公司的最新最贵模型。没有人能够准确说出在本次活动中花费多少资金来购买通行证，而大多数人一致认为，这很容易一天就要花费几千英镑。