本文译自数学家陶哲轩（Terence Tao）个人博客，作者畅谈尝试使用Lean在泛代数领域开展机器辅助证明，以及号召广泛合作众包数学研究项目，源代码已在GitHub开源。（https://github.com/teorth/equational）
作者：Terence Tao（陶哲轩） 2024-9-25 译者：zzllrr小乐（数学科普公众号）2024-9-26 |
|---|
传统上，数学研究项目是由少数（通常是一到五名）专家级数学家进行的，其中每个人都足够熟悉项目的各个方面，可以验证彼此的贡献。由于需要验证所有贡献，组织更大规模的数学项目一直是一项挑战，特别是那些涉及公众贡献的项目；数学论证的组成部分中的一个错误可能会使整个项目失败。此外，典型数学项目的复杂性使得期望具有本科数学教育水平的公众，能够用有意义的方式为诸多此类项目做出贡献是不现实的。
出于相关原因，将现代人工智能（AI）工具的帮助纳入研究项目也具有挑战性，因为这些工具可能会“产生幻觉”，产生出看似合理但无意义的论点，因此在将其添加到项目中之前需要进行额外的验证。
证明辅助语言，例如Lean，提供了一种克服这些障碍的潜在方法，并允许涉及专业数学家、更广泛的公众和/或AI工具的大规模合作，为复杂的项目做出贡献，前提是它可以以模块化方式分解为较小的部分，无需了解整个项目的所有方面即可对其攻坚。目前，通过证明助手实现的此类大规模合作的主要例子，是对现有数学结果进行形式化的项目（例如对Marton的PFR（Polynomial Freiman-Ruzsa）猜想的最新证明的形式化，已在之前的博客文章中进行了讨论 https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ ）。目前，这些形式化大多是由人类贡献者（包括专业数学家和感兴趣的公众）众包的，但也有一些新兴的努力结合了更多的自动化工具（“过时的”自动化定理证明器，或更现代的基于AI的工具）来协助完成（仍然相当乏味的）形式化任务。
然而，我相信这种范式也可以用来探索新的数学，而不是形式化现有的数学。包括我在内的几个人过去组织的在线协作“Polymath”项目就是一个例子；但由于他们没有将证明助理纳入工作流程中，所有贡献必须由项目的人类主持人来管理和验证，这是一项相当耗时的职责，并且限制了进一步扩大这些项目规模的能力。但我希望证明助手的加入能够消除这个瓶颈。
我对使用这些现代工具同时探索一类多个数学问题，而不是当前一次只关注一两个问题的方法的可能性特别感兴趣。这似乎是一项本质上可模块化和重复性的任务，如果有合适的平台来严格协调所有贡献，它就尤其可以从众包和自动化工具中受益；这是一种以前的方法通常无法扩展到的数学类型（除非可能需要多年的时间，因为个别论文一次慢慢地探索该类的一个数据点，直到获得对该类的合理直觉）。除此之外，拥有大量要处理的问题数据，可能有助于对各种自动化工具进行基准测试，并比较不同工作流程的效率。
最近的一个此类项目的例子是“忙碌海狸”挑战赛（ https://bbchallenge.org/13132838 ），该挑战赛显示今年7月第五个“忙碌海狸数 ”BB(5) 等于 47176870 。一些较旧的众包计算项目，例如互联网梅森素数大搜索（GIMPS https://www.mersenne.org ），本质上也与此类项目有些相似（尽管使用更传统的工作而不是证明助手来证明）。我有兴趣听到任何其他现有的探索数学空间的众包项目的例子，以及这些例子中是否有与我在这里提出的项目相关的经验教训。
更具体地说，我想提出以下（诚然是人为的）项目作为试点，以进一步测试这一范式，该范式受到去年MathOverflow上的一个问题（ https://mathoverflow.net/questions/450930/is-there-an-identity-between-the-associative-identity-and-the-constant-identity ）的启发，并且没过多久在我的 Mastodon帐号上进行了进一步讨论（ https://mathstodon.xyz/@tao/110736805384878353 ）。
该问题属于泛代数（universal algebra）领域，涉及原群（Magma）简单等式理论的（中等规模）探索。原群只不过是一个集合 G 具备一种二元运算 ∘: G × G → G 。最初，此运算∘没有额外强加的公理，因此原群本身是有些无聊的对象。当然，通过额外的公理，例如恒等公理或结合公理，我们可以获得更熟悉的数学对象，例如群（group）、半群（semigroup）或幺半群（monoid）。在这里，我们将对（无常数）等式公理感兴趣，即涉及从运算∘以及G中的一个或多个不确定变量构建的表达式的等式。这种公理的两个熟悉的例子是交换公理
x ∘ y = y ∘ x
以及结合公理
(x ∘ y) ∘ z = x ∘ (y ∘ z)
其中x,y,z 是原群 G 中的不定变量。另一方面（左）恒等公理 e ∘ x = x 这里不会被视为等式公理，因为它涉及一个常数 e ∈ G （e是单位元），我们在这里不考虑。
为了说明我想到的项目，让我首先介绍原群等式公理的十一个例子：
例如，等式7是交换公理，等式10是结合公理。等式1常数公理，是最强的，因为它迫使原群 G 至多有一个元素；在相反的极端，等式11自反公理是最弱的，每一个原群都满足。
然后我们可以问哪些公理蕴含了哪些其他公理。例如，等式1蕴含此列表中的所有其他公理，而这些公理又蕴含等式11。等式8蕴含了等式9这种特殊情况，而等式9又蕴含了等式10这种特殊情况。完整的蕴含偏序集可以用下面的哈斯图（Hasse diagram）来描述：
这特别回答了MathOverflow 的问题：常数公理等式1和结合公理等式10之间是否存在中间的等式公理。
这里的大多数蕴含关系都很容易证明，但有一个重要的蕴含是在与前一篇密切相关的MathOverflow 帖子的回答中获得的（ https://mathoverflow.net/a/450905/766 ）：
命题1：等式4蕴含等式7。
证明：设 G 满足等式4，即对任意 x,y ∈ G，有
(x ∘ x) ∘ y = y ∘ x (1)
特别地令 y = x ∘ x ，我们得出结论
(x ∘ x) ∘ (x ∘ x) = (x ∘ x) ∘ x
因此，通过(1)的另一个应用，我们看到 x ∘ x 是幂等的：
(x ∘ x) ∘ (x ∘ x) = x ∘ x (2)
现在，在(1)中等号右边用 x ∘ x 替换x，然后应用(2) ，我们看到
(x ∘ x) ∘ y = y ∘ (x ∘ x)
所以特别地， x ∘ x 与 y ∘ y 可交换 :
(x ∘ x) ∘ (y ∘ y) = (y ∘ y) ∘ (x ∘ x) (3)
此外，两次应用（1），我们有
(x ∘ x) ∘ (y ∘ y) = (y ∘ y) ∘ x = x ∘ y
因此(3)简化为 x ∘ y = y ∘ x ，即等式7。□
可以在此处（ 文末Lean代码1 ）找到Lean中对上述证明的形式化。
我要指出的是，确定一组等式公理是否决定另一组公理的一般问题是不可判定的；参见Perkins这篇论文（ https://mathscinet.ams.org/mathscinet/article?mr=236012 ）的定理14。（这在本质上类似于众所周知的各种文字问题的不可判定性。）所以，这里的情况有点类似于忙碌海狸大挑战，在过去的某个复杂点上，我们必然会遇到无法解决的问题；但希望在我们达到这个门槛之前，会发现一些有趣的问题和现象。
上面的哈斯图不仅断言了列出的等式公理之间的蕴含关系；它还断言公理之间的非蕴含 。例如，如图所示，交换公理等式7不蕴含等式4的公理
(x + x) + y = y + x
要看到这一点，我们只需提供一个遵循交换公理等式7但不遵循等式4公理的原群示例；但在这种情况下，我们可以简单地选择（例如）自然数集 𝐍 与加法运算 x ∘ y := x+y 。更一般地，该图断言以下非蕴含 ，其（与指示的蕴含 一起）完整地描述了这十一个公理之间的蕴含 偏序集：
等式2 不蕴含 等式3。
等式3 不蕴含 等式5。
等式3 不蕴含 等式7。
等式5 不蕴含 等式6。
等式5 不蕴含 等式7。
等式6 不蕴含 等式7。
等式6 不蕴含 等式10。
等式7 不蕴含 等式6。
等式7 不蕴含 等式10。
等式9 不蕴含 等式8。
等式10 不蕴含 等式9。
等式10 不蕴含 等式6。
我们邀请读者提出反例来证明其中的一些蕴含。最难找到的反例类型是那些证明等式9 不蕴含 等式8 的反例：可以在此处找到解决方案（文末Lean代码2 ）。我在 Lean 中放置了所有上述蕴含和非蕴含的证明，可以在这个 github仓库文件中找到（ https://github.com/teorth/equational/blob/master/Equational/Basic.lean ）。
正如我们所看到的，仅计算11个等式的哈斯图就已经有些乏味了。我提出的项目是尝试将这个哈斯图扩展几个数量级，覆盖明显更大的一组等式。我建议的集合是使用原群运算∘最多四次，直到重新标记以及自反对称公理的的等式集合 ℰ ；这包括上面的十一个等式，但还包括更多。还有多少？回想一下卡特兰数（Catalan number） C_n 是n次二元运算∘的应用（应用于 n+1 个占位变量）形成表达式的方法数；并且，给定一串 m 个占位变量，贝尔数（Bell number）B_m 是为每个变量分配名称（直到重新标记）的方式数量，其中允许为某些占位变量分配相同的名称。因此，忽略对称性，最多涉及四次运算的等式数为
∑_{n,m ≥ 0: n+m ≤ 4} C_n C_m B_{n+m+2} = 9131
左边和右边相同的等式个数是
∑_{n=0}^2 C_n B_{n+1} = 1×1 + 1×2 + 2×5 = 13
这些都等价于自反公理（等式11）。其余9118个等式按对称性成对出现，因此ℰ的总大小是
1 + 9118/2 = 4560
我还没有生成此类恒等式的完整列表，但想必这可以用 Python 等标准计算机语言直接完成（我还没有尝试过，但我想得出来：与现代AI进行一些来回交流会生成大部分所需的代码）。
根本不清楚ℰ的几何形状会看起来像什么。大多数等式都无法相互比较吗？它会被分层到“强”和“弱”公理层吗？是否会有很多等价公理？现在记录任何关于这个偏序集结构的猜测，并将这些预测与之后项目的结果进行比较，可能会很有趣。
对偏序集 ℰ的暴力穷举计算，需要 4560 × (4560 - 1) = 20789040 次比较，看起来相当令人畏惧；但当然，由于偏序公理，我们很可能可以通过少得多的比较来判断偏序集中的等价性。我认为应该可以用向中央存储库（例如我刚刚创建的 github 存储库）提交各种等式之间的蕴含或非蕴含的Lean证明的形式，众包对这个偏序集的探索，这可以在Lean中进行验证，并根据记录所有当前状态（真、假或开放）的某些文件进行检查 20789040次 比较，从而避免多余的努力。大多数提交都可以自动处理，几乎不需要人工审核；并且偏序集的状态可以在每次提交后更新。
我想象有一些“唾手可得的果实”可以很容易地建立大量的蕴含（或反蕴含）。例如，等式2 或等式3 等定律或多或少完整地描述了二元运算 ∘，并且应该很容易检查4560个定律中有哪些可被这两个定律之一蕴含。偏序集 ℰ 具有与通过替换二元运算∘为它的反射 ∘ᵒᵖ: (x,y) ↦ y ∘ x 相关的反射对称性，原则上这将总工作量减少了大约两倍。原群的具体例子，例如带有加法运算的自然数集，满足ℰ 中的一些等式而不满足其他等式，因此可以用来产生大量的反蕴含。一些现有的等式逻辑自动证明工具，例如Prover9 和 Mace4（https://www.cs.unm.edu/~mccune/prover9/ 分别用于获得蕴含式和反蕴含式），可以用来处理大多数剩余的“简单”情况（尽管可能需要一些工作来转换输出给Lean）。然后，剩下的“困难”案例可以通过人类贡献者和更先进的AI工具的某种组合来解决。
也许，与形式化项目类似，我们可以拥有一个与项目的形式化Lean组件并行发展的半形式化“蓝图”。这样，该项目就可以接受不一定精通Lean的贡献者的人工编写的证明，也可以接受自动化工具（例如前面提到的 Prover9 和 Mace4）的贡献，这些工具的输出格式不同于Lean。然后，将这些半形式证明转换为Lean的任务可以由其他人或自动化工具来完成；特别地，我认为现代AI工具对于工作流程的这一部分特别有价值。但我不太确定现有的蓝图软件是否可以扩展，以处理该项目将会生成的大量单独的证明；由于这部分不会得到形式化验证，因此这里可能还需要大量的人工审核，并且这也可能无法适当扩展。与过去的 Polymath 项目本质类似，也许该项目的半形式化部分可以在像本博客这样的论坛上进行协调。
如果能将这样的项目，与某种以偏序集ℰ的不完整判定作为输入的图可视化软件集成，那就太好了（ℰ中的每一个潜在的比较 E ⟹ E' ，都被标记为真、假或开放），使用偏序公理尽可能地完成图，然后以视觉上吸引人的方式呈现部分已知的偏序集。如果有人知道这样的软件包，我很高兴在评论中听到它。
不管怎样，我很高兴收到有关这个项目的任何反馈；除了之前的请求之外，我还对改进该项目的任何建议感兴趣，并评估是否有足够的兴趣参与实际启动该项目。（我想象着按照Polymath项目的思路模糊地运行它，尽管可能没有正式标记为这样。）
参考资料 |
|---|
https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/
https://bbchallenge.org/13132838
https://www.mersenne.org
https://mathoverflow.net/questions/450930/is-there-an-identity-between-the-associative-identity-and-the-constant-identity
https://mathstodon.xyz/@tao/110736805384878353
https://mathoverflow.net/a/450905/766
https://mathscinet.ams.org/mathscinet/article?mr=236012
https://github.com/teorth/equational/blob/master/Equational/Basic.lean
https://www.cs.unm.edu/~mccune/prover9/
近期文章 |
|---|
· 开放 · 友好 · 多元 · 普适 · 守拙 ·
让数学
更加
易学易练
易教易研
易赏易玩
易见易得
易传易及
欢迎评论、点赞、在看、在听
收藏、分享、转载、投稿
点击左下角 阅读原文
查看原始文章出处
点击zzllrr小乐
公众号主页
右上角
设为星标★
数学科普不迷路！
