4 papers
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…
Learning Conjecturing from Scratch
Thibault Gauthier, Josef Urban
We develop a self-learning approach for conjecturing of induction predicates on a dataset of 16197 problems derived from the OEIS. These problems are hard for today's SMT and ATP s…