Formalizing computability theory via partial recursive functions
我们提出了一个扩展的$\mathtt{mathlib}$图书馆的精益定理证明形式化的基础，可计算性理论。我们使用原始递归函数和部分递归函数作为主要的研究对象，我们使用建设性编码的部分功能，使他们可执行的程序时，有问题的可证明停止。主要定理包括构造一个通用的部分递归函数和证明停机问题的不可判定性。类型类推断提供了一种透明的方式来在需要的地方提供哥德尔编号并封装编码细节。
2019-07-18 cs.LO math.LO
Formalizing Carleson's Theorem in Lean
Princeton University（普林斯顿大学）；University of Bonn（波恩大学）；University of Rennes（雷恩大学）；Utrecht University（乌得勒支大学）；Harmonic（哈莫尼克）；The Hague（海牙）；Eindhoven University of Technology（埃因霍温理工大学）；University of Massachusetts Lowell（马萨诸塞大学洛厄尔分校）；Baruch College（巴鲁克学院）；National University of Singapore（新加坡国立大学）
本文介绍了在 Lean 证明助手中形式化 Carleson 定理的项目，涵盖数学内容、组织、蓝图及设计决策，是公开协作的成果。
2026-09-28 cs.LO math.CA
Formalizing the Ring of Adèles of a Global Field
整体域的阿黛勒环及其单位群，即理想群，是现代数论中的基本对象。我们在Lean 3定理证明器中讨论了它们的定义的形式化。作为一个先决条件，我们形式化adic赋值Dedekind域。给出了一些应用，包括整体类域论的主要定理的陈述和数域的理想类群同构于其理想类群的显式商的证明。
2022-03-06 cs.LO math.NT
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
自从1976年四色定理的证明以来，计算机生成证明在数学和计算机科学中已经成为现实。在过去的十年中，我们已经看到了正式的证明，使用验证证明助手被用来验证这种证明的有效性。在本文中，我们描述了一个形式化的理论的大小最优排序网络。从这个形式化，我们提取一个认证的检查器，成功地验证了计算机生成的最优性证明多达8个输入。该检查器依赖于一个不可信的预言机，以快捷方式搜索超过160万个NP完全子问题的证人。
2015-03-02 cs.LO
Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms
本文扩展了PVS环理论，形式化了Euclidean域的唯一析因性并验证了整数环等结构，同时规范了Euclidean gcd算法并证明其正确性可继承至具体结构。
2024-04-23 cs.LO
Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
Texas Advanced Computing Center, University of Texas at Austin（德克萨斯大学奥斯汀分校高级计算中心）
Sequencelib利用Lean语言形式化OEIS中的序列并证明超过160万条定理，通过转换器和性能优化实现高效计算。
2026-01-16 cs.LO
Formalizing Geometric Algebra in Lean
本文探讨了将几何（或Clifford）代数形式化为Lean 3定理证明器，建立在Lean数学库Mathlib的大量工作基础上。当我们使用Lean源代码来演示我们的许多想法时，我们包含了对Lean语言的简要介绍，针对的是没有Lean或定理证明者经验的读者。我们通过适当的关系将多向量形式化为张量代数的商，从而自动给出了Clifford代数的环结构，进而建立了Clifford代数的泛性质.我们表明，这是完全不同的方法所采取的现有形式化的几何代数在其他定理证明，最值得注意的是，我们的方法不需要选择的基础。我们继续展示如何操作和结构，如对合，versors，和$\mathbb{Z}_2$-分级可以单独使用的通用属性定义，以及如何恢复归纳原则的通用属性适合于证明这些定义的声明。我们概述了形式化wedge产品和$\mathbb{N}$分级所需的步骤，以及mathlib中目前使其具有挑战性的一些差距。
2022-04-19 cs.LO
Formalizing Scarf, Brouwer, and Nash in Lean
Xiamen University Malaysia（厦门大学马来西亚分校）
该研究在Lean 4中形式化了从斯卡夫定理到布劳威尔不动点定理及有限博弈中混合纳什均衡存在性的组合路径，通过特定构造和论证实现，并得出用于探索证明结构理解的BrouwerBench基准。
2026-07-08 cs.GT cs.LO
Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
本文在 Lean 4 中形式化了 Mason-Stothers 定理及其多个推论，包括 Fermat-Cartan 方程不可解性等，并与现有形式化工作对比，成果已集成进 mathlib 库。
2025-09-25 cs.LO math.RA
Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean
该研究在Lean中形式化了任意域上维数至多三的可解李代数的分类定理，涉及底层向量空间计算，并扩展了mathlib的线性代数与李理论库。
2025-05-26 cs.LO math.RA math.RT
Formalizing relations in type theory
类型理论作为数学形式化的框架和提供半自动证明检查和构造的证明助手的基础，在数学基础中起着重要的作用。在类型论中，每个定理的推导都导致了一个形式化的术语来封装整个证明过程。在本文中，我们使用类型理论的一个变体，即具有定义的构造演算，来形式化二元关系的标准理论。这包括关系的基本运算，关系的特殊性质的准则，这些性质在基本运算下的不变性，等价关系，良序，和超穷归纳法。定义和证明作为旗帜式推导。
2021-02-17 cs.LO math.LO
Formalizing Automated Market Makers in the Lean 4 Theorem Prover
本文在 Lean 4 定理证明器中形式化了恒定乘积自动做市商，并提供了套利等关键经济属性的机械化证明，替代了传统的纸笔证明。
2024-02-08 cs.CE cs.GT cs.LO
Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
The University of Utah（犹他大学）
本文用立方阿格达形式化同调类型理论中的实数，避免了经典证明中的可数选择、 Bishop 集合构造的持久书务开销和 Dedekind 切割在预设类型理论中的繁琐层级跟踪。
2026-04-23 cs.LO
Formalizing a Diophantine Representation of the Set of Prime Numbers
DPRM（Davis-Putnam-Robinson-Matiyasevich）定理是Hilbert第10问题负解的主要步骤。近30年来对这个问题的研究已经产生了几个同样令人惊讶的结果。这些包括存在的丢番图方程与减少数量的变量，以及明确建设的多项式，代表特定的集，特别是一套素数。在这项工作中，我们正式这些建设中的Mizar系统。我们专注于素数的集合及其使用10个变量的显式表示。这是目前已知的最小的代表。为此，我们证明了指数函数是丢番图，以及二项式系数和阶乘的相同性质。这种形式化是DPRM定理之后丢番图集形式化方法研究的下一步。
2022-04-26 cs.LO math.NT
Tutte's theorem as an educational formalization project
本文在Lean中形式化了图论中的Tutte定理，并提出了一个教育形式化项目框架，以最少教师输入学习形式化数学，适用于学术和社区环境。
2025-04-25 cs.LO math.CO
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
University of Bath（巴斯大学）
通过形式化验证发现2006年物理论文中存在错误，推翻了其关于双希格斯双态模型势稳定性的核心定理，揭示了形式化方法在物理研究中的重要性。
2026-04-20 cs.LO hep-ph hep-th
From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory
School of Data Science, The Chinese University of Hong Kong, Shenzhen（香港中文大学深圳数据科学学院）；School of Science and Engineering, The Chinese University of Hong Kong, Shenzhen（香港中文大学深圳科学与工程学院）
本文开展Lean形式化工作，对一本14章的概率论教材进行形式化，生成机器可验证配套资料，复用Mathlib结果并引入接口引理，为AI辅助数学构建形式化基础。
2026-07-31 cs.LO
Fully Mechanized Proofs of Dilworths Theorem and Mirskys Theorem
在Coq证明助手中给出了Dilworths定理和Mirskys定理的两个完全机械化的证明。Dilworths定理指出，在任何有限偏序集（偏序集）中，最小链覆盖和最大反链的大小是相同的。Mirskys定理是Dilworths定理的一个对偶。我们用Perles [2]（对Dilworths定理）和Mirsky [5]（对对偶定理）形式化了证明。我们还提出了一个图书馆的定义和事实，可以作为一个框架，形式化其他定理的有限偏序集。
2017-03-17 cs.DM cs.LO
Formalizing the $\infty$-Categorical Yoneda Lemma
本研究借助支持合成∞-范畴理论的新型证明助手Rzk，首次实现∞-范畴理论结论的形式化，核心成果包括范畴论基本定理米田引理的形式化，且框架内构造自动具备自然性或函子性。
2023-12-13 cs.LO math.AT math.CT
Transporting Theorems about Typeability in LF Across Schematically Defined Contexts
针对 LF 规范推理中定理需在不同上下文模式间迁移的问题，本文基于 $\mathcal{L}_{LF}$ 提出可靠的迁移证明规则，并通过类型从属关系定义上下文模式包含，且已集成于 Adelfa。
2025-09-30 cs.LO
Formalizing the Face Lattice of Polyhedra
本文在 Coq 中首次形式化了多面体的面，构建了相关库并设计自动表示机制，证明了面的格性质及 Balinski 定理。
2022-05-17 cs.LO math.CO math.OC
A Formalization of the Generalized Quantum Stein's Lemma in Lean
Perimeter Institute for Theoretical Physics（理论物理珀西默研究所）；Institute for Quantum Computing, University of Waterloo（滑铁卢大学量子计算研究所）；Department of Physics and Astronomy, University of Waterloo（滑铁卢大学物理与天文系）
该工作用 Lean 定理证明器形式化了广义量子斯坦引理的修正证明，修正了原证明中的小瑕疵，并完善了量子资源理论定义，为量子信息形式化提供了稳健基础。
2025-10-09 cs.LO quant-ph
Applied Type System: An Approach to Practical Programming with Theorem-Proving
纯类型系统（PTS）框架提供了一种简单而通用的方法来设计和形式化类型系统。然而，在存在依赖类型的情况下，通常存在某些尖锐的问题，这些问题使得PTS难以直接适应许多常见的现实编程特征，诸如一般递归、递归类型、效果（例如，在本文中，应用类型系统（ATS）被提出作为一个框架，设计和形式化类型系统，以支持实际的编程与高级类型（包括依赖类型）。特别是，它表明，ATS可以很容易地容纳被称为编程与定理证明（PwTP），其中程序和证明构造在一个语法交织的方式，产生一个实用的方法来内在化的约束解决需要在类型检查的范式。ATS的关键显著特征在于静态和动态之间的完全分离，静态是类型的形成和推理，动态是程序的构建和评估。通过这种分离，程序不再可能出现在PTS中允许的类型中。本文不仅包含了ATS的形式化开发，而且还包含了一些取自ats-lang.org的例子，这是一种程序设计语言，其类型系统植根于ATS，以支持采用ATS作为框架来制定用于实际编程的高级类型系统。
2017-03-25 cs.LO cs.PL
Towards the Certification of Complexity Proofs
我们报告我们的形式化的矩阵解释在伊莎贝尔/HOL。矩阵需要证明终止证明，我们希望利用它们的复杂性证明，太。对于后者的目标，只有基本的方法已经被整合，我们讨论了一些即将出现的问题时，形式化更复杂的结果矩阵的解释，这是基于凯莱-汉密尔顿定理或联合谱半径理论。
2012-08-08 cs.LO
Formalization of some central theorems in combinatorics of finite sets
我们提出了充分形式化的证明，从组合学的一些中心定理。这些是Dilworth的分解定理，Mirsky的定理，霍尔的婚姻定理和Erdens-Szekeres定理。Dilworth分解定理是其中的关键结果。它指出，在任何有限偏序集（偏序集）中，最小链覆盖和最大反链的大小是相同的。Mirsky定理是Dilworth分解定理的对偶，Dilworth分解定理指出在任何有限偏序集中，最小反链覆盖和最大链的大小相同。我们利用Dilworth定理证明了Hall婚姻定理和Erdens-Szekeres定理。这些定理所涉及的组合对象是集合和序列。所有的证明都在Coq证明助手中形式化。我们开发了一个图书馆的定义和事实，可以作为一个框架，形式化的其他定理有限偏序集。
2017-03-31 cs.DM cs.LO
Formalizing the Confluence of Orthogonal Rewriting Systems
Universidade de Brasília（巴西利亚大学）
可确定性是一种编程原则，它以语法的方式保证功能规范的确定性。基本上，正交性一方面避免了非确定性的固有模糊性，禁止存在指定相同函数的不同规则并且可以同时应用（非模糊性），另一方面，它消除了在这些规则的左侧出现变量重复的可能性（左线性）。在术语重写系统（TRS）理论中，确定性被众所周知的汇合性质所捕获，该性质基本上表明，无论何时从一个术语进行不同的计算或简化都是可能的，计算出的答案应该一致。虽然证明在技术上是详尽的，但汇流是众所周知的正交性的结果。因此，正交性是递归函数的规范所固有的一个重要的数学学科，它自然地应用于函数式编程和规范。从形式化的理论TRS的证明助手PVS，这项工作描述了如何融合的正交TRS已正式化，公理化的基础上的属性的规则，位置和替代参与并行步骤的减少，在这个证明助手。证明了一些类似的，但限制性的性质，如非二义性和（左和右）线性TRS的合流的性质已经完全形式化。
2013-03-29 cs.AI cs.LO cs.PL
A proof complexity conjecture and the Incompleteness theorem
Charles University（查理大学）
该研究通过定义p-时间函数g_T，证明了任何能形式化一阶逻辑语法的理论必不完整，并探讨了命题证明系统、NP集与证明复杂性生成器之间的关系。
2023-09-15 cs.LO math.LO
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r)
University of British Columbia（不列颠哥伦比亚大学）
我们提出了一个机械证明的Cauchy-Schwarz不等式在ACL 2（r）和形式化的必要的数学进行这样的证明。这包括将$\mathbb{R}^n$形式化为内积空间。我们还提供了一个应用Cauchy-Schwarz的形式化$\mathbb R^n$作为一个度量空间，并表现出连续性的一些简单的功能$\mathbb R^n\to\mathbb R$。柯西-施瓦茨不等式将向量的大小与其与另一个向量的投影（或内积）联系起来：\[|\langle u,v\rangle| \leq \|u\| \|v\|\]等式当且仅当向量线性相关。它经常用于数学的许多分支，包括线性代数，实分析，泛函分析，概率等，事实上，不等式被认为是“一百个最伟大的定理”之一，并被列入“形式化100个定理”项目。据我们所知，我们的形式化是第一个使用ACL 2（r）或任何其他一阶定理证明器的证明。
2018-10-10 cs.AI cs.LO
A Machine-checked proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory
Agda Universal Algebra Library（agda-algebras）是我们开发的类型和程序（定理和证明）库，用于使用Agda程序设计语言和证明助手在依赖类型论中形式化通用代数的基础。在本文中，我们借鉴和解释许多组件的agda代数库，我们提取到一个单一的Agda模块，以提出一个自包含的形式和建设性的证明Birkhoff的HSP定理在马丁-洛夫依赖类型论。在我们的演讲过程中，我们强调了一些更具挑战性的方面，形式化的基本定义和定理的通用代数类型论。尽管如此，我们希望这篇论文和agda代数库可以作为进一步的证据来支持这样一个主张，即依赖类型论和Agda语言，尽管它们对用户提出了技术要求，但对于那些拥有足够耐心和决心用证明助手正式验证其结果的工作数学家（比如我们自己）来说，是可以访问的。事实上，agda-algebras库现在包括了大量的定义、定理和泛代数的证明，说明了归纳和依赖类型在表示和推理一般代数和关系结构方面的表达能力。
2021-11-30 cs.LO math.LO
A Coq Formalization of Lebesgue Integration of Nonnegative Functions
积分和微分一样，是一种基本的微积分工具，广泛应用于许多科学领域。在正式的证明助手中形式化积分的数学概念和相关结果有助于直接或间接地对涉及使用积分的数值程序的正确性提供最高的置信度。由于它能够将黎曼积分扩展到广泛的一类不规则函数，以及定义在比实数线更一般的空间上的函数，勒贝格积分非常适合用于数学领域，如概率论，数值数学和实分析。本文给出了$σ$ -代数、测度、单函数和非负可测函数的积分的Coq形式化，以及Beppo Levi（单调收敛）定理和Fatou引理的完整形式证明.超过一个普通的形式化的已知文献，我们提出了几个设计选择，以平衡数学可读性和可用性之间的和谐Coq定理。这些结果是走向$L^p$ ~空间如Banach空间形式化的第一个里程碑。
2021-12-09 cs.LO math.FA
Elements of Differential Geometry in Lean: A Report for Mathematicians
我们报告我们的经验形式化微分几何与mathlib，精益数学库。我们的叙述是面向几何学家的，他们没有类型论的知识，但渴望了解更多关于数学的形式化，也许好奇到在未来给Lean一个尝试。为了达到这个效果，我们强调可能令人惊讶的形式化和它的笔和纸的对等物之间的差异所产生的精益的平等待遇。我们的三个案例研究是李群，向量丛和李群的李代数。
2021-08-01 cs.LO math.DG
(Seemingly) Impossible Theorems in Constructive Mathematics
我们证明了一些建设性的结果，在第一次，甚至可能在第二次看起来是不可能的。
2019-04-12 cs.LO math.LO
