回顾刚刚过去的 2023 年,结出累累硕果的组合数学是最令世人瞩目的数学分支。在该领域里,全年中几乎每两个月便冒出一项令全球数学家叹为观止的重大理论突破。刚到 10 月份,今年在组合学方面的重要论文,竟然给研究和学习者一种“吃撑”的感觉:极值图论和拉姆齐理论、平面染色理论、平面密铺、不可传递骰子、加性组合以及被菲尔兹奖得主 W. T. Gowers 誉为组合学(可能的)第一猜想的“有限集合的并集猜想”,组合学中的各个子领域全面开花,统统取得了历史性的重大进展,甚至为有些课题画上了完美的句号!
关于集合的加法,有一个符合经验的直观洞见:如果集合 A 本身拥有很好的代数结构,则 A+A 的和集的规模(就是元素个数)与 A 相比,不会太“大”。
由这一观点出发,数学家 Kati Marton 应用逆向思维,提出如果 A+A 的和集足够小,则我们可以推知 A 所具有的代数结构。
把上面的思想用数学术语严格陈述,可以得到多项式 Freiman-Ruzsa 猜想:
如果 A 是一个特征为 2 的有限域 F 的子集,满足 |A+A|≤K|A| ,其中 K 是一个常数,那么可通过域上一个不大于 A 的子群的不超过 2*K^12 个陪集而将 A 覆盖于其中(原猜想表述里指数为未知常数,12 由最新论文所确定)。陪集的数量很可能非常大。但这是 K 的多项式,不至于随 K 的增大而指数级增长。
Kati Marton 悬挂在布达佩斯 Renyi 学院走廊上的照片。|图源:Gil Kalai的博客Combinatorics and more: Image (wordpress.com)
Marton 是出生于匈牙利的数学家,因其在信息论、concentration of measure(随机变量取值集中的现象)、概率论和遍历理论方面的研究而闻名于世。在对 concentration of measure 研究中,Marton 巧妙地引入信息论和熵的概念,获得了一个简短的精彩证明。在多项式 Freiman-Ruzsa 猜想的证明中,类似于上面的熵方法似乎扮演了重要的角色,这一点真是再恰当不过了。
或许,抗拒这一潮流的唯一内源性力量是,形式化论文本质上是把部分审稿成本转移到论文作者的身上——我们为了向学界“自证”,就需要再掌握一门编程语言 Lean(或未来取代它的语言),并且要花时间形式化自己的数学论文。但是,在 2022 年以后,似乎学习使用新的编程语言不再是什么沉重的负担。因为大语言模型的出现,现有 AI 在其它方面或许帮助有限,但是在辅助编程方面,则可以带来极高的增益。而随着相关技术的进步。这种AI助手只会越来越强。同时,相关语言,如 Lean 也会迭代得更加灵活,方便。
未来的发展,无论是计算机辅助证明工具,还是各类型的 AI ,最终目标都是对数学定理的自动化证明。现在的 Lean 本质上还是一种传统的计算机辅助证明工具,其核心是形式化证明。它不是当前主流的生成式 AI 和 CoT(思维链)可自动推理的大语言模型。形式化证明的概念已经存在很久了,与基于大模型和生成式方法的当前人工智能是完全不同的概念。当然,即便是后者,目前也无法独立完成真正意义上的数学证明。在将 Lean 语言与 AI 结合的过程中,除非有一天 AI 能够创造性地自动完成 Blueprint 和 Lean 中的关键创造性步骤,否则我们也无法将这种工具称为具备数学能力的人工智能。
Lean 的最新版本是 Lean 4 。它的目标是提供一个高效、可扩展、可靠的平台,用于形式化数学、验证软件和硬件,以及开发通用的函数式程序。我在这里分享一本开源教程 Mathematics in Lean(链接见参考资料 6)。
参考资料
1. [2311.05762] On a conjecture of Marton (arxiv.org)
2. Marton's “Polynomial Freiman-Ruzsa” Conjecture was Settled by Tim Gowers, Ben Green, Freddie Manners and Terry Tao < Combinatorics and more < Reader — WordPress.com
3. Additive Combinatorics | Van Vu (yale.edu)
4. On a conjecture of Marton | What's new (wordpress.com)
5. ‘A-Team’of Math Proves a Critical Link Between Addition and Sets | Quanta Magazine