形式化证明冷思考：数学证明中的对应问题
从数理哲学角度，探讨数学证明的对应性问题。形式化证明一方面可以作为判定结论真伪的凭证，另一方面，研究者也希望读懂证明的每一处逻辑细节。人工推导的非形式化证明与机器形式化证明之间，如何建立清晰的对应关联，是亟待解决的问题。
西蒙・德迪奥（Simon DeDeo）
伊蒙・杜德（Eamon Duede）
作者：西蒙・德迪奥（Simon DeDeo，卡内基梅隆大学、圣塔菲研究所）
伊蒙・杜德（Eamon Duede，普渡大学、美国阿贡国家实验室）2026-3-18
译者：zzllrr小乐（数学科普公众号）2026-5-26
摘要
人们常说，数学证明通过指明存在与之对应的形式化推导来为其结论提供辩护。我们认为，这一广为流传的观点依赖于一个未经充分考察的对应概念，即一个特定推导 “对应” 于一个特定证明究竟意味着什么。仅仅存在形式化是不够的，对所需对应的实质性说明可分解为两个标准 —— 对原定理的恰当表征，以及对原证明步骤的追踪。对我们当前实际存在的形式化系统的考察表明，我们确立这些标准的方式具有准经验性，这也为数学自身的未来发展提出了新的要求。
预备知识
一般而言，认为数学证明具有认知价值的观点是没有争议的。然而，一旦人们试图阐明这种价值的内涵，以及证明如何确保这种价值，争议便随之产生。毕竟，证明显然有诸多作用：传递数学思想、传达理解、统一或拓展此前相互独立的知识体系。同时，证明也被认为具有独特的辩护作用。在这种作用下，证明理应确立数学断言的正确性，从而保证数学实践所特有的高度共识。令人困惑的哲学问题在于，顶级期刊与教科书中的数学证明尽管是非形式化的、不完整的、充斥着隐含假设、逻辑跳跃、对背景理解的依赖，且时常夹杂局部错误，却依然能稳定地发挥这一作用。这类对象何以能以数学知识所具备的可靠性与演绎安全性为数学断言提供辩护，远非显而易见。
主流观点将非形式化数学证明的辩护效力最终归结为存在对应的形式化推导。根据这一所谓的 “标准观点”，一个非形式化证明是正确的，当且仅当它表明能够在合适的形式化证明系统中生成一个完全显式的证明 [Azz04, Avi19, Ham22, ML86]。标准观点有多种表述形式，但它们的共同立场是：一个真正的证明在其非形式化呈现之下，存在或应当存在一条 “从显式公理集出发的无间断逻辑推理链”[Hal12, 第 x 页]。标准观点的反对者通常否认非形式化证明的正确性可仅仅基于底层推导的存在，转而强调证明中不可还原的语义、方法论与实践相关特征，这些特征无法被对应的无间断形式化推理链所捕捉 [Rav99, Tan15]。
然而，标准观点的支持者与批评者都默认一个前提：对任意给定证明，谈论一个与非形式化证明对应的形式化证明是有意义的。基于这一共同前提，争论的焦点转向了对应的形式化推导是否、在何种程度上、以及如何为辩护的认知价值做出贡献。
本文主张，对应这一前提本身不能被视为理所当然。对于当代基于库的形式化项目而言，这一问题不仅具有理论意义：问题不在于一个可被非形式化表达的定理是否存在形式化证明，而在于这样的证明对应于某个人类特定的证明思路究竟意味着什么。也就是说，成功得到一个不仅对应于某定理的证明，更对应于该定理某一特定证明的形式化证明，本身就是一项认知成就，而当代形式化生态系统可能会系统性地阻碍这一成就的实现。
本文分为五个部分。第一部分简要梳理并定位标准观点及其批评者，强调二者均默认非形式化与形式化证明之间对应关系的可理解性。我们区分 “弱” 与 “强” 两种对应概念，并论证强对应在现有文献中的优先地位。第二部分展开强对应概念：要实现所需的对应，形式化证明必须同时满足两点，一是恰当地表征相关断言，二是追踪这些断言的非形式化证明步骤。这两项任务均具挑战性，我们将讨论现有形式化项目如何尽可能将对应的负担转移到表征层面，以及这样做的合理性。第三部分说明，继承而来的基础设施与固化的依赖结构会进一步动摇传统的对应图景，因为它们允许混合不同建模传统片段的形式化正确证明存在。我们认为这会导致更深层的不对称性：人类证明在语义上先于形式化推导，而在大型库中构建的形式化推导很可能脱离其本应表达的证明思路与解释结构。
基于此，第四部分从正面提出确立对应的三种路径：因果路径、解释路径与结构路径。这使得形式化实践与其他人类证明处于更平等的地位，它系统性地约束证明空间，依据数学共同体共享的背景模型，筛选出可理解、具解释力且可复用的定义与推导路径。这些约束部分源于数学家的犯错经验与对话交流，其形成既受制于证明空间的底层结构，也回应着参与者的认知局限与历史背景。我们简要援引形式化领域近期的一场争议，说明实践者如何应对对应问题及其原因。第五部分为结论。
1 对应
顶级数学期刊与教科书中的证明是自然语言与数学符号的结合体，基于共识构建，且出于必要性将诸多推理步骤隐含处理。遵循文献惯例，我们将这类证明称为非形式化证明。与之相对，形式化证明是在固定证明系统中完成的推导，其中从公理到结论的每一个演绎依赖都被精确化，且原则上可被机械检验。非形式化与形式化证明的目标都是确立数学定理，这意味着至少在原则上，一个给定结论可以同时拥有非形式化与形式化证明。此外，数学界的主流观念认为，若一个非形式化证明真正正确，则该定理必然存在对应的形式化推导。这一观念可见于中叶结构主义传统，如麦克莱恩（Mac Lane）与布尔巴基（Bourbaki）[Lan35, Bou70]，且很可能延续自更早的弗雷格（Frege）[F⁺79] 的逻辑主义与希尔伯特（Hilbert）[HA38] 的形式主义纲领。
标准观点并非单一论题，而是一组以形式化推导为认知价值辩护基础与目标的观点。至少在本文表述中，它存在模糊性，因为非形式化与形式化证明的关系可被解读为两种方式。第一种解读是：若定理 θ 的非形式化证明 π 是真正的证明（而非看似证明实则不然的论证 [DT21]），则存在 θ 的形式化推导 δ，这称为弱解读。第二种解读是：若定理 θ 的非形式化证明 π 是真正的证明，则存在 θ 的、与 π 对应的形式化推导 δ，这称为强解读。弱解读下，θ 的任意形式化推导均可；强解读下，对应要求推导 δ 与 π 所表达的证明思路之间具有特定的结构、因果或解释关系。
标准观点的支持者并不总是明确区分这两种解读，文献也因此在二者间摇摆，掩盖了真正的核心问题 ¹。显然，若非形式化证明正确，则 θ 必然存在某个形式化推导，这等价于说若 θ 为真且可证，则 θ 可在与非形式化系统能力相当的合适形式化系统中推导。弱解读虽显而易见，却无法说明作为 θ 某一特定证明的 π 的正确性具有何种独特认知作用。同一底层推导 δ 同样可以支撑 θ 的其他任意非形式化证明 π'，无论其策略、概念工具或解释目标有何不同。换言之，弱解读似乎只验证定理而非证明本身，但学界通常关注的是特定证明的正确性，而非特定定理的真或可证性 [Gow23]。
¹ 例如，阿维加德（Avigad）指出 “投入足够工作量，非形式化证明可转化为形式化推导”[Avi21]，麦克莱恩（Mac Lane）则认为足够详细的非形式化证明（他称之为概要）应 “使该概要翻译为形式化证明成为可能”[ML86]，二者的表述显然都强于仅要求形式化推导存在。
为说明这一点，假设存在同一定理 θ 的两个非形式化证明 π₁与 π₂。π₁的思路与策略依赖单一数学领域内复杂繁琐的操作，π₂的思路与策略则巧妙融合多个看似无关领域的思想。数学家确信 π₁是真正的证明，却因 π₂的优雅与统一性对其更为关注，希望验证 π₂是否为真正的证明，于是将其形式化为 δ。弱解读下，形式化 δ 仅确认 θ 可推导，而这一点数学家早已从 π₁的存在中得知。π₂的独特策略是否有效、其优雅融合是否构成真正证明，完全未被评估。
由此可见，要说明特定证明作为证明的认知价值，标准观点需要强解读，进而需要阐明非形式化证明 π 与形式化证明 δ 之间需存在何种对应关系，使得 δ 的形式结构匹配 π 的推理组织。这种对应还需能区分同一定理的不同证明 π' 乃至错误证明 π*。哲学任务从证明推导存在转向解释推导对应于特定证明思路的含义。
2 对应问题的两个方面
多数哲学文献将对应概念视为未加分析的初始概念，认为其足够清晰，可直接援引而无需细致考察。即便标准观点的重要批评者也未质疑对应的可理解性。例如，拉夫（Rav）对标准观点的有力批判，旨在否定数学证明 π 的认知价值可被其对应的形式化推导 δ 穷尽 [Rav99]。哈马米（Hamami）对标准观点的严谨重构 [Ham22] 也未分析为何形式化推导是某一特定证明的推导，而非仅某一特定定理的推导。换言之，争论的共同框架是：对应的充分性或范围可被争议，但其可理解性被默认。
强对应立场的直觉是：对任意特定非形式化证明 π，仅存在形式化证明 δ 不足以让我们认定 π 是成功的。我们需要确信 δ 最终确立的命题恰当地表征了 π 开头的命题，也需要看到 δ 的特征如何追踪 π 的推理。非形式化与形式化证明都以逐步展开的方式呈现推理，δ 追踪 π 意味着存在从 π 中每一步到 δ 中某一步或若干步骤的恰当映射，该映射保留非形式化论证的依赖结构，即便形式化证明可能重排或分解单个步骤。因此，对应概念是追踪条件与表征条件的共同满足。
对应：形式化证明 δ 对应于非形式化证明 π，当且仅当 δ 成功追踪 π 所论证的推理序列，且恰当地表征 π 所表达的定理 θ。
就追踪而言，关键并非逐行模仿，而是保留足够的推理结构，使 π 与 δ 可被识别为实现同一证明思路与策略。就表征恰当性而言，关键并非 δ 是 π 中定理陈述的语法转述，而是用于建模 π 所涉数学内容的形式化对象、谓词与依赖关系的恰当性。
对应问题的两个方面已存在数十年。早期形式化项目如布尔巴基学派由领域核心数学家开展，他们几乎默认参与者对当时非形式化数学有恰当表征，能以一致视角审视形式化工作，并验证并行证明的步骤得到恰当追踪。非形式化证明在形式化过程中可能被展开，例如需额外说明如何将函数编码为集合，但如果形式化出现明显偏离，则意味着非形式化证明需要修改或重写。
形式化证明的新型计算工具让这些未被明说的表征与追踪需求受到广泛关注。如今，Lean、Rocq、Isabelle/HOL 等形式化语言被大量社群与顶尖数学家使用，已完成多项重要数学成果的形式化 ²。
² 例如，参见由约翰・科梅林（Johan Commelin）主导的液态张量实验 [CTB⁺22, Har21]，该实验形式化了菲尔兹奖得主彼得・舒尔茨（Peter Scholze）在解析几何中提出的高难度 “挑战” 定理。
为结合近期进展理解对应问题的两个方面，我们从一个简单例子入手。考虑欧几里得素数定理的如下 “证明”：
定理：不存在最大的素数。
证明 *：假设存在最大素数 N，构造数 M 为 1 到 N 所有整数的乘积加 1。M 不能被小于等于 N 的任意整数整除，因此 M 是素数。M 大于 N，矛盾。□
首先考察追踪条件面临的挑战。当前主流形式化语言均能陈述并证明欧几里得素数定理，但例如 Lean 中该定理的正确形式化证明存在，无法说明证明这一非形式化证明的情况。原因在于证明的第四句话存在错误：M 不能被小于等于 N 的任意整数整除，不代表 M 是素数；正确证明利用 M 证明存在素数 p，p 不必等于 M。因此，形式化证明（假设系统可靠）不会追踪第四句的非形式化错误，形式化语言中也不会出现断言 M 恒为素数的内容。
即便非形式化证明正确，追踪问题依然存在。任意定理都有无穷多种形式化证明，并非所有都追踪同一非形式化证明。例如欧拉对该定理的证明利用调和级数∑ᵢ₌₁^∞1/n 发散的事实，人类可借助现有形式化技术找到与欧几里得证明完全不同的形式化证明。还有一些形式化证明表面上没有直观可读的非形式化对应。AlphaProof 在欧几里得简单例子上的演示生成了有效的 Lean 代码，即有效证明 ³，但其表面上并未清晰追踪人类的推理步骤。
³ 我们默认 Lean 内核的有效性与 mathlib 的可靠性，尽管这一问题广受关注 [Mac04]。
表征恰当性方面同样存在问题。定理中的自然语言语句 “不存在最大的素数” 必须被形式化，但我们没有明确标准判断该语句与形式化重述之间对应的恰当性。事实上，在现有形式化生态系统中，当输入 “∀n,∃p,(素数 p)∧(p>n)” 时，符号与谓词是否真的表示 “对所有”“存在”“是素数”“大于” 并不总是明确。
这类怀疑并非哲学家的空想。早期在 Isabelle 中形式化二次互反律的尝试成功追踪了非形式化证明，却因表征不当失败：素数的定义导致不存在素数，证明等价于空集上一切命题为真 [Avi19]。这一挑战至今存在，正如约翰・科梅林（Johan Commelin）所说的 “这不是一支烟斗”（参见 [DeD24]）。学界普遍认为，解决方案具有准经验性，需类似软件工程单元测试的方式，用多种测试用例对定义进行 “压力测试”[GM16]。正如球体填充问题形式化项目负责人之一所言 [BHL⁺26]：
“对定义进行压力测试当然并非万无一失，有时只有尝试极其怪异或深刻的内容才能发现问题。但只要谨慎设计与巧妙测试相结合，我们通常能发现错误。”[Har26]
支持对应的证据会累积至认知收益递减的程度，而非以演绎确定性确立。强标准观点承诺为非形式化证明 π 的演绎确定性提供依据，但我们只能归纳地判断其对 θ 的辩护是否成立。
实践中，现有形式化项目通过两步克服对应问题⁴，这一划分在主导当代形式化的类型论语言中自然成立。
⁴我们并非断言这是社群成员公认的工作议程。
以 Lean 中欧几里得定理证明的片段为例：
theorem primes_unbounded (n : Nat) : ∃p, Prime p ∧ p≥n := by let m := Nat.factorial n + 1 have h2 : 2≤m := by have : 1≤Nat.factorial n := Nat.succ_le_of_lt (Nat.factorial_pos n) …
第一行包含类型签名：非形式化地说，primes_unbounded 被定义为一个函数，接受自然数 n，返回一个证明（类型为 “∃p, 素数 p∧p≥n”，该类型属于命题类型），证明存在大于等于 n 的素数 p。表征恰当性通过检查类型签名确立，只要信任类型系统，签名通常易于用自然语言表达，可被视为 “意图声明”：证明结束时，系统自身会验证已构造并返回承诺类型的项。
by 之后的剩余行构成实际构造签名承诺内容的计算结构。理想情况下，追踪恰当性通过检查 by 后的内容是否匹配自身推理来确立。但实践中，定理复杂度提升后这一过程变得困难。Lean 与多数类型论语言一样高度依赖 “策略”：通用工具会分析调用前的内容，在受限空间内搜索以推进证明至下一阶段。这些策略展开的输出可被查看，但通常难以理解，使用者转而观察策略如何使证明向目标状态推进。规范的 Lean 风格建议使用完成目标所需的最弱策略，但这只是风格选择，系统并不禁止使用过强的策略，以人类难以理解的方式完成所需步骤。
追踪相较于表征的相对不透明性，对人类形式化工作产生实际影响。例如多项式弗莱曼–鲁扎猜想（PFR）的非形式化证明 [GGMT25] 约 13000 词，包含 17 个标注为定理、推论、引理或命题的陈述；对应的 Lean 形式化 [tea26] 则至少有 910 个声明，即关联类型签名与定理、引理或其他定义的代码片段。即便放宽非形式化证明中声明的标准，纳入 67 个带编号公式与约 15 至 20 个文字定义，形式化证明的声明数量仍至少多出十倍。
两种模式的巨大差距显而易见。现有形式化项目的意图声明远多于非形式化对应项，这意味着对应问题可更多依赖表征恰当性判断。这一状况较为有利：当前类型论语言的特性使得表征恰当性通常比追踪更易判断，且通过以可读形式暴露大量中间断言，对应关系更易评估。
这一高比例并非 PFR 独有。对玛丽娜・维亚佐夫斯卡（Maryna Viazovska）8 维球体填充问题解答 [Via17] 的形式化 [BHL⁺26] 对比显示，非形式化证明包含 12 个定理与命题、65 个带编号公式和约 20 个文字定义，而人类撰写的形式化尝试中约有 1362 个声明，该工作于2026年2月下旬由 Math, Inc. 的人工智能工具意外完成。详情参阅：
AI与人类协作在数学领域迎来里程碑时刻 ——21世纪菲尔兹奖获奖证明首次完成形式化验证——IEEE Spectrum
2026.5数学未来研讨会系列——球体堆积问题的形式化by 玛丽娜·维亚佐夫斯卡（Maryna Viazovska，2022年菲尔兹奖得主）——斯坦福FMS
完全展开的形式化证明不一定标注甚至保留这些边界。例如编译为最终形式后，结果是一个大型有向图，可能包含数十万个节点 [VD22]。因此，形式化语言的使用难度意味着人类开展形式化工作时，必须依据追踪原始论证的蓝图进行。
这一约束对确立标准观点所需认知效力的对应关系有积极作用。尽管如此，这些对应关系仍依赖证据收集。形式化推导是否对应于特定非形式化证明，最终是一个经验问题，而标准观点预设了这一问题的答案，却未自身提供。
3 库、锁定效应与共享模型
我们已经看到，标准观点需要强对应概念，而这一概念又要求形式化证明恰当地表征并追踪其非形式化对应项。此外，对任意真正的非形式化证明 π，确立其与形式化证明 δ 的对应关系部分是一项经验成就。标准观点承诺的对 π 的演绎确证，因此成为归纳偶然事件，而形式化工作者拥有实现这一确证的有效方法。
然而，即便形式化工作者操作无误，其所处的形式化基础设施也会扭曲对应关系：它向作者强加的证明结构选择源于库的历史，而非 π 底层证明思路的特征。典型的非形式化证明从远离公理的演绎起点开始，预设大量既有结果作为后续工作的接口。因此，数学在社会与历史偶然中的发展，构成了当下的生态系统，并随新证明的出现持续演化。
实践中，数学家将非形式化证明 π 形式化时，不仅身处 π 诞生的知识生态系统（π 在其中可被理解与拓展），同时也处于 δ 所属的独立生态系统，该系统由自身不断演化的历史与社会偶然因素塑造。
与非形式化数学类似，形式化数学证明必然依赖大量已形式化的既有结果。历史约束的影响更为显著，因为形式化证明必须覆盖从公理到目标定理的每一步推理：例如在 Lean 中，δ 必须在库中所有既有结果的环境下通过编译，即 mathlib4 生态系统。
证明与声明由致力于特定生态系统的社群成员添加至这些库中。与 π 的生态系统因非形式化特性而在约定上多元包容不同，δ 的形式化库是刚性的依赖结构，每个定义必须与其他所有内容精确兼容。
证明强结论所需的基础设施，是社群开展特定形式化项目的副产品。部分项目源于个人偏好与即兴选择，但多数是面向其他数学家、资助机构或希望将技术商业化的企业，展示形式化价值的高规格工作，例如液态张量实验。无论动机如何，早期形式化工作会逐渐固化，修改成本高昂 [Wim07]。这种路径依赖已在形式化证明中显现，其依赖结构与 Linux 内核等大型软件项目相似 [VD22]。
随着依赖图围绕早期选择不断扩张，后续形式化工作必然继承这些选择，无论它们是否很好地表征当前被形式化证明的底层思路。结果是，依据非形式化证明 π 工作的数学家可能被迫使用与 π 概念工具不匹配的库定义，即便这些定义能成功得到 θ，最终的形式化推导 δ 对 π 的追踪也可能很弱甚至不存在。对应关系被混合，π-δ 关系由库的约定与约束中介并改变 —— 这些选择是形式化工作者继承而非自主做出的。数学始终具有历史性与路径依赖，新的变化是它遭遇了全新、独立且可能更难演化的传统。
4 确立对应的路径
对应关系如何确立？我们认为，将非形式化证明形式化的数学家在实践中至少可通过三种独立方式验证表征与追踪的恰当性。遵循温萨特（Wimsatt）[Wim07] 的观点，我们认为这些方式的独立性具有认知意义：各自易受不同失效来源影响的方式若能达成一致，将提供单一方式无法实现的鲁棒性。
第一种是结构路径：数学家可验证 π-δ 对共享相关结构。第二种是因果路径：数学家可验证从非形式化证明到形式化对应项的因果链路。第三种是解释路径：数学家可验证非形式化解释形式化证明为何能通过类型检查，或形式化证明解释非形式化证明为何成立。
原则上，结构对应通过检查 δ 中的对象与推理步骤是否镜像 π 中的内容确立。在上述简单的 primes_unbounded 例子中，可注意到非形式化中考虑 m=n!+1 与形式化开头定义 m 为 Nat.factorial n+1 的对应关系，并额外对 Nat.factorial 与 + 进行压力测试，确保这些符号按预期工作。如前所述，随着待验证新数学与库最初设计所针对的数学之间差距扩大，结构路径的难度会显著增加。若要确立对应，必须借助结构对比之外的资源。
将形式化视为翻译时，因果路径变得相关。在这一路径下，人们能看到 π 中的某一步如何引导自己在 δ 中编写特定步骤，而非其他同样有效的步骤，如同 “跟随” 论证。因果关系不必保留结构。若 π 基于集合论或经典逻辑撰写，而 δ 使用类型论与构造性逻辑，数学家翻译过程中的部分步骤可能仅具有微弱的结构关联。至少在当前阶段，因果关系中哪些方面至关重要尚不明确，尤其是在人工智能工具参与的情况下。因果路径提供来源信息，区分依据该特定证明生成的推导与恰好证明同一定理的推导。
最后，解释关系不仅是开展形式化工作的初衷 [Avi24]，还具有特殊效力：例如 δ 与 π 足够接近，能清晰填补空隙；或反过来，π 帮助理解 δ 中特别晦涩的部分。若形式化深化了对原始非形式化证明的理解，例如揭示底层论证中未被注意的方面，我们便有理由更确信表征与追踪均已实现。这与 “输入垃圾，输出垃圾” 的俗语相反：当形式化为原始非形式化证明带来意外的认知收益时，便暗示表征与追踪均取得成功。
因果与解释路径均体现在阿维加德（Avigad）对 Math, Inc. 人工智能自动完成球体填充证明争议的回应中。
“形式化本身几乎没有价值，因为维亚佐夫斯卡（Viazovska）结果的正确性从未受到质疑。参与者投身该项目，是为了重新审视这些结果、深化理解，并构建支持未来工作的库与基础设施。”[Avi26, 第 3 页]
换言之，有价值的形式化必须参与因果过程，即通过新的人类解释者重新审视维亚佐夫斯卡（Viazovska）的结果，并有望服务于提升数学理解的认知目标 [Thu06]。
5 结论
本文主张，标准观点承诺解释非形式化数学成就的演绎确定性，这一承诺被无限期推迟。其演绎表象之下是更为丰富的对应概念，这一概念通过多种可废止路径的收敛，为有限理性的人类所把握。遵循温萨特（Wimsatt）的观点，形式化推动数学进步的原因，正是这些路径可独立失效。形式化并非连接非形式化证明与形式化确定性的演绎桥梁，而是由多条独立证据路径支撑的、可废止的经验性对应成就。
人工智能驱动数学的快速发展，使这些问题比以往任何时候都更为紧迫 [DD24]。一旦因果来源与解释透明性被削弱，支撑强对应主张所需的收敛性也会随之减弱。
致谢
作者感谢杰里米・阿维加德（Jeremy Avigad）、戴维・巴拉克（David Barack）、丹尼尔・C・弗里德曼（Daniel C. Friedman）、西达尔塔・哈里哈兰（Sidharth Hariharan）与蔡斯・诺曼（Chase Norman）对本文初稿的有益反馈。本工作由约翰・坦普尔顿基金会资助西蒙・德迪奥（Simon DeDeo）的项目 “解释普遍真理”（编号 63750），以及阿尔弗雷德・P・斯隆基金会资助伊蒙・杜德（Eamon Duede）的项目 “人工智能与不断演化的学科探究规范”（编号 G-2025-79234）支持。
原文参考资料
[AVI19]J. Avigad (2019)Automated reasoning for the working mathematician.Frontiers of Combining Systems (FroCoS), London.Cited by: §2, Preliminaries.
[AVI21]J. Avigad (2021)Reliability of mathematical inference.Synthese 198 (8), pp. 7377–7399.Cited by: footnote 1.
[AVI24]J. Avigad (2024)Mathematics and the formal turn.Bulletin of the American Mathematical Society 61 (2), pp. 225–240.Cited by: §4.
[AVI26]J. Avigad (2026)Mathematicians in the age of AI.arXiv (2603.03684).Note: https://arxiv.org/abs/2603.03684Cited by: §4.
[AZZ04]J. Azzouni (2004)The derivation-indicator view of mathematical practice.Philosophia Mathematica 12 (2), pp. 81–106.Cited by: Preliminaries.
[BHL+26]C. Birkbeck, S. Hariharan, S. Lee, G. Ma, B. Mehta, and M. Viazovska (2026)Formalising Sphere Packing in Lean.Note: https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/Accessed: 2026-02-16Cited by: §2, §2.
[BOU70]N. Bourbaki (1970)Théorie des ensembles.Vol. 1363, Hermann Paris.Cited by: §1.
[CTB+22]J. Commelin, A. Topaz, R. Barton, A. J. Best, R. Brasca, K. Buzzard, Y. Dillies, F. van Doorn, F. Glöckle, M. Himmel, H. Macbeth, P. Massot, B. Mehta, S. Morrison, F. A. E. Nuccio, J. Riou, D. Testa, and A. Yang (2022)Liquid Tensor Experiment.Note: https://github.com/leanprover-community/lean-liquidAccessed: 2026-02-16Cited by: footnote 2.
[DE 21]S. De Toffoli (2021)Groundwork for a fallibilist account of mathematics.The Philosophical Quarterly 71 (4), pp. pqaa076.Cited by: §1.
[DED24]S. DeDeo (2024)AlephZero and mathematical experience.Bulletin of the American Mathematical Society 61 (3), pp. 375–386.Cited by: §2.
[DD24]E. Duede and K. Davey (2024)Apriori knowledge in an era of computational opacity: the role of AI in mathematical discovery.Philosophy of Science, pp. 1–11.Cited by: §5.
[Fo79]G. Frege et al. (1879)Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought.From Frege to Gödel: A source book in mathematical logic 1931, pp. 1–82.Cited by: §1.
[GM16]V. Garousi and M. V. Mäntylä (2016)A systematic literature review of literature reviews in software testing.Information and Software Technology 80, pp. 195–216.Cited by: §2.
[GOW23]T. Gowers (2023)What makes mathematicians believe unproved mathematical statements.Annals of Mathematics and Philosophy 1 (1), pp. 57–110.Cited by: §1.
[GGM+25]W. T. Gowers, B. Green, F. Manners, and T. Tao (2025)On a conjecture of Marton.Annals of Mathematics 201 (2), pp. 515–549.Cited by: §2.
[HAL12]T. C. Hales (2012)Dense sphere packings: a blueprint for formal proofs.Vol. 400, Cambridge University Press.Cited by: Preliminaries.
[HAM22]Y. Hamami (2022)Mathematical rigor and proof.The Review of Symbolic Logic 15 (2), pp. 409–449.Cited by: §2, Preliminaries.
[HAR26]S. Hariharan (2026)Personal communication by e-mail.Note: Received: 2026-02-17Cited by: §2.
[HAR21]K. Hartnett (2021)Proof assistant makes jump to big-league math.Quanta Magazine 28.Cited by: footnote 2.
[HA38]D. Hilbert and W. Ackermann (1938)Grundzüge der theoretischen logik.Cited by: §1.
[HMS+25]T. Hubert, R. Mehta, L. Sartran, M. Z. Horváth, G. Žužić, E. Wieser, A. Huang, J. Schrittwieser, Y. Schroecker, H. Masoom, et al. (2025)Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, pp. 1–3.Cited by: §2.
[LAN35]S. M. Lane (1935)A logical analysis of mathematical structure.The Monist 45 (1), pp. 118–130.Cited by: §1.
[MAC86]S. Mac Lane (1986)Functions, transformations, and groups.In Mathematics Form and Function,pp. 123–149.Cited by: Preliminaries, footnote 1.
[MAC04]D. MacKenzie (2004)Mechanizing proof: computing, risk, and trust.MIT Press.Cited by: footnote 3.
[RAV99]Y. Rav (1999)Why do we prove theorems?.Philosophia mathematica 7 (1), pp. 5–41.Cited by: §2, Preliminaries.
[TAN15]F. Tanswell (2015)A problem with the dependence of informal proofs on formal proofs.Philosophia Mathematica 23 (3), pp. 295–310.Cited by: Preliminaries.
[TEO26]teorth et al. (2026)Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results).Note: https://github.com/teorth/pfr/tree/master/PFRAccessed: 2026-02-16Cited by: §2.
[THU06]W. P. Thurston (2006)On proof and progress in mathematics.In 18 Unconventional essays on the nature of mathematics,pp. 37–55.Cited by: §4.
[VIA17]M. S. Viazovska (2017)The sphere packing problem in dimension 8.Annals of mathematics, pp. 991–1015.Cited by: §2.
[VD22]S. Viteri and S. DeDeo (2022)Epistemic phase transitions in mathematical proofs.Cognition 225, pp. 105120.Cited by: §2, §3.
[WIM07]W. C. Wimsatt (2007)Re-engineering philosophy for limited beings: piecewise approximations to reality.Harvard University Press.Cited by: §3, §4.
参考资料