A Formal Proof of the Strong Normalization Theorem for System T in Agda
我们提出了一个框架的正式元理论的lambda演算在一阶语法，有两种名称，一个代表自由和绑定变量，和其他常量，并通过使用斯托顿的多重替换。在这个框架之上，我们形式化了Girard对简单类型λ演算和系统T的强规范化定理的证明。对于后者，我们也提出了一个简化的原始证明。整个开发过程都使用Agda系统进行了机器检查。
2023-03-23 cs.LO
An Evaluation of the Archive of Formal Proofs
正式证明档案（AFP）是Isabelle证明助手的正式证明的在线存储库。它是出版、发现和查看校样库的中心位置。我们于2020年11月进行网上调查，以评估网站的适合性。在这份报告中，我们提出并讨论了结果，结果表明，该网站的长期用户普遍对法新社感到满意，但有一些领域，如导航，搜索和脚本浏览，需要改进。
2021-04-02 cs.DL cs.LO
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
本文提出了在Isabelle/HOL中用于关联结构证明的形式化线性代数技术，首次完成了Fisher不等式的形式化，并展示了该技术可适应组合学的未来形式化工作。
2022-07-06 cs.LO math.CO
Pseudo-Formalization for Automatic Proof Verification
本文提出了一种名为伪形式化的证明格式，该格式在保持自然语言灵活性的同时，保留了形式证明的模块性和精确性，通过块验证算法实现了对自然语言证明的高效验证，其在错误发现的精度和召回率上优于现有基线方法。
2026-10-02 cs.LG cs.LO
Translating Informal Proofs into Formal Proofs Using a Chain of States
School of Mathematical Sciences, Peking University, Beijing 100871, P.R. China（北京大学数学科学学院）
通过状态链方法将非正式证明转换为正式证明，提升证明生成效率和准确性。
2025-12-12 cs.AI cs.LO
Logipedia: a multi-system encyclopedia of formal proofs
针对形式化证明库跨系统可用性差、易因系统停止维护而遗失的问题，研究提出构建基于逻辑框架与反推数学、以标准语言表述证明的多系统在线形式化证明百科全书Logipedia，实现证明跨系统复用。
2023-04-06 cs.LO
Formal verification of a proof procedure for the description logic ALC
描述逻辑（DL）是一种用于以结构化和形式化的方式表示和推理应用领域知识的语言。为了实现这一目标，已经实施了几个证明器，如RACER和FaCT++，但这些证明器本身尚未获得认证。为了确保这些DL中推导的合理性，有必要正式验证这些推理机应用的推导。形式化方法为证明过程的规范和验证提供了强大的工具，其中包括证明过程的可靠性，完整性和终止性等属性的方法。在本文中，我们提出了一个证明过程的描述逻辑ALC的定义，基于语义tableau方法。我们通过使用Isabelle证明助手证明其可靠性、完备性和终止性来确保证明器的有效性。证明分为两个阶段进行，首先在抽象级别上建立这些属性，然后将它们实例化以用于基于列表的实现。
2013-07-31 cs.LO
Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
Southwest University（西南大学）；State Key Laboratory of Intelligent Vehicle Safety Technology（智能车辆安全全国重点实验室）；Aarhus University（奥胡斯大学）；University of York（约克大学）
本文在Isabelle/HOL中形式化分析了Sigmoid函数并证明了通用逼近定理，填补了形式化证明库的空白，提升了神经网络的可信度。
2025-12-03 cs.LO cs.SE
A Formal Correctness Proof of Edmonds' Blossom Shrinking Algorithm
King’s College London（伦敦国王学院）；Max Planck Institute for Informatics（马克斯·普朗克信息学研究所）
本文首次对Edmonds blossom缩小算法进行了形式正确性证明，形式化了算法的核心数学结构和性质，并提供了详细的正确性证明。
2025-12-19 cs.DS cs.LO
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
我们在这里研究了一个新版本的归纳构造演算（CIC），证明助手Coq是基于它的：一致归纳构造演算，它通过构建任意的一阶决策过程来真正扩展CIC：deduction仍然负责CIC内核，而计算则外包给专用的一阶决策程序，这些程序可以从货架上取下来，只要它们提供证明证书。整个系统的可靠性是证书检查器和内核可靠性的增量属性。一个详细的例子表明，由此产生的证明风格变得更接近工作数学家。
2008-04-23 cs.LO
Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials
我们描述的形式化Coq的证明，数字e和$π$是超越的。这个证明是在两个数学领域的交界处，这两个领域通常被分开考虑：微积分（实数和初等复分析）和代数。对于微积分的工作，我们依赖于Coquelicot库，对于代数的工作，我们依赖于Mathematical Components库。此外，我们的形式化证明的一些元素来源于更古老的库，用于Coq分布中包含的实数。$π$的情况下广泛依赖于多变量多项式的属性，这个实验也是一个机会，把测试这些多变量多项式的新开发的库。
2015-12-09 cs.LO
Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
本文在Lean 4中用Mathlib证明了Wolstenholme定理，通过展开移位阶乘积并利用幂和消失性，展示了其在模p^3下的等价性。
2026-08-11 cs.LO
A formal proof of the Kepler conjecture
本文介绍了一个形式化的证明开普勒猜想的稠密球包装的结合HOL光和Isabelle证明助手。这篇论文构成了现已完成的Flyspeck项目的官方出版物。
2015-01-09 cs.LO math.MG
A Formal Proof of PAC Learnability for Decision Stumps
Boston College（波士顿学院）；University of Pittsburgh（匹兹堡大学）；IMDEA Software Institute（IMDEA软件研究所）
我们提出了一个正式的证明精益的可能近似正确（PAC）的概念类的决策树桩的可学习性。机器学习理论中的这一经典结果导出了简单类型分类器的错误概率上的界。虽然这样的证明似乎简单的纸上，分析和测量理论的微妙之处出现时，进行充分正式。我们的证明结构，以便分离的学习函数的确定性属性的推理证明的可测量性和概率分析。
2021-01-07 cs.LG cs.LO stat.ML
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
本文描述了离散实闭域在Coq证明助手中的形式化。这个抽象的结构捕捉例如实代数数的理论，一个具有良好算法性质的实数的可判定子集。实代数数和更一般的半代数簇的理论是实分析中许多有效方法的核心，包括非线性算术的决策过程或实值函数的优化方法。在定义了离散实闭域的抽象结构和多项式实根的基本理论之后，根据计算机代数中关于量词消去的标准文献，给出了一个基于伪余项序列的代数证明的形式化.这种形式化涵盖了理论的很大一部分，这是在计算机代数实践中实现的有效算法的基础。这项工作的成功为这些有效方法的正式认证铺平了道路。
2012-02-15 cs.LO
Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs
在过去的几年里，伊莎贝尔正式证明档案已经发展到相当大的规模。它弥补了一个令人印象深刻的机构的研究，使一些统计方法的各个方面的定理证明，并尚未被用尽。然而，不断增长的规模也带来了一些挑战：材料变得越来越难找到，可重用性和易于理解变得更加重要。本文总结了我在这些课题上的研究计划，并简要介绍了初步的结果，这些结果表明文档依赖图的节点入度服从无标度分布。
2022-09-27 cs.LO
A formal proof of Hensel's lemma over the p-adic integers
$p$ -进数域$\mathbb{Q}_p$和$p$ -进整数环$\mathbb{Z}_p$是现代数论的重要构造. Hensel引理被Gouvêa描述为“$p$ -adic数的最重要的代数性质”，证明了在初始种子点的条件下，$\mathbb{Z}_p$上多项式的根的存在性。对于$p$ -自基，该定理可以在比一般环弱得多的假设下得到证明。我们构造$\mathbb{Q}_p$和$\mathbb{Z}_p$在精益证明助手，与各种相关的代数性质，并正式证明强形式的亨塞尔引理。证明是代数和分析推理的交叉点，并演示了精益数学库如何处理这样一个异构的主题。
2019-09-25 cs.LO
Formal Proof of SCHUR Conjugate Function
我们工作的主要目标是形式化地证明SCHUR软件（一个用于李群和对称函数特征计算的交互式程序）的关键命令的正确性。计算的核心依赖于组合结构的枚举和操作。作为第一个“概念证明”，我们提出了一个形式证明的共轭函数，写在C。此函数计算整数分区的共轭。为了正式证明这个程序，我们使用了Frama-C软件。它允许我们注释C函数并生成证明义务，这些义务使用几个自动定理证明器进行证明。本文还借鉴方法论，讨论了如何形式化证明这类程序。
2010-04-28 cs.LO cs.MS cs.SC
ACL2 Proofs of Nonlinear Inequalities with Imandra
本文提出ACL2与Imandra的集成，利用Imandra的非线性决策过程生成证明，推理在实数域进行，证明在有理数域有效，并可在ACL2和ACL2(r)中运行，证明从Positivstellensatz反驳中提取，通过凸优化找到。
2023-11-15 cs.LO cs.SC
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
这个扩展的抽象是关于努力建立一个正式的描述的三角剖分算法，从一个天真的描述的算法，三角形，边缘和三角剖分简单地给出了作为集和最复杂的概念是那些边界和分离的边缘。当执行有关该算法的证明，对称性的问题出现，本博览会试图给这些对称性如何处理的帐户。所有这些工作都依赖于Coq和数学组件库的正式开发。
2018-09-03 cs.CG cs.LO
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
2021-02-11 cs.LO math.LO
Towards Verifying Nonlinear Integer Arithmetic
我们消除了一个关键的路障，有效地验证非线性整数运算使用CDCL SAT求解器，通过展示如何构建最广泛使用的乘法器电路的许多属性的短分辨率证明。这种简短的证明被证明是不存在的。更准确地说，我们给出了n^{O（1）}大小的正则分辨率证明的任意次数2的身份阵列，对角，和布斯乘子和拟多项式- n^{O（\log n）}大小的证明这些身份华莱士树乘子。
2018-08-09 cs.LO
On Logic of Formal Provability and Explicit Proofs
1933年，哥德尔考虑了两种描述可证明性的模态方法。一个捕获了形式可证明性，并导致了逻辑GL和Solovay的完备性定理。另一种是以模态逻辑S4为基础，发展出阿特莫夫的证明逻辑LP。本文研究了作者提出的逻辑GLA，它是GL和LP语言的结合体。GLA具有Kripke风格的语义和相应的完备性定理。建立了GLA关于算术可证性语义的可靠性和完备性。
2014-05-11 cs.LO math.LO
A Unifying Framework for Global Optimization: From Theory to Formalization
本文提出一个统一的测度理论框架，用于严格研究随机迭代全局优化算法，并在Lean中形式化证明了一般一致性定理。
2026-10-12 cs.FL cs.LO math.OC
Isabelle technology for the Archive of Formal Proofs with application to MMT
本文概述了形式证明档案（AFP）背后的Isabelle技术。交互式开发和准交互式构建工作对逻辑（通常是Isabelle/HOL）、数学工具实现的Isabelle/ML和物理系统集成的Isabelle/Scala提出了显著的可扩展性要求--所有这些都集成在Isabelle/PIDE（Prover IDE）中。AFP的持续增长要求Isabelle的性能不断改进。这是一份关于Isabelle 2019（2019年6月）情况的报告，其中包括显着的附加组件，如证明器会话导出和无头PIDE，用于基于语义信息的自动更新。一个示例应用程序是Isabelle/MMT，它能够将所有Isabelle + AFP转换为OMDoc和RDF三元组，但将Isabelle技术重用于其他应用程序是直接的。
2019-06-11 cs.LO
Formal Semantics of a Classical-Quantum Language
我们调查的形式语义的一个简单的命令式语言，具有经典和量子结构。更具体地说，我们提供了一个操作语义，一个指称语义和两个霍尔风格的证明系统：一个抽象的和一个具体的。这两个证明系统是基于满意度的，灵感来自于Barthe等人的概率程序的程序逻辑。抽象的证明体系是健全的、相对完整的，而具体的证明体系只是健全的。
2021-07-02 cs.LO
QED at Large: A Survey of Engineering of Formally Verified Software
开发程序正确性的形式化证明可以增加实际和感知的可靠性，并有助于更好地理解程序规范及其基本假设。支持这种发展的工具已有40多年的历史，但直到最近才得到广泛的实际使用。基于机器检查的形式化证明的构建的项目现在达到了前所未有的规模，可以与大型软件项目相媲美，这导致了证明开发和维护的新挑战。尽管其日益重要，证明工程领域很少考虑自己的权利;相关的理论，技术和工具跨越许多领域和场所。这篇文献综述对程序正确性的证明工程有了全面的了解，包括在实践中的影响、基础、证明自动化、证明组织和实际证明开发。
2020-03-13 cs.LO cs.PL
A Formal Logic for Formal Category Theory (Extended Version)
我们提出了一个特定领域的类型理论的建设和证明范畴论。类型论公理化了范畴、函子、原函子和自然变换的广义形式的概念。类型论对标准谓词逻辑施加了一个有序的线性限制，它保证范畴之间的所有函数都是函子的，所有关系都是前函子的，所有转换都是自然的，不需要单独的证明。重要的范畴论证明，如米田引理和Co-yoneda引理成为关于单位、张量和（有序）函数类型之间关系的简单类型论证明，并且可以被视为谓词逻辑中定理的有序精化。类型论是虚拟装备范畴化模型的合理和完备的理论，它是对范畴论的内在和丰富。虽然我们的类型理论中的证明看起来像标准的基于集合的论点，但句法规则确保所有的证明和构造都可以扩展到丰富的内部设置。
2023-02-18 cs.LO math.CT
Formal Proof of a Wave Equation Resolution Scheme: the Method Error
针对一维声波方程的有限差分格式，在Coq中形式化证明其收敛性，首次实现此类数学证明的机器验证。
2011-11-09 cs.LO cs.NA math.NA
Formal Verification of Flow Equivalence in Desynchronized Designs
Cortadella，Kondratyev，Lavagno和Sotiriou的研究工作包括一个手写的证明，证明一个特定的握手协议保持了流等价性，一个基于同步锁存器的规范和它们的非同步化的加密数据异步实现之间的等价性概念。在这项工作中，我们确定了一个反例Cortadella等人。的证明说明了他们的协议实际上如何导致违反流等价性。然而，在他们的论文中确定的两个并发性较低的协议确实保持了流等价性。为了验证这一事实，我们形式化的Coq证明助手流等价，并提供机械化，机器检查证明我们的结果。
2020-04-06 cs.LO
The Lax-Milgram Theorem. A detailed proof to be formalized in Coq
INRIA（法国国家信息与自动化研究所）
本文提供了一个详细的手写证明，用于在Coq中形式化Lax-Milgram定理，该定理在有限元方法的数值模拟程序校验中起到关键作用。
2016-10-04 cs.LO cs.NA math.NA
Spreads and Packings of PG(3,2), Formally!
研究了如何在Coq证明助手中形式化最小射影空间PG（3，2）。然后，我们正式描述的蔓延和包装PG（3，2），以及他们的一些性质。形式化是相当简单的，然而，随着所涉及的对象数量的迅速增加，我们需要利用一些对称性参数以及智能证明技术来使证明搜索和验证更快，从而使用Coq证明助手更容易处理。这项工作可以被看作是形式化更高维的射影空间的第一步，例如PG（4，2），或更高阶的射影空间，例如PG（3，3）。
2022-01-03 cs.LO cs.SC
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations
本文提出了一个多元非线性不等式的形式化验证工具。我们的验证方法是基于泰勒近似的区间算术。我们的工具在HOL Light证明助手中实现，它能够验证矩形域上的多元非线性多项式和非多项式不等式。我们的工作的主要特点之一是一个有效的实现的验证过程，可以证明非平凡的高维不等式在几秒钟内。我们开发了验证工具作为Flyspeck项目（开普勒猜想的正式证明）的一部分。Flyspeck项目包括大约1000个非线性不等式。我们成功地测试了我们的方法对100多个Flyspeck不等式，并估计，形式化验证过程是约3000倍，比非正式的验证方法在C++中实现慢。我们还描述了未来的工作和前瞻性的优化我们的方法。
2013-01-08 cs.LO math.LO
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Université Paris-Saclay（巴黎萨克雷大学）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）；University of Greifswald（格赖夫斯瓦尔德大学）
本文提出一种在Dedukti框架中验证高阶逻辑自动定理证明器证明的通用方法论，应用于EP演算并集成至Leo-III，实现约80%证明步骤自动重构，成为首个支持独立可检查证明重构的高阶证明器。
2026-09-28 cs.LO
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques
Yonsei University（延世大学）；JENTI Inc.（JENTI公司）；Korea Institute for Advanced Study（韩国高等研究院）；Johann Radon Institute for Computational and Applied Mathematics（约翰·拉东计算与应用数学研究所）
本文聚焦形式化证明生成的挑战，将ChatGPT与基础搜索技术集成并结合Lean形式语言，在miniF2F数据集上以31.15%的通过率超越已知基准，扩展实验验证了模型在多场景的可比性能，为AI辅助形式化证明研究提供新方向。
2025-02-19 cs.AI cs.LO
Formal Proof of a Wave Equation Resolution Scheme: the Method Error
INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE（法国国家信息与自动化研究所）
本文在Coq中形式化了一维声波方程的最简单有限差分格式，并证明了其收敛性，首次实现了此类数学证明的机器检查。
2011-11-14 cs.LO cs.NA math.NA
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
计算机代数和数值分析中的许多问题都可以归结为计算或近似计算一个区间内多项式的实根。现有的主要证明助手中的已验证根计数过程主要基于经典的Sturm定理，该定理仅计数不同的根。在本文中，我们加强了根计数能力在Isabelle/HOL的第一次正式证明布丹-傅立叶定理。随后，基于笛卡尔的符号规则和泰勒移位，我们已经提供了一个验证过程，有效地过近似的实根的数量在一个区间内，计数重。为了准确地计算多重根，我们扩展了我们以前的Sturm定理的形式化。最后，我们结合验证组件在上述发展，以改善我们以前的认证复根计数程序的基础上柯西指数。我们相信这些经过验证的例程对于认证程序和构建策略至关重要。
2018-11-27 cs.LO
Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction
我们提出了一个自动化的演绎方法，使我们能够产生接近人类的直觉和实践的证明。该方法以表格为基础，比依赖子句形式的同类方法产生更自然的证明，并采用了追加演绎的原理，其中追加演绎的原理是用来丰富演绎系统的新的演绎规则。我们提出了两种实现这种方法，其中包括扩展的Zenon自动定理证明。第一个实现是一个版本专用于集理论的B正式的方法，而第二个实现是一个通用的版本能够处理任何一阶理论。我们还提供了几个问题的例子，这些问题可以通过这些工具来处理，并且来自不同的理论，例如B集理论或TPTP库的理论。
2015-01-06 cs.LO
Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language
Shanghai Jiao Tong University（上海交通大学）
提出一种宽松自然形式语言作为中间目标，通过分阶段精化实现可验证的数学自动形式化，结合规则转换与LLM启发式方法，并利用领域特定策略语言生成验证条件。
2026-06-24 cs.LO cs.PL
Abstraction-Based Proof Production in Formal Verification of Neural Networks
The Hebrew University of Jerusalem, Israel（耶路撒冷希伯来大学）；Technical University of Munich, Germany（慕尼黑技术大学）；Amherst College, USA（阿默斯特学院）
本文提出支持证明生成的基于抽象的 DNN 验证框架，将任务拆分为抽象网络正确性与抽象可靠性证明，填补可扩展性和形式化保证之间的缺口。
2025-06-11 cs.AI cs.LO
Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
Huawei Hong Kong Research Center（华为香港研究中心）；Department of Cultural Studies（文化研究系）；The Chinese University of Hong Kong（香港中文大学）
本文批判性地审视形式推理与自动定理证明领域的基准测试实践，倡导开放代码、开放数据及完整无错误的基准，并识别和提出消除贡献障碍的方法，以促进跨群体协作。
2025-07-07 cs.AI cs.LG cs.LO
The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
微积分是一种证明一阶逻辑中陈述有效性的形式主义。它通常用于计算机科学数学逻辑模块。形式证明在微积分中是有限的树，通过连续地将证明规则应用于公式，从而逐步简化它们。学生们经常在诸如形式逻辑和形式证明等主题所涉及的数学形式和抽象层次上挣扎。这些困难可以归类为句法或语义。在句法层面上，学生需要理解什么是正确形式的证明，如何在不脱离微积分的数学框架的情况下应用规则（例如在纸上），等等;除此之外，在语义层面上，学生需要掌握找到正确证明的策略。序贯微积分训练器是一个工具，旨在帮助学生学习正式证明给定语句的技术。在本文中，我们描述的教学动机背后的工具和技术，用于解决问题的句法以及语义层面上。
2018-03-05 cs.CY cs.LO
New Opportunities for the Formal Proof of Computational Real Geometry?
本文的目的是探讨这样一个问题：在什么程度上我们可以产生形式化的，机器可验证的，证明在真正的代数几何？“这个问题以前就被问过，但到目前为止，回答这些问题的主要算法还没有正式化。我们提出了一个论文，一个新的算法，用于确定可满足性的公式在实数通过圆柱代数覆盖[Ábrahám，达文波特，英格兰，克雷默，\emph{Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driver Search Using Cylindrical Algebraic Coverings}，2020]可能会提供跟踪和输出，使结果更容易受到机器验证比那些竞争的算法。
2020-04-08 cs.LO cs.SC
Eliciting implicit assumptions of proofs in the MIZAR Mathematical Library by property omission
Center for Artificial Intelligence（人工智能中心）；New University of Lisbon（里斯本新大学）
当使用交互式定理证明器进行形式化证明时，经常会发生关于数学概念的额外背景知识（声明性或过程性）被采用而形式化器没有显式地调用它，以帮助形式化器专注于证明的相关细节。在产生和研究形式化的数学论证的背景下，这种机制显然是有价值的。但我们可能并不总是希望压制背景知识。为了某些目的，尽可能精确地知道在形式证明中隐含地使用了什么背景知识是很重要的。在本文中，我们描述了在MIZAR数学库的正式数学证明上进行的一个实验，以引出一类隐含使用的背景知识：函数和关系的性质（例如，交换性、不对称性等）。
2011-09-03 cs.AI cs.LO math.LO
ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib
Dreadnode（德雷德节点）
本研究提出ProofJudge系统，通过智能体式LLM从五个维度评估Mathlib形式化证明质量，在218个声明数据集上验证其与人类偏好对齐度，发布开源制品支持相关研究。
2026-08-24 cs.AI cs.CL cs.LO
Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification
本文研究利用大语言模型（LLM）在多项式形式验证（PFV）中生成人类可读证明，以便后续通过推理引擎验证，并给出了交互示例与未来方向。
2025-05-29 cs.AR cs.LO cs.SC
Proving uniformity and independence by self-composition and coupling
耦合证明是一种经典的证明技术，用于建立两个概率过程的概率性质，如随机优势和马尔可夫链的快速混合。最近，耦合已被调查作为一个有用的抽象形式化推理的概率程序的关系属性，特别是建模约简为基础的密码学证明和验证差分隐私。在本文中，我们证明了概率耦合可以用于验证非关系的概率属性。具体来说，我们表明，程序逻辑pRHL-其证明是正式版本的耦合证明-可用于形式化的一致性和概率独立性。我们使用EasyCrypt证明助手正式验证我们的主要示例。
2017-04-01 cs.LO cs.PL
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in any Characteristic
本文在Lean定理证明器中形式化了任意特征域上Weierstrass椭圆曲线的非奇异点，并给出纯代数证明，证明其加法构成阿贝尔群，避免了高级代数几何或繁琐计算。
2023-05-15 cs.LO math.AC math.AG
A Logic of Interactive Proofs (Formal Theory of Knowledge Transfer)
我们提出了一个交互式证明的逻辑作为交互式计算的直观基础的框架，我们通过一个交互式的类似的Goedel-McKinsey-Tarski-Artemov定义的直观逻辑嵌入到一个经典的模态逻辑的证明，和Curry-Howard同构之间的直观证明和类型化的程序。我们的交互式证明实现了持久的认知影响，在他们的预期社区的同行评审，包括在诱导的（命题）知识，他们的证明目标的（个人）知识的证明与解释审查。也就是说，交互式证明通过在多代理分布式系统中传输某些个人知识（可知证明）来实现命题知识（可知事实）的转移。换句话说，我们作为一个社区可以拥有正式的共同知识，即如果我们的一个对等成员知道证明，那么该成员就会知道它的证明目标。最后但并非最不重要的是，我们证明了非平凡的交互式计算定义在我们的简单类型的交互式组合逻辑，但等价于非交互式计算定义的简单类型的组合逻辑。
2017-08-08 cs.CR cs.DC cs.LO
JEFL: Joint Embedding of Formal Proof Libraries
University of Innsbruck（因斯布鲁克大学）；University of Warsaw（华沙大学）
在不同的交互式证明助手库中使用的逻辑基础的异质性使得在它们之间发现相似的数学概念变得困难。在本文中，我们比较了以前提出的算法，我们的无监督嵌入方法，可以帮助我们检索类似的概念，跨库匹配的概念。我们的方法是基于Word2Vec的快速文本实现，在此之上添加了一个树遍历模块，以适应我们的数据导出管道的表示格式的算法。我们比较的可解释性，可定制性和在线服务的方法，并认为神经嵌入方法有更多的潜力被集成到一个互动的证明助手。
2021-07-21 cs.CL cs.LG cs.LO
AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
Axiomatic AI；Institut de Ciències Fotòniques (ICFO)（光子科学研究所）；Massachusetts Institute of Technology (MIT)（麻省理工学院）；Institució Catalana de Recerca i Estudis Avançats (ICREA)（加泰罗尼亚研究与高级研究所）
该研究发布了AxQM，这是物理学领域规模最大的教科书级证明综合基准，含1019个任务，用于评估自动形式化系统，所有任务保证有解且由Lean内核确定性评分。
2026-09-07 cs.AI cs.LO quant-ph
Logic of Non-Monotonic Interactive Proofs (Formal Theory of Temporary Knowledge Transfer)
我们提出了一个单调逻辑的内部化非单调或即时交互证明（LiiP）和重建现有的单调逻辑的内部化单调或持久交互证明（LiP）作为一个最小的保守扩展LiiP。即时交互式证明在其预期的同行评审者社区中产生了脆弱的认识影响，这种影响在于通过与解释评审者的证明知识对他们的证明目标的知识的短暂归纳：如果我的同行评审者知道我的证明，那么她至少会（在那一瞬间）知道它的证明目标是正确的。它们的影响是脆弱的，它们对知识的归纳也是短暂的，因为它可能只在学习证明的瞬间才存在。这就解释了将真值可以变化的陈述的证明内在化的重要可能性，与不变陈述相反，这些陈述不能有持久的证明。因此，即时交互证明通过在多个交互代理的分布式系统中传输某些个人知识（可知的非单调证明）来实现某些命题知识（可知的短暂事实）的临时转移。
2013-01-31 cs.CR cs.DC cs.LO
