A formalization of the Gelfond-Schneider theorem
Institute for Computing and Information Sciences, Radboud University（拉德堡德大学计算与信息科学研究所）
本文用Lean 4证明助手形式化了希尔伯特第七问题及其解格尔丰德-施内尔定理，证明了代数数的幂次为超越数。
2026-03-25 cs.LO
Formalization of the Axiom of Choice and its Equivalent Theorems
本文描述了Morse-Kelley集合论中选择公理的形式化及其几个著名的等价定理。这些定理包括Tukey引理、Hausdorff极大值原理、极大值原理、Zermelo公设、Zorn引理和良序定理。我们依次用选择公理证明上述定理，最后用Zermelo公设和良序定理证明选择公理，从而完成了它们之间等价性的循环证明。使用Coq证明助手对证明进行了形式化的检查，其中Morse-Kelley集理论被形式化。整个形式证明过程表明，基于Coq的数学定理机器证明具有高度的可靠性和严密性。本文的形式化工作对于大多数应用，特别是在集合论、拓扑学和代数学中的应用是足够的。
2019-06-10 cs.FL cs.LO
Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
Freie Universität Berlin（柏林自由大学）；Vienna University of Technology（维也纳技术大学）
哥德尔的本体论证明已经分析了第一次与前所未有的详细程度和形式的帮助下，高阶定理证明。以下是已经完成的（并按此顺序）：一个详细的自然演绎证明。TPTP THF语法中公理、定义和定理的形式化。使用Nitpick自动验证公理和定义的一致性。自动证明定理与证明LEO-II和Satallax。使用Coq证明助手的逐步形式化。使用Isabelle证明助手的形式化，其中定理（和一些额外的引理）已使用Sledgehammer和Metis自动化。
2017-09-03 cs.AI cs.LO math.LO
A formalization of forcing and the unprovability of the continuum hypothesis
我们在精益3定理证明器中使用布尔值模型描述了强制的形式化，包括强制的基本定理和一阶逻辑与布尔值可靠性定理的深度嵌入。作为我们的框架的应用程序，我们专门我们的建设，定期开放的康托空间$2^{ω_2 \times ω}$的布尔代数，并正式验证失败的连续假设在由此产生的模型。
2019-04-23 cs.LO math.LO
A Constructive Formalization of the Weak Perfect Graph Theorem
完美图定理是描述图$G$的团数$ω(G) $与色数$χ(G) $之间关系的重要图论结果。一个图$G$称为\emph{perfect}，如果对于$G$的每个导出子图$H$都有$χ(H)=ω(H)$.强完美图定理（SPGT）指出一个图是完美的当且仅当它不包含奇洞（或奇反洞）作为它的导出子图。弱完美图定理（WPGT）指出，一个图是完美的，当且仅当它的补图是完美的。在本文中，我们提出了一个正式的框架，工作与有限的简单图。我们在Coq证明助手中建模有限简单图，将其顶点表示为可数无限域上的有限集。我们认为，这种方法提供了一个正式的框架，它是方便的工作与不同类型的图的构造（或扩展）涉及的证明的Lovász复制引理（LRL），这也是关键的结果，用于证明弱完美图定理。最后，我们使用这个设置开发一个建设性的形式化的弱完美图定理。
2019-12-04 cs.DM cs.LO cs.PL
Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant
我们提出的证明丢番图'第20个问题（第六册丢番图'算术），其中包括想知道是否存在直角三角形的双方可以衡量为整数和其表面可能是一个广场。这个问题在17世纪被费马否定地解决了，他使用了无限下降的“奇妙”方法（ipse difficult Fermat）。这种方法，在历史上是归纳法的第一次使用，包括产生越来越小的非负整数解，假设存在一个;这自然会导致反证推理，因为我们以零为界。我们描述了这种证明的形式化已进行的Coq证明助手。此外，作为一个直接的和同样具有历史意义的应用，我们还提供了费马最后定理（n=4）的证明（由费马），以及Coq中相应的形式化。
2005-10-04 cs.LO cs.SE math.NT
Further Formalization of the Process Algebra CCS in HOL4
在这个项目中，我们已经扩展了以前的工作在HOL4的进程代数CCS的形式化。我们增加了对弱互模拟等价和观测同余（有根弱等价）的完全支持，以及相关的定义、定理和代数定律。一些深引理也在这个项目中得到了形式化的证明，包括邓引理、Hennessy引理和几种版本的“弱等价中包含的Coarse同余”。对于最后一个定理，我们已经证明了基于序数的完整版本（没有任何假设）。
2017-07-27 cs.LO
A Formalization of Unique Solutions of Equations in Process Algebra
在这篇论文中，一个全面的形式化米尔纳的演算通信系统（也称为CCS）已经完成了在HOL定理证明器（HOL 4），在HOL 88的旧工作的基础上。这包括强/弱互模拟等价和观测同余的所有经典性质，CCS的同余理论，各种版本的“互模拟高达”技术，以及几个深层定理，即“弱等价中包含的粗同余”，以及Milner书中的三个版本的“方程的唯一解”定理。这项工作进一步扩展到支持并发理论的最新发展，即“收缩”关系和相关的“收缩的唯一解”定理由博洛尼亚大学的Davide Sangiorgi教授发现。因此，本文还形式化了一个相当完整的CCS“收缩”（以及一个类似的关系称为“膨胀”）理论。在此基础上，作者发现了一种新的收缩变形，称为“观测收缩”。形式上证明了这种新的关系是CCS过程的直和所保持的，并且具有一种更优美的形式的“压缩唯一解”定理，而不受CCS文法的任何限制.
2017-12-05 cs.LO cs.PL
Geometric Formalization of First-Order Stochastic Dominance in $N$ Dimensions: A Tractable Path to Multi-Dimensional Economic Decision Analysis
针对多维随机占优传统分析方法形式化难度高的问题，本文提出N维一阶随机占优的几何刻画方法，用Lean 4完成形式化验证，可直接支持多类经济金融问题的严谨分析。
2025-05-19 cs.LO econ.TH q-fin.CP
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
Formalization of Auslander--Buchsbaum--Serre criterion in Lean4
本文在Lean4中形式化了Auslander-Buchsbaum-Serre准则，通过Ext函子定义深度，证明正则局部环的性质，并发展了Cohen-Macaulay模的理论。
2025-12-09 cs.FL cs.LO math.AC
An Isabelle formalization of protocol-independent secrecy with an application to e-commerce
建立了一个与协议无关的保密定理，并将其应用于几个非平凡协议。特别是，它适用于保护自由漫游的移动代理做比较购物的计算结果提出的协议。这里提出的所有结果已经正式证明在伊莎贝尔的建设拉里保尔森的归纳方法。因此，这提供了一个可以应用于其他协议的一般定理库。
2006-10-11 cs.LO
Theory-Scale Auto-Formalization of Logics for Computer Science
提出LCS-Bench基准，通过半自动化流水线构建包含327个教材条目、4076个Lean声明的理论级自动形式化数据集，评估14个模型，发现最先进模型仅达20.1%准确率。
2026-06-26 cs.LG cs.LO cs.PL
Formalizing Pick's Theorem in Isabelle/HOL
本研究受HOL Light中皮克定理形式化工作启发，在Isabelle/HOL中调整证明策略规避了多边形内部分割的核心证明难点，同时从基础层面扩充现有几何库，完成皮克定理的形式化并反思了策略优劣。
2024-05-03 cs.LO
Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory
Department of Biostatistics & Bioinformatics, Duke University（杜克大学生物统计与生物信息学系）；Department of Mathematical Sciences, Carnegie Mellon University（卡内基梅隆大学数学科学系）；Department of Biostatistics, Harvard T.H. Chan School of Public Health（哈佛大学陈曾熙公共卫生学院生物统计系）
提出一种假设约束的多智能体Lean 4形式化流程，通过七个专业角色协调工作，实现渐近统计理论中参数和半参数模型的形式化，确保公理干净且忠实于原文。
2026-06-23 cs.AI cs.LG cs.LO
A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
Microsoft（微软）；Centro de Informática, Universidade Federal de Pernambuco（计算机中心，伯南布哥联邦大学）
本文在Lean 4中形式化了Nagata因子定理，证明若R为Noetherian域，S为R的素数生成子半群且S^{-1}R为UFD，则R本身为UFD。同时形式化了两个基于Nagata的证明，展示R[X]为UFD的条件，并推导出R[X][Y]的结论。
2026-04-06 cs.LO math.AC
Towards a constructive formalization of Perfect Graph Theorems
图的团数$ω(G) $和色数$χ(G) $之间的相互作用是图论中一个很好的研究课题。完美图定理可能是这方面最重要的结果。图$G$称为\emph{perfect}，如果对$G$的每个导出子图$H$都有$χ(H)=ω(H)$。强完美图定理（SPGT）指出一个图是完美的当且仅当它不包含奇洞（或奇反洞）作为它的导出子图。弱完美图定理（WPGT）指出，一个图是完美的，当且仅当它的补图是完美的。在本文中，我们提出了一个正式的框架来验证这些结果。我们在Coq证明助手的构造性类型论中对有限简单图进行建模，并在此框架下给出了弱完美图定理证明的核心思想Lovász复制引理的构造性证明.
2018-12-28 cs.DM cs.LO
Formalization of QFT
Center Of Mathematical Sciences And Applications, Harvard University（哈佛大学数学科学与应用中心）；Jefferson Physical Laboratory, Harvard University（哈佛大学杰斐逊物理实验室）；MIT（麻省理工学院）
本文通过Lean 4证明助手形式化了构造自由玻色量子场论并证明其满足Glimm-Jaffe公理，展示了数学物理中的延伸论证可通过现有AI工具转化为机器验证证明。
2026-03-16 cs.LO hep-th math-ph
Formalization of Complex Vectors in Higher-Order Logic
复向量分析在物理学和工程学等许多学科中被广泛用于分析连续系统。在本文中，我们提出了一个高阶逻辑形式化的复向量空间，以方便进行这种分析的声音的核心定理证明：HOL光。我们对复向量的定义建立在复数和实向量的定义之上。这种扩展使我们能够广泛地受益于已经验证的定理的基础上复杂的分析和真正的向量分析。为了显示我们的图书馆的实用性，我们采用它来形式化电磁场，并证明了平面波的反射定律。
2014-05-15 cs.LO
Formalization of Amicable Numbers Theory
School of Electronics and Information, Shanghai Dianji University（上海电机学院电子信息学院）
本文在Lean~4中形式化了亲和数理论，包括亲和数对的定义、Thābit公式和欧拉规则的证明，以及Borho-Hoffmann方法的首次完整形式化。
2026-01-12 cs.LO
Formalization of Lerch's Theorem using HOL Light
拉普拉斯变换是一种代数方法，广泛用于分析物理系统，通过求解微分方程建模其动态或通过评估其传递函数。首先用微分方程建立系统的动力学模型，然后利用拉普拉斯变换将微分方程转化为等价的代数方程。这些方程可以进一步简化，以获得系统的传递函数或在频域中求出微分方程的解。其次，拉普拉斯变换的唯一性提供了这些微分方程在时域中的解。传统的基于拉普拉斯变换的分析技术，即，纸笔证明和计算机模拟方法由于其固有的局限性而容易出错，因此不适合于系统的分析。高阶逻辑定理证明可以克服这些技术的局限性，并可以确保系统的准确分析。在本文中，我们扩展了拉普拉斯变换的高阶逻辑形式化，其中包括拉普拉斯变换的形式化定义及其各种经典性质的验证。本文的主要贡献之一是Lerch定理的形式化，该定理描述了Laplace变换的唯一性，因此在频域求解线性微分方程中起着至关重要的作用。为了说明，我们提出了一个$4$ - $π$软错误串扰模型，这是广泛使用的纳米技术，如集成电路（IC）的形式化分析。
2018-06-08 cs.LO
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
UT Austin（德克萨斯大学奥斯汀分校）
本研究提出多语言基准PutnamBench，包含普特南竞赛640条定理的多证明器形式化表述，评估发现现有神经与符号定理证明器仅能求解少量问题，为神经定理证明研究提供了高难度开放挑战基准。
2024-11-03 cs.AI cs.CL cs.LG
Formalization of Bond Graph using Higher-order-logic Theorem Proving
键合图是描述复杂工程和物理系统动力学的统一图形方法，广泛应用于电气、机械、医学、热力学和流体力学等领域。传统上，这些动态分析使用纸和笔的证明方法和基于计算机的技术。然而，这两种技术都有其固有的局限性，如人为错误倾向，结果的近似和巨大的计算需求。因此，这些技术不能被信任用于执行基于键合图的动态分析系统的安全关键领域，如机器人和医学。形式化方法，特别是高阶逻辑定理证明，可以克服这些传统方法的缺点，并提供这些系统的准确分析。它已被广泛应用于工程和物理系统的动力学分析。在本文中，我们提出使用高阶逻辑定理证明进行键合图的物理系统的分析。特别是，我们提供了键合图的形式化，其中主要包括功能，允许键合图转换到其相应的数学模型（状态空间模型）和验证其各种属性，如，稳定性。为了说明我们所提出的方法的实际有效性，我们提出了正式的稳定性分析的假肢机电一体化的手使用HOL光定理证明。此外，为了帮助HOL中的非专家，我们在MATLAB中编码我们正式验证的稳定性定理，以执行拟人假肢机电一体化手的稳定性分析。
2021-11-24 cs.LO
A formally verified proof of the Central Limit Theorem
我们描述了一个证明的中心极限定理，已正式核实的伊莎贝尔证明助手。我们的形式化的基础上，并扩展伊莎贝尔的图书馆分析和测量理论的概率。该定理的证明使用特征函数，这是一种傅立叶变换，以证明，在适当的假设下，随机变量的总和弱收敛到标准正态分布。我们还讨论了支持正式化的库和基础设施，并反思了我们从这一努力中吸取的一些教训。
2017-02-01 cs.LO cs.MS math.PR
A formalization of convex polyhedra based on the simplex method
在证明助手Coq中给出了凸多面体的形式化。我们的工作的基石是一个完整的实施单纯形法，连同证明其正确性和终止。这允许我们以有效的方式定义多面体上的基本谓词（即，作为程序），并将它们与相应的通常的逻辑对应物相关联。为此，我们广泛使用布尔反射方法。这种方法的好处是，我们可以很容易地推导出多面体上的几个基本结果的证明，如Farkas引理，线性规划的对偶定理和Minkowski定理。
2018-08-10 cs.LO math.CO math.OC
A Formalization of the Process Algebra CCS in HOL4
进程代数CCS的旧形式化（无值传递，具有显式重新标记运算符）已从HOL 88定理证明器移植到HOL 4（Kananaskis-11及更高版本）。通过SOS（Structured操作语义）推理规则定义CCS过程之间的转换，并基于SOS转换规则证明所有代数定律（包括展开定理）。我们已经使用HOL 4的新的共归纳关系支持重新定义强和弱互模拟等价，并表明新的定义是等价的旧的。最后，还有自动检测CCS转换的决策过程。其目的是提供一个最新的健全和有效的工具来支持CCS的验证和推理，并提供了一个形式逻辑的基础上进一步的理论发展的并发理论。
2017-06-17 cs.LO
A Unifying Framework for Global Optimization: From Theory to Formalization
本文提出一个统一的测度理论框架，用于严格研究随机迭代全局优化算法，并在Lean中形式化证明了一般一致性定理。
2026-10-12 cs.FL cs.LO math.OC
Formalization and Implementation of Algebraic Methods in Geometry
我们描述了我们正在进行的项目的代数方法的形式化几何定理证明（吴的方法和Groebner基地的方法），其实施和整合的教育工具。该项目包括对Isabelle/HOL证明助手中的代数方法进行形式化验证，并开发一个新的、开源的代数方法Java实现。该项目应填补这一领域仍然存在的一些空白（例如，代数方法和综合几何之间缺乏正式的联系，以及缺乏适合于与动态几何工具集成的代数方法的独立实现），并且应该能够在教育中实现定理证明的新应用。
2012-02-22 cs.LO cs.MS cs.SC
A Formalization of the Laplace Transform and Its Inversion in Lean 4
Technion – Israel Institute of Technology（以色列理工学院）
在Lean 4中形式化复值函数的拉普拉斯变换及相关规则，证明其布罗米奇型逆变换定理，应用于谐振子拉普拉斯域解的形式化，并探讨相关挑战。
2026-08-10 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
A Coq Formalization of the Bochner integral
Bochner积分是Lebesgue积分的推广，适用于取值于Banach空间的函数。因此，它的数学定义和形式化的Coq证明助手更具挑战性，因为我们不能依赖于实数的性质。我们的贡献包括一个原始的形式化的简单功能，Bochner可积性定义的依赖型，和建设的证明可测函数的可积性在温和的假设（弱可分性）。然后，我们定义了Bochner积分，并证明了几个定理，包括控制收敛性和与现有的非负函数的Lebesgue积分形式化的等价性。
2022-02-10 cs.LO math.FA
Formalization of Transform Methods using HOL Light
变换方法，如拉普拉斯和傅立叶，经常用于分析工程和物理系统的动态行为，基于其传递函数和频率响应或其相应微分方程的解。在本文中，我们提出了一个正在进行的项目，重点是高阶逻辑形式化的转换方法使用HOL光定理证明。特别是，我们提出了形式化的动机，其次是相关的工作。接下来，我们介绍迄今为止完成的任务，同时强调在正式化过程中面临的一些挑战。最后，我们提出了一个路线图，以实现我们的目标，目前的状态和未来的目标，这个项目。
2017-05-29 cs.LO
A Formalization of the Generalized Quantum Stein's Lemma in Lean
该工作用 Lean 定理证明器形式化了广义量子斯坦引理的修正证明，修正了原证明中的小瑕疵，并完善了量子资源理论定义，为量子信息形式化提供了稳健基础。
2025-10-09 cs.LO quant-ph
A Coq Formalization of Lebesgue Integration of Nonnegative Functions
积分和微分一样，是一种基本的微积分工具，广泛应用于许多科学领域。在正式的证明助手中形式化积分的数学概念和相关结果有助于直接或间接地对涉及使用积分的数值程序的正确性提供最高的置信度。由于它能够将黎曼积分扩展到广泛的一类不规则函数，以及定义在比实数线更一般的空间上的函数，勒贝格积分非常适合用于数学领域，如概率论，数值数学和实分析。本文给出了$σ$ -代数、测度、单函数和非负可测函数的积分的Coq形式化，以及Beppo Levi（单调收敛）定理和Fatou引理的完整形式证明.超过一个普通的形式化的已知文献，我们提出了几个设计选择，以平衡数学可读性和可用性之间的和谐Coq定理。这些结果是走向$L^p$ ~空间如Banach空间形式化的第一个里程碑。
2021-12-09 cs.LO math.FA
Formalization of non-Archimedean functional analysis 1: spherically complete spaces
Institute for Theoretical Sciences, Westlake University（西湖大学理论科学研究院）
本文提出非阿基米德泛函分析中球面完备空间的正式化，涵盖定义、性质及应用，如Birkhoff-James正交性和Hahn-Banach定理。
2026-08-25 cs.LO math.FA math.NT
Fourier Series Formalization in ACL2(r)
我们在ACL 2（r）逻辑中形式化了傅立叶级数的一些基本性质，ACL 2（r）是ACL 2的一个变体，支持通过非标准分析的方式对实数和复数进行推理。更具体地说，我们扩展了一个框架，正式评估定积分的实值，连续函数使用微积分第二基本定理。我们的扩展框架也适用于包含自由参数的函数。利用这个框架，我们能够证明三角函数之间的正交关系，这是傅立叶级数分析的基本性质。指数和的定积分的求和规则也形式化的应用扩展的框架连同微积分的第一基本定理和微分的求和规则。然后从正交性关系和积分求和法则出发，形式化了周期函数的傅里叶系数公式。因此，傅立叶和的唯一性是一个直接的推论。给出了无穷级数定积分求和规则在ACL ~ 2（r）中的形式化。这个任务的一部分是证明Dini一致收敛定理和极限函数在一定条件下的连续性。证明这些定理的一个关键技术是应用非标准分析的溢出原理。
2015-09-21 cs.LO
FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature $-$ Toward the Formalization of the Classification of Finite Simple Groups
University of Warwick（华威大学）
本研究提出AI辅助工作流FormaTheoria，应用于有限单群分类定理的形式化，构建了经机器检查的Lean开发项目，验证了深度依赖的有限群理论，为推进该定理的形式化奠定基础。
2026-08-12 cs.LO math.GR
ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings
Georgia Institute of Technology（佐治亚理工学院）；Bogazici University（博阿齐奇大学）
ProofBridge通过联合嵌入模型实现自然语言定理和证明到Lean 4的自动形式化，结合检索增强微调和迭代证明修复，提升语义和类型正确性。
2026-03-29 cs.AI cs.LO
A Formalization of Finite Group Theory
以前在ACL 2和Nqthm中的群论公式，基于“encapsulate”或“defn-sk”，由于它们未能提供一条通过归纳证明群阶的路径而受到限制，这是该领域中最有趣的结果所必需的，超越了拉格朗日定理（断言群阶被子群阶整除）。我们描述了一种替代方法，有限群理论，弥补这一不足，基于一个明确的表示一组作为一个操作表。我们定义了一个“defgroup”宏生成参数化的家庭的群体，我们适用于加法和乘法组的整数模n，对称群，任意商群，和循环子群。除了证明拉格朗日定理，我们提出了一个归纳证明的交换情况下的柯西定理：如果一个集团G的秩序是整除由一个素数p，那么G有一个元素的秩序p。
2022-05-24 cs.LO
Formalization of $p$-adic $L$-functions in Lean 3
The Euler-- Riemann zeta function is a largely studied numbertheoretic object, and the birthplace of several conjectures, such as the Riemann Hypothesis . Different approaches are used to study it, including $p$ -adic analysis : deriving information from $p$ -adic zeta functions. A generalized version of $p$ -adic zeta functions ( Riemann zeta function ) are $p$ -adic $L$ -functions (resp. Dirichlet $L$ -functions). This paper describes formalization of $p$ -adic $L$ -functions in an interactive theorem prover Lean 3. Kubota--Leopoldt $p$ -adic $L$ -functions are meromorphic functions emerging…
2023-02-28 cs.LO math.NT
Formal Component-Based Semantics
为提高程序设计语言语义的可伸缩性，提出了一种解决方案，即由Peter D.苔藓预计该框架也可以有效地用于模块化Meta理论推理。本文提出了一种形式化的定理证明器Coq的基于一致性的语义。它基于模块化SOS（SOS的一个变体），并且基本上使用了依赖类型，同时受益于类型类。这种形式化构成了对定理证明器中的模块化Meta理论形式化的贡献。作为一个小的例子，一个小型语言的确定性的模块化证明。
2011-08-16 cs.LO
Long-horizon autoformalization of a core theorem underlying MIP* = RE
Munich Center for Quantum Science and Technology (MCQST)（慕尼黑量子科学与技术中心）；Tsinghua University（清华大学）
FormalFlow系统通过人类监督下的AI证明代理协作，在63天内完成了MIP* = RE核心定理的Lean 4机器检查证明，生成了126,367行代码，为量子复杂性提供了验证基础。
2026-10-22 cs.AI cs.LO quant-ph
FindFacts: A Scalable Theorem Search
伊莎贝尔正式证明档案（AFP）在2019年底已经增长到500多篇文章。与此同时，在其中找到形式化并没有变得更容易。在撰写本文时，网站特定的AFP谷歌搜索和伊莎贝尔发现理论分别。find_consts命令（仅适用于导入的理论）仍然是Isabelle中唯一可用的形式化工具。我们提出FindFacts，一个新的特定领域的搜索工具，正式伊莎贝尔理论的内容。而不是利用长期统一，我们解决了一个经典的钻取下搜索引擎的问题。我们特别强调的可扩展性的搜索系统，使整个AFP可以交互式搜索。
2022-04-27 cs.LO
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
Microsoft（微软）；Centro de Informática, Universidade Federal de Pernambuco（巴西联邦伯南布哥大学信息学中心）
本文在Lean 4中形式化了任意维数的斯托克斯定理，通过弗雷歇导数实现真正微分形式拉回，并结合mathlib4的extDeriv抽象，扩展了链级斯托克斯理论，验证了奇异立方链的d²=0性质。
2026-05-01 cs.LO math.DG
A Formalization of the Mean-Field Derivation of the Vlasov Equation
Stanford University（斯坦福大学）；Massachusetts Institute of Technology（麻省理工学院）
该研究以数学家指导AI在Lean 4中形式化研究成果为案例，将其构建为形式化游戏。通过此方式对非线性弗拉索夫方程适定性完整形式化，展示了开发过程及成果，还介绍了最优传输机制的分离情况及开发时间等，为形式化研究提供了新方法。
2026-07-21 cs.AI cs.LO math-ph
A formal proof of the Ramanujan--Nagell theorem in Lean 4
利用 Lean 交互式定理证明器和 Mathlib 库，完整形式化了 Ramanujan–Nagell 定理，即丢番图方程 $x^2 + 7 = 2^n$ 仅有五个整数解。
2026-06-01 cs.LO math.NT
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
Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL
该研究在 Isabelle/HOL 中完成了 STARK 风格透明证明协议的形式化，构建了含证明者/验证者可执行模型等内容的开发成果，为相关领域提供了形式化方法层面的支撑。
2026-09-23 cs.LO cs.SE
Formalization of Biological Circuit Block Diagrams for formally analyzing Biomedical Control Systems in pHRI Applications
本文提出在pHRI场景下用HOL Light定理证明器对生物医学控制系统框图进行形式化建模与演绎推理，并以超滤透析控制为例验证方法有效性。
2024-12-31 cs.LO
AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
Georgia Institute of Technology（佐治亚理工学院）；University of Pennsylvania（宾夕法尼亚大学）；Foothill College（山麓学院）；Rutgers University（罗格斯大学）；Simon Fraser University（西蒙弗雷泽大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）
AIProver 通过证书驱动的 HarnessEvolve 演化工具，联合后训练 119B 模型，在 LoCoBench 上实现研究级证明自动形式化，显著提升语义正确性并降低成本。
2026-10-06 cs.AI cs.LG cs.LO
Initial Semantics for higher-order typed syntax in Coq
初始语义学旨在将与签名相关联的语法表征为某个类别的初始对象。我们提出了一个初步的语义结果类型的高阶语法连同其形式化的Coq证明助手。主要定理在2010年第二作者的博士论文中首次在纸上证明，并在不久后正式验证。对于固定的对象类型集合T上的简单类型绑定签名S，我们将一个称为S的表示范畴的范畴联系起来。我们证明了这个范畴有一个初始对象Sigma（S）。从它的构造中可以清楚地看出，对象Sigma（S）值得与S相关联的名称抽象语法。通过大量使用依赖类型，我们的定理在证明助手Coq中实现并证明了正确性。通过单子的方法产生了一种语法实现，其中术语和变量都是固有类型的，即对象类型反映在元级别类型中。这篇文章被看作是一篇研究文章，而不是关于一个经典数学结果的形式化。我们的定理的性质-涉及冗长，技术证明和复杂的代数结构-使它特别有趣的形式化验证。我们的目标是促进使用计算机定理证明器作为研究工具，并因此，一种新的方式出版的数学成果：一个平行的描述定理及其形式化应允许验证正确转录的定义和声明到证明助手，和简单，但技术证明应该很好地隐藏在一个数字图书馆。我们认为，科克的丰富的类型论，结合其各种功能，如隐式参数，允许一个特别可读的形式化，因此非常适合数学交流。
2011-09-17 cs.LO math.LO
Formalized Hopfield Networks and Boltzmann Machines
Università Cattolica del Sacro Cuore（天主教圣心大学）；Radboud University Nijmegen（拉德堡德大学尼姆维根分校）
本文通过形式化方法验证了Hopfield网络和Boltzmann机的收敛性与正确性，证明了Hebbian学习和遍历性的数学基础。
2026-09-16 cs.LG cs.LO
A Lean 4 Formalization of Scott's Continuous Lattices (1972)
Catskills Research Company（卡茨基尔研究公司）
用 Lean 4 形式化验证了 Scott 1972 年论文中连续格与 λ-演算模型的全部 43 个编号结果，包括单射 T₀-空间与连续格的等价性及 D∞ 构造。
2026-09-09 cs.LO math.LO
Munkres' General Topology Autoformalized in Isabelle/HOL
Independent（独立研究者）；Aalborg University（奥尔堡大学）；University of Melbourne（墨尔本大学）；AI4REASON and University of Gothenburg / Chalmers University（AI4REASON 和哥德堡大学 / 查尔姆斯理工大学）
本研究利用LLM辅助在Isabelle/HOL中自动形式化Munkres泛拓扑教材，生成85000余行代码，涵盖39章节，证明包括Tychonoff定理等核心结果，方法结合声明性证明与sledgehammer工具，展现高效形式化潜力。
2026-04-08 cs.AI cs.LG cs.LO
