ProofCloud: A Proof Retrieval Engine for Verified Proofs in Higher Order Logic

TL;DR

ProofCloud presents a fast, searchable retrieval engine for verified proofs in higher-order logic ($HOL$) and demonstrates end-to-end verification by translating and checking OpenTheory packages with $Dedukti$ via $Holide$ under an updated OpenTheory kernel. The work shows that all six OpenTheory packages can be translated and checked, providing proof of reliability for cross-prover proof sharing and reuse. The combined system enables efficient reuse of proofs, transparency of classical vs constructive arguments, and accessible proof-checking results through a web-facing interface. This advances the practical use of formal proofs across the HOL family by linking storage, retrieval, and independent verification.

Abstract

This paper introduces ProofCloud, a proof retrieval engine for verified proofs in higher order logic. It provides a fast proof searching service for mathematicians and computer scientists for the reuse of proofs and proof packages. In addition, it includes the first complete proof-checking results and benchmarks of the OpenTheory repository.

Figures (4)

• Figure 1: The Interface of ProofCloud
• Figure 2: A Proof Page of ProofCloud
• Figure 3: Dependency of Packages of OpenTheory
• Figure 4: A Proof Checking Page of ProofCloud