12 papers
Polymorphism Meets DHOL
Rhea Ranalter, Florian Rabe, Cezary Kaliszyk
DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-b…
Munkres' General Topology Autoformalized in Isabelle/HOL
Dustin Bryant, Jonathan Julián Huerta y Munive, Cezary Kaliszyk +1
We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Ch…
Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
Chad E. Brown, Cezary Kaliszyk, Josef Urban
We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multip…
Payment Channels with Proofs
Chad E. Brown, Cezary Kaliszyk, Josef Urban
The fundamental building blocks of the Bitcoin lightning network are bidirectional payment channels. We describe an extension of payment channels in the Proofgold network which all…
Exploring Formal Math on the Blockchain: An Explorer for Proofgold
Chad E. Brown, Cezary Kaliszyk, Josef Urban
Proofgold is a blockchain that supports formalized mathematics alongside standard cryptocurrency functionality. It incorporates logical constructs into the blockchain, including de…
Hammering Higher Order Set Theory
Chad E. Brown, Cezary Kaliszyk, Martin Suda +1
We use automated theorem provers to significantly shorten a formal development in higher order set theory. The development includes many standard theorems such as the fundamental t…