首页/论文/2005.03089

arXiv 2005.030892020-05-05cs.LOcs.SE

Experiences from Exporting Major Proof Assistant Libraries

Michael Kohlhase, Florian Rabe

英文摘要：

The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented tremendous theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution and our experiences will prove valuable to others undertaking such efforts.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

在HOL库中匹配概念

Matching concepts across HOL libraries

许多证明助手库包含相同数学概念的形式化。这些概念通常以不同的方式引入（定义），但它们所具有的属性以及相应的形式化是相同的。对于基本概念，比如自然数，由于数学命名约定，在库之间匹配它们通常很简单。然而，对于更高级的概念，即使对于专家来说，在不同的库中找到类似的形式化也是一项重要的任务。在本文中，我们研究了自动发现的相似概念，跨图书馆的证明助手。我们提出了一种规范化的正式图书馆和一些相似性措施的概念属性的方法。我们在基于HOL的证明助手HOL 4、HOL Light和Isabelle/HOL上对该方法进行了评估，发现了398对同构常数和类型。

2014-05-15cs.LO

JEFL: Joint Embedding of Formal Proof Libraries

University of Innsbruck（因斯布鲁克大学）；University of Warsaw（华沙大学）

The heterogeneous nature of the logical foundations used in different interactive proof assistant libraries has rendered discovery of similar mathematical concepts among them difficult. In this paper, we compare a previously proposed algorithm for matching concepts across libraries with our unsupervised embedding approach that can help us retrieve similar concepts. Our approach is based on the fasttext implementation of Word2Vec, on top of which a tree traversal module is added to adapt its algorithm to the representation format of our data export pipeline. We compare the explainability, custo…

2021-07-21cs.CLcs.LGcs.LO

Constructive Analysis in the Agda Proof Assistant

Proof assistant software has recently been used to verify proofs of major theorems, yet even the libraries of some of the most prominent proof assistants lack much of undergraduate mathematics. In particular, the Agda proof assistant has no formalization of the real numbers and their arithmetic. In this thesis, I present my implementation of Errett Bishop's constructive real numbers in Agda, including their arithmetic, ordering, and fundamental results, such as uncountability and Cauchy completeness. We will also survey the basic concepts of constructive analysis and the Agda proof assistant.

2022-05-04cs.LO

Making Isabelle Content Accessible in Knowledge Representation Formats

The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult. After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of …

2020-05-05cs.LO

The Lean mathematical library

This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led us here.

2019-12-16cs.LOmath.LO

从Coq中提取Herbrand树

Extracting Herbrand trees from Coq

软件认证旨在证明程序的正确性，但在许多情况下，使用外部库只允许有条件的证明：它取决于库满足其规范的假设。特别是，这些库中的错误仍然可能影响认证程序。在这种情况下，出现的困难是隔离有缺陷的库函数并提供反例。在本文中，我们表明，这个问题可以在逻辑上形式化为一个矛盾的普遍理论的Herbrand树的建设和地址it.The解决方案，我们提出的是基于证明Herbrand定理的证明助手Coq。经典的程序提取使用Krivine的经典的可实现性，然后将此证明转换为认证的程序，计算Herbrand树。使用这个树和对库函数的调用，我们能够确定哪个函数是有缺陷的，并显式地产生一个反例来说明它。

2013-04-16cs.LO

更多相关论文收起更多论文

A formally verified proof of the Central Limit Theorem

We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle's libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. We also discuss the libraries and infrastructure that supported the formalization, and reflect on some of the lessons we have learned from the effort.

2017-02-01cs.LOcs.MSmath.PR

Alignment-based Translations Across Formal Systems Using Interface Theories

Translating expressions between different logics and theorem provers is notoriously and often prohibitively difficult, due to the large differences between the logical foundations, the implementations of the systems, and the structure of the respective libraries. Practical solutions for exchanging theorems across theorem provers have remained both weak and brittle. Consequently, libraries are not easily reusable across systems, and substantial effort must be spent on reformalizing and proving basic results in each system. Notably, this problem exists already if we only try to exchange theorem …

2017-12-05cs.LO

An Open Challenge Problem Repository for Systems Supporting Binders

A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with binders offer a very limited evaluation of such libraries, and the examples given often do not exercise and stress-test key aspects that arise in the presence of binders. In this paper we design an open repository ORBI (Open challenge problem Repository for systems supporting reasoning with BInders). We believe the field of reasoning about languages…

2015-07-29cs.LOcs.PL

Reliably Reproducing Machine-Checked Proofs with the Coq Platform

The Coq Platform is a continuously developed distribution of the Coq proof assistant together with commonly used libraries, plugins, and external tools useful in Coq-based formal verification projects. The Coq Platform enables reproducing and extending Coq artifacts in research, education, and industry, e.g., formalized mathematics and verified software systems. In this paper, we describe the background and motivation for the Platform, and outline its organization and development process. We also compare the Coq Platform to similar distributions and processes in the proof assistant community, …

2022-03-18cs.DLcs.LO

对Sigmoid函数的正式分析及通用逼近定理的正式证明

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem

本文在Isabelle/HOL中形式化分析了Sigmoid函数并证明了通用逼近定理，填补了形式化证明库的空白，提升了神经网络的可信度。

2025-12-03cs.LOcs.SE

jsCoq: Towards Hybrid Theorem Proving Interfaces

MINES ParisTech PSL Research University（巴黎高等矿业学院PSL研究大学）

We describe jsCcoq, a new platform and user environment for the Coq interactive proof assistant. The jsCoq system targets the HTML5-ECMAScript 2015 specification, and it is typically run inside a standards-compliant browser, without the need of external servers or services. Targeting educational use, jsCoq allows the user to start interaction with proof scripts right away, thanks to its self-contained nature. Indeed, a full Coq environment is packed along the proof scripts, easing distribution and installation. Starting to use jsCoq is as easy as clicking on a link. The current release ships m…

2017-01-25cs.HCcs.LGcs.LO

Proof Artifact Co-training for Theorem Proving with Language Models

University of Pittsburgh（匹兹堡大学）；OpenAI；IBM Research（IBM研究院）；Google Research（谷歌研究院）；Stanford University（斯坦福大学）；Carnegie Mellon University（卡内基梅隆大学）；CIBO Technologies（CIBO科技）；University of Toronto（多伦多大学）；University of Cambridge（剑桥大学）

Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built. This is particularly challenging when applying large Transformer language models to tactic prediction, because the scaling of performance with respect to model size is quickly disrupted in the data-scarce, easily-overfitted regime. We propose PACT ({\bf P}roof {\bf A}rtifact {\bf C}o-{\bf T}raining), a general methodology for extracting abundant self-supervised data from kernel-level proof terms fo…

2022-03-16cs.AIcs.LGcs.LO

为轻锤设计的前提选择

Premise Selection for a Lean Hammer

Carnegie Mellon University（卡内基梅隆大学）；Mistral AI

LeanHammer通过神经前提选择系统提升Lean证明助手的自动推理能力，实现端到端的通用领域验证工具。

2026-02-25cs.AIcs.LGcs.LO