从 AI for Math 的进展，到“闭包论”与证明超图

本文写于 2026 年 8 月 2 日。“闭包论”并不是数学界已有的正式流派，而是本文为一组常见观点取的名字：AI 目前主要在既有定义、定理和技术的范围内搜索、迁移与组合；只有发明新的普适方法，才算真正把数学的边界向外推了一步。

闭包给出数学的边界，真正决定可达性的则是边界之内的道路与桥梁。

这两年 AI 在数学领域的进展，快得甚至让人有些不适应。

2024 年，AlphaProof 和 AlphaGeometry 2 在当年的国际数学奥林匹克（IMO）上拿到 28 分，踩线达到银牌标准。它们解出了六道题里的四道，其中还包括一道全球只有五名参赛者解出的难题。不过当时还需要人工将题面翻译成形式语言，并且部分题目耗费了数天的计算时间。^[1]

到了第二年，Gemini Deep Think 已经可以直接阅读自然语言题面，在 4.5 小时的标准比赛时间内独立做出五道题，拿下 35 分，经评审打分达到了金牌水平。^[2] 当然，能做竞赛题并不意味着系统已经具备了成熟数学家的研究能力。毕竟竞赛题目的边界是固定的、结论是确定存在的，而真正的研究则需要在茫茫未知中选择问题、建立概念。但即便如此，“机器只能进行机械推导”这种断言，显然已经不符合现实了。

这种变化很快从竞赛延伸到了科研一线。2025 年，研究者 Uijeong Jang 与 Ernest Ryu 发表了关于 Nesterov 加速梯度法点收敛问题的一份辅助证明，并明确指出 ChatGPT 在研究过程中起到了关键作用。Ryu 曾谈到，模型并没有凭空发明新的数学原理，它真正的优势在于调动已有的知识库，从相邻领域中找出来研究者未必能立刻联想到的方程、论证和跨学科联系。模型给出的方向绝大多数是错的，但其中一个不完整的结构性建议被研究者捕捉到并加以修正，最终构成了证明的核心主线。^[3][4]

真正改变讨论气氛的，是 2026 年夏天接连出现的两个结果。

7 月，OpenAI 公布了一份循环双覆盖猜想（Cycle Double Cover Conjecture，简称 CDC）的证明。说明中写道，证明由 GPT-5.6 Sol Ultra 得出，Codex 参与整理成文。此后，Sang-il Oum 与 Jim Geelen 很快分别写出了独立的讲解版本，帮助共同体检查和消化这份证明。^[5]

约十天后，Levent Alpöge 宣布，Claude Fable 5 找到了雅可比猜想（Jacobian Conjecture）的一个三维反例。这个反例很短，检查也不困难，并很快被人工写入 Lean 验证；不过二维情形至今仍然开放。^[6]

这两个结果的形态很不一样。CDC 的工作是一份完整证明：它把若干已有定理重新组织起来，找到了一条此前无人走通的短路线。雅可比猜想则是一个决定性的反例：困难主要不在验证，而在于从巨大的候选空间中找到那个过去没有人注意到的对象。它们未必都意味着 AI 已经发明了全新的普适数学技术，却也很难再被简单归入“机械复述”或“照搬已有证明”。

紧接着，2026 年 8 月初，OpenAI 又集中公布了十项涵盖高维几何、编码理论、群论和理论计算机科学等方向的研究工作，并附上论文稿和由 Lean 核验的形式化证书。^[7] 这些材料刚刚进入公开检验，具体价值仍有待数学共同体逐项审阅。但讨论的重点已经明显改变：人们不再只问 AI 能不能解题，而开始追问，它找到的证明、反例和中间结构，究竟算不算新的数学知识。

正是在这样的背景下，一种关于 AI 数学能力的判断逐渐变得常见。本文暂且把它称作“闭包论”。

一种很有吸引力的判断

数学家 Thomas Bloom 在谈论 FrontierMath 开放问题基准时，用过一个很形象的说法。他认为，数学高度专业化，不同领域像一根根不规则伸出的尖峰；我们已知知识的“凸包”内部仍有许多空隙。AI 很善于跨越专业边界，把相距很远的文献和技巧接在一起，因此能够填补这些空隙。真正悬而未决的问题是：它能否越过现有“凸包”的边界，发明新的方法。^[8]

这不是孤立的看法。Timothy Gowers 认为，AI 可能很适合执行那些“在根本上算常规、对具体研究者却不常规”的技术：不是因为步骤本身深不可测，而是因为个人不可能同时熟悉所有子领域。Terence Tao 设想，机器可以批量检查上百万个候选命题，让数学带上一部分实验科学的色彩；Evan Chen 则强调它在跨领域检索、猜想生成和降低专业门槛方面的潜力。^[9]

这些数学家并没有组成一个观点完全一致的阵营，也没有共同使用“闭包论”这个词。但他们触及了同一条界线：

调用已有知识，与创造新的数学技术，是否是两种本质不同的贡献？

围绕这个问题，大致形成了两种不同强度的观点。

弱版本的“闭包论”是一种对经验事实的描述：到目前为止，AI 的成功确实主要依赖于已有的定义、定理、证明套路以及跨领域的检索与迁移。它或许能用人类未曾预料的方式组合这些材料，但组合所用的零部件大体上早已存在。

而强版本的“闭包论”则多推了一步：只要一个结论原则上能由既有技术推导出来，它就没有真正增加数学知识；唯有发明全新的方法，才算实质性地拓宽了数学的边界。

前一种观点基本符合事实，也提出了有价值的思考；但后一种观点却混淆了两个概念：一个结论“在原则上是否逻辑可达”，与人类“是否拥有一条足够清晰、简短且可复用的路径去实现它”，完全是两回事。

要理清这个区别，得先看看到底什么是“闭包”。

从“技术凸包”到“演绎闭包”

有数学家曾把已知知识比作一个“技术凸包”，认为 AI 只是在填补这个凸包内部的空隙。这个比喻很形象，但从严格的数学角度看并不算贴切。^[8:1] 凸包是定义在向量空间里的，点与点之间可以做加权平均；但数学技术并没有天然的坐标系，“三成归纳法”加“七成傅里叶分析”并不会自动融合出一项新技术。

更正式的概念叫演绎闭包。

给定一批前提、定义和公理，再规定允许使用的推理规则，把从中能够证明的所有命题收集起来，就得到这批知识的演绎闭包。若把原来的命题集合记作 $S$，它的演绎闭包可以记作 $Cn(S)$。Tarski 对“哪些结论能由哪些前提推出”这一关系的抽象研究，给出了这类算子的标准性质；逻辑学把这种关系称作后承关系。^[10]

其中最重要的一条是：

$$Cn(Cn(S))=Cn(S).$$

意思很朴素：既然第一次已经把所有能推出的结论都收集齐了，再对这些结论做一次同样的推导，不会得到更多东西。闭包是幂等的——“幂等”只是说，同一操作做第二次，结果和第一次相同。

因此，如果一条新定理本来就能由旧理论证明，那么把它加入旧理论，并不会改变无穷资源下的最终可证明集合。就这个狭窄而严格的意义说，闭包论没有错。

问题在于，演绎闭包对每个命题只保留了一个最粗糙的信息：这个命题究竟“可证”还是“不可证”。

它不记录证明过程有多长，不记录使用了哪些中间想法，不记录搜索时踩过多少坑，也不记录某个中间引理是否具备被上百个问题重复调用的价值。两套数学知识库在逻辑闭包的角度看可以完全等价，但在实际的可读性、可搜索性以及解决现实问题的能力上，却可能天差地别。

把这些差异简化为“可证”与“不可证”，就像评估交通网络时只看两地是否连通。盘山公路、乡村小路和高速铁路在这个指标下给出的答案都一样：能到。但对真正需要出行的人来说，三小时与三个月显然不能混为一谈。

数学知识不只是命题清单

这种质疑并不是为了回应 AI 才临时提出的。

数学家 William Thurston 曾专门写文章强调，数学的实质性进展并不能仅仅归结为定理和公式的叠加。一个领域真正发生质变，往往是因为人们形成了新的视角、直觉与语言，开始明白哪些问题才值得追问，哪些结构应当放在一起观察。^[11]

Yehuda Rav 的观点则更进一步：普通数学证明本身就是数学知识的核心载体，它所蕴含的认知价值远远超出了最后写下的那行定理陈述。^[12] 同一个命题，无论是代数证明、几何证明还是概率证明，在“是否成立”这一点上没有区别，但它们却能分别通向截然不同的研究方向。

做一个简单的反思就能发现：如果“处于旧理论的演绎闭包之内”就意味着没有新知识，那么现代数学的大多数成果都会被取消资格。数学的发展很少依赖于频繁更换基础公理；新定理之所以新，通常不是因为它跳出了原有公理体系，而是因为此前没人找到可行的推导路径，或者没人看清推导背后的统一结构。

换句话说，演绎闭包描述数学的逻辑边界，却没有描述数学内部的道路。

要谈 AI 对数学的作用，我们需要一张地图，而不只是一圈边界。

证明超图：把证明重新放回图中

一种更合适的模型是证明超图。

先从普通的图说起。地图上的城市是节点，道路是边。一条普通边连接一个起点和一个终点。证明却经常需要同时使用多个前提：知道 $A$，再知道“$A$ 可以推出 $B$”，才能得到 $B$。这不是一条单独前提通向结论的边，而是一组前提共同通向一个结论。

能够一次连接多个起点的边，叫作超边。这个名字听起来很重，含义却很简单：普通边像“从甲地到乙地”；超边更像一道菜谱，面粉、水和酵母必须一起到位，才能得到面包。

于是可以把数学画成下面的样子：

前提 A ─┐
前提 B ─┼──［一次推理］──► 中间结论 L ──► 目标 P
前提 C ─┘                         └──────► 目标 Q

超边允许多个前提共同导出一个结论，中间结论还可以被后续证明复用。

为方便叙述，可以把节点看作命题。严格一点说，节点应当是“带着当前假设的命题”，因为同一句话在不同前提下不是同一个证明状态。每条超边表示一次合法推理，或者一次对已有定理的调用。

一份证明也不应被看作一条单向延伸的直线，而更像一棵树：各个分支分别推导不同的前提，最终汇聚到结论。若某个中间结论能在不同地方复用，整份证明就会形成一张有向无环图（DAG）。

2026 年，Maissam Barkeshli、Michael Douglas 与 Michael Freedman 在一篇预印本中提出了相近的整体图景：形式数学可以看作一个有方向、有次序的证明超图，节点是可证明的陈述，超边把一组输入命题组合成输出命题。^[13] 这个想法并非凭空出现，逻辑论证的图形表示有很长的历史；它的价值在于，把“证明结构”从单纯的可证性中重新分离出来。

这里还要区分两张图。理想化的“全图”包含一个形式系统里所有可证命题和所有可能证明；在这张图里，新发现并没有凭空创造原先不存在的逻辑道路。人类和 AI 实际拥有的却只是其中一小块：已经发现、命名、整理并能被检索的知识库。数学研究主要改变的是这张可访问的子图。一个证明即使早已存在于理想化全图中，只要过去没有主体能够找到、压缩或利用它，它对现实数学仍然不是现成资源。

现实中的知识库只是理想化全图的一部分；新枢纽会把原本分散的区域连接起来。

距离比连通性更有信息

既然把数学表达为一张网络，下一步自然需要给其中的道路标上“成本”。

一条证明步骤的成本可以包含很多维度：写下它所需的推导步数、计算机检索的时间、验证所需的资源，或者一个数学家理解它所需的背景知识。尽管这些成本难以用单一的数值精准衡量，但我们可以直观地将从已知出发到达目标命题的最小代价，称为该命题的“证明距离”。

假设现在有人证明了一个全新的中间引理 L。在静态的逻辑闭包看来，什么都没有改变——L 本就在理论可推导的范围内。但在证明网络中，这个引理把一段极其繁复且频繁出现的推导过程，压缩成了一个可以直接调用的节点和一条低成本的快捷通道。

这很像在两条原本需要绕行数百里的河岸之间架起了一座桥。修桥并没有创造新的陆地，也没有在逻辑上第一次实现“连通”，但它把原本难以承受的出行成本降低到了现实可行的范围。交通路线变化后，周围的物资流动和区域分工也会随之发生重塑。

重要引理像桥梁：不改变逻辑连通性，却显著缩短现实中的证明距离。

数学中的优秀引理，扮演的就是这种桥梁的角色。它的核心价值不只在于自身被成功证明了一次，而在于它提供了一个无需每次都重新展开的思维模块。一旦被反复调用，它就成为了数学公共基础设施的一部分。

有限预算下，可达范围会改变

演绎闭包默认推理者拥有无限时间、无限内存，并且最终能找到一切存在的证明。现实中的数学家和 AI 都不是这种逻辑全知的主体。

设一个研究者只能花费预算 $B$。预算可以是三个月、十万次搜索，也可以是一个人能够掌握的认知负担。把成本不超过 $B$ 的命题收集起来，可以写成：

$$F_B=\{P:\text{存在一份成本不超过 }B\text{ 的证明}\}.$$

完整演绎闭包不变，并不妨碍 $F_B$ 大幅扩大。

假设某个目标需要同时依赖三个中间结论。虽然它们各自都可证明，但证明合在一起超过了预算。一个新引理若能同时缩短这三段论证，目标就会第一次进入实际可操作的范围；随后，这个目标本身又能成为新的引理，继续缩短其他证明，由此引发知识的级联生长。

所以，人类并不是对同一个固定集合机械地“再取一次闭包”。每一次重要发现都会改变可调用的定理库、命名方式、搜索索引和问题表示。下一轮推理面对的，已经不是上一轮那张图。

引理、切规则与“把证明展开”

证明论中有一个与此非常接近的概念，叫作 cut，通常译作“切”。不必记住形式规则，只需把它理解为：

先证明一个中间命题 $L$，再把 $L$ 当作引理去证明最终结论。

许多逻辑系统都有“切消去”定理：即使不允许使用这个中间引理，原则上也能把整份证明重新展开，直接从最初前提推到结论。于是允许引理和不允许引理的系统，可以证明同样多的命题。

可“能展开”不等于“展开后同样好”。把一个被多处调用的引理全部内联，就像把程序中每次函数调用都替换成整段函数源码。结果可能急剧膨胀。George Boolos 那篇著名的文章干脆以《不要消去切》为题，展示了中间引理对证明长度的巨大影响。^[14]

证明复杂度研究把这种区别做得更精确。Cook 与 Reckhow 奠定的框架，不只问两个证明系统能否证明相同命题，还问一个系统中的短证明，能否在另一个系统里保持短小。^[15] 后续研究给出了明确例子：允许共享中间结果的网络式证明可以保持线性规模，而强迫每个分支重复展开的树形证明却需要指数级长度。^[16]

这说明“闭包相同”与“实际可用的证明能力相同”之间隔着很大一段距离。前者只关心终点是否存在，后者关心道路是否能够被真正使用。

Proof nets：证明不等于书写顺序

Jean-Yves Girard 的 proof nets——通常译作“证明网”——提供了另一个重要视角。

传统证明经常按一行接一行的顺序书写，但许多步骤彼此独立，先写哪一步并不重要。交换两个独立步骤，纸面上的证明会变成另一串文字，内在依赖关系却没有变化。Girard 发展证明网，正是为了把这些偶然的书写次序剥掉，让证明真正依赖哪些前提、哪些部分可以并行，更直接地显现出来。^[17]

证明网和本文所说的证明超图并不完全相同。证明网主要观察一份证明内部的结构；这里的证明超图还想描述整座数学知识库：哪些定理被命名，哪些结果可以跨证明复用，哪条路容易被搜索到，某个新概念会把多少远处的区域拉近。

两者共享的核心态度是：

不能只保留“有证明”这件事，而把证明的形状全部抹掉。

“在闭包内”到底还可以新在哪里

在证明网络的视角下，数学创新实际上展现出了不同的层次。

最直观的是发现“新终点”——证明了一个此前无人知晓的命题。它或许仍在既有的逻辑闭包内，但在人类已探索的地图中属于全新的节点。

第二种是找到“新路径”——为已知定理给出更简短、更初等或更能揭示本质的新证明。终点没有改变，但道路的性质变了。

第三种是建立“新枢纽”——发现一个能被多个后续问题频繁调用的中间引理。它本身或许并不惊人，却能显著降低周边大片区域的证明距离。

第四种是引入“新坐标系”——提出一种新的定义或问题表示方式，使原本纷繁复杂的现象显现出统一的结构。这类新定义通常并不改变理论的逻辑边界，但它能从根本上改变研究者的思考习惯。

最后一种则是发明“新造路法”——即提出一种通用的证明策略，它不只是修通某一条具体的路，而是给出了一套批量生成道路的方法。这正是数学界通常所说的“新技术”。

“闭包论”高度关注最后一种创新，这种侧重有其合理性，因为普适的方法通常比孤立的结果更有价值。但如果把前四种创新一概归结为“闭包内的重复劳动”，就低估了数学知识的组织形态。许多后来成为基础设施的概念，最初并没有扩大逻辑上的可证范围，它们改变的是哪些证明能够被人类看到、理解并继续使用。

但捷径也不自动等于理解

降低证明距离固然关键，但它本身并不能作为衡量数学价值的唯一尺度。

设想有一个黑箱，只要输入任何真命题，就直接回答“成立”。从图论上看，它为每个真命题都铺了一条一步到达的道路，整个证明空间的直径几乎变成了 1。但它没有告诉我们为什么，也没有提供可以迁移到下一个问题的结构。

因此，一条真正好的数学捷径通常还应具备几种性质：

• 它不只服务一个题目，而能在不同情境中复用；
• 它压缩的不是表面文字，而是一段反复出现的推理结构；
• 它解释了结论成立的机制，而不是把复杂性藏进不透明的黑箱；
• 它有自然的前提和结论，容易被人或搜索系统识别；
• 它能够引出新的问题、猜想或表示。

Bloom 在讨论 AI 数学成果时提出的定性问题，实际上比“有没有越出凸包”更接近这一标准：方法是否新，能否解决其他问题，是否改变我们对一个领域的理解，还是只对单一目标有效的临时技巧。^[8:2]

一条好定理像交通枢纽，而不是通往一栋房子的私人隧道。

这也体现了人类“提问权”的价值。证明网络能够描述道路怎样连接，却不能单凭结构决定道路应该修向哪里。AI 可以批量生成和检验猜想，但在近乎无穷的真命题中，哪些节点值得连接、哪些方向值得长期投入，仍需要数学审美、问题意识以及来自物理世界的启发。至少在可见的未来，数学家的角色不会只是与机器比较证明速度，也会更多地体现在提出问题、判断价值和设计知识结构上——既是证明者，也是提问者、品鉴者和架构师。

应该怎样评价 AI 的数学贡献

“AI 是否已经发明了人类意义上的新数学技术”仍然是一个开放问题。当前证据并不整齐：有些成果主要来自大规模搜索，有些来自跨领域迁移，有些包含值得进一步抽象的中间结构；新近发布的研究主张还需要时间检验。把所有案例统一称为“突破”，和把所有案例统一称为“拼接”，都过早了。

更合适的评价不应只问：

它有没有离开现有知识的闭包？

还应继续问：

1. 它找到的引理或方法，后来是否被不同问题反复使用？
2. 它是否显著缩短了一批证明，降低了后续搜索的计算与认知成本？
3. 它是否提出了人类原先没有使用的自然定义或表示？
4. 专家读完后，是否获得了新的机制解释，而不只是一份可核验的答案？
5. 去掉这个新结构后，系统的能力是否真的下降？

这些问题同时衡量正确性、证明压缩、复用性、搜索成本和理解深度。它们比单一排行榜更慢，也更难量化，却更接近数学共同体实际评价研究成果的方式。

闭包不是终点，而是底图

“闭包论”确实触及了一个客观事实：当前的 AI 之所以表现出色，很大程度上源于它强大的检索迁移能力和搜索速度，而不是因为它已经掌握了发明全新数学原则的能力。它也警示我们，真正能推动领域发展的普适方法，远比一次性的解题技巧更有价值。

但演绎闭包并不适合作为衡量创新价值的唯一标准。它只能给出终点在逻辑上是否可达，却无法反映道路的长短、桥梁的存在与否，也无法解释为什么某种证明结构能带给研究者深刻的理解。

证明超图提供了一种更符合实际的图景：数学并不是一个不断膨胀的静态命题集合，而是一张持续被重构的网络。新定理在增加节点，新引理在铺设捷径，新定义在重构坐标，新方法在批量生成道路。即使理论上的最大边界未曾改变，有限的主体实际能够触达和使用的数学区域，依然在发生着深刻的扩张。

因此，“某项工作仍在闭包之内”是一个客观的事实陈述，但并不等同于“它没有带来新的数学知识”。

数学的创新，有时是发现一片全新的大陆，但很多时候，只是在关键之处修好了一座桥。当原本遥远的两端因为这座桥而进入日常的研究视野时，我们手中的数学地图，就已经与过去截然不同了。

---

参考文献

---

1. Thomas Hubert et al., “Olympiad-level formal mathematical reasoning with reinforcement learning,” Nature, 2025. https://doi.org/10.1038/s41586-025-09833-y ↩︎

2. Thang Luong and Edward Lockhart, “Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad,” Google DeepMind, 2025-07-21. https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/ ↩︎

3. Uijeong Jang and Ernest K. Ryu, “Point Convergence of Nesterov’s Accelerated Gradient Method: An AI-Assisted Proof,” arXiv:2510.23513, 2025; revised 2026. https://arxiv.org/abs/2510.23513 ↩︎

4. OpenAI, “How GPT-5 helped mathematician Ernest Ryu solve a 40-year-old open problem,” 2025. 该文是对合作过程的机构叙述；数学结论以 Jang 与 Ryu 的论文为准。https://openai.com/index/gpt-5-mathematical-discovery/ ↩︎

5. OpenAI, “A Proof of the Cycle Double Cover Conjecture,” 2026-07. 证明原稿；Sang-il Oum, “A proof of the cycle double cover conjecture by OpenAI: An exposition,” arXiv:2607.16356, 2026. arXiv；Jim Geelen, “OpenAI’s proof of the Cycle Double Cover Theorem,” arXiv:2607.15399, 2026. arXiv ↩︎

6. Kevin Buzzard, “Human mathematicians are being outcounterexampled,” Xena Project, 2026-07-20. 文章；Terence Tao, “A digestion of the Jacobian conjecture counterexample,” 2026-07-21. 文章；Dean Cureton, “Levent Alpöge/Fable 5’s counterexample to the Jacobian conjecture in Lean 4,” 2026. GitHub ↩︎

7. OpenAI, “Ten advances in mathematics and theoretical computer science,” 2026-08-01. 页面同时链接论文稿、推理说明与 Lean 证书。https://openai.com/index/ten-advances-in-mathematics/ ↩︎

8. Thomas Bloom, “Editorial Board Commentary,” FrontierMath: Open Problems, Epoch AI，访问于 2026-08-02。 https://epoch.ai/frontiermath/open-problems/about/mathematician-commentary ↩︎ ↩︎ ↩︎

9. Anson Ho and Tamay Besiroglu, “What is the future of AI in mathematics? Interviews with leading mathematicians,” Epoch AI, 2024-12-04. 受访者包括 Terence Tao、Timothy Gowers、Richard Borcherds 与 Evan Chen。https://epoch.ai/frontiermath/tiers-1-4/expert-perspectives ↩︎

10. Josep Maria Font, Ramon Jansana, and Don Pigozzi, “Algebraic Propositional Logic,” The Stanford Encyclopedia of Philosophy, section 1, “Abstract consequence relations.” https://plato.stanford.edu/entries/logic-algebraic-propositional/ ↩︎

11. William P. Thurston, “On Proof and Progress in Mathematics,” Bulletin of the American Mathematical Society 30 (1994): 161–177. https://arxiv.org/abs/math/9404236 ↩︎

12. Yehuda Rav, “Why Do We Prove Theorems?”, Philosophia Mathematica 7, no. 1 (1999): 5–41. https://doi.org/10.1093/philmat/7.1.5 ↩︎

13. Maissam Barkeshli, Michael R. Douglas, and Michael H. Freedman, “Artificial Intelligence and the Structure of Mathematics,” arXiv:2604.06107, 2026. 其中“通用证明超图”仍是研究纲领式模型，不是已经完成的数学理论。https://arxiv.org/abs/2604.06107 ↩︎

14. George Boolos, “Don’t Eliminate Cut,” Journal of Philosophical Logic 13 (1984): 373–378. https://doi.org/10.1007/BF00247711 ↩︎

15. Stephen A. Cook and Robert A. Reckhow, “The Relative Efficiency of Propositional Proof Systems,” The Journal of Symbolic Logic 44, no. 1 (1979): 36–50. https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/relative-efficiency-of-propositional-proof-systems/218048250981F835B4B2A4080205A0BA ↩︎

16. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson, “Near Optimal Separation of Tree-Like and General Resolution,” Combinatorica 24 (2004): 585–603. https://doi.org/10.1007/s00493-004-0036-5 ↩︎

17. Jean-Yves Girard, “Proof-Nets: The Parallel Syntax for Proof-Theory,” in Logic and Algebra, 1996. https://girard.perso.math.cnrs.fr/Proofnets.pdf ↩︎