Proof Society Seminar

Date: 03/03/2025
Speaker: Henry Towsner (University of Pennsylvania)
Title: Proofs that Modify Proofs
Abstract:  In this talk, we outline an approach to cut-elimination for full second order arithmetic using a modified form of the Buchholz Omega-rule. The usual Buchholz Omega-rule is a rule branching over (“small”) deductions; this method works for systems around the strength of Pi11-comprehension, but breaks down approaching Pi12-comprehension.
We describe an extended sequent calculus in which the cut-elimination functions can themselves be represented by non-well-founded deductions. The Omega-rule can then be reinterpreted as a rule which takes a function as a premise. The extension to Pi12-comprehension then requires us to work with functionals—that is, functions on functions—and iterating through the finite types extends the method to full second order arithmetic. We will also briefly describe how to assign “ordinals” to non-well-founded deductions to extract an ordinal analysis from the cut-elimination algorithm.

Date: 03/02/2025
Speaker: Jeremy Avigad (Carnegie Mellon University)
Title: Verifying Proofs on Blockchain
Abstract: In cryptography, a *proof system* is a protocol between a prover and a verifier that enables the prover to convince the verifier that a claim is true. They are often probabilistic; given a source of randomness, it is often more efficient to convince the verifier only that it is very likely that the claim is true. Such proof systems now have interesting applications to blockchain technology, where they are used, among other things, to validate the execution of smart contracts. It is easy to make mistakes when implementing cryptographic protocols and designing smart contracts, and billions of dollars are lost to hacks every year. Fortunately, another proof technology can help: interactive proof assistants, which have long been used to verify hardware and software systems, can also be used to verify the correctness of cryptographic protocols. In this talk, I will describe some formal verification efforts I have carried out with colleagues at StarkWare Industries using the Lean proof assistant.. I will explain some of the ideas behind smart contracts and interactive proof assistants without assuming familiarity with either.
Slides and Recording