Online talk: Peter Nelson

Monday, March 22, 3pm ET (7pm GMT, 8am Tue NZDT)
Peter Nelson, University of Waterloo
Formalizing matroids

YouTube: https://youtu.be/wMRrSWsZSFM (sorry for the delay on this/accidentally deleting the post!)
 
Abstract:

Like in many areas of mathematics, long and technical proofs in combinatorics are becoming more common. When we consider the refereeing process, the unpleasant screeds of case-analysis with which many of us are familiar, and our high standards for mathematical truth, it is natural to have uncomfortable doubts due to simple human fallibility. A potential panacea is to use proof assistants to formally verify the correctness of our theorems. I will describe efforts I have made in recent months to formalize parts of matroid theory using the lean theorem prover, and a modest few results about matroids that are now formalized, including Edmonds’ Matroid Intersection Theorem. The talk is particularly aimed towards combinatorialists that are curious about this area; I will discuss both the bigger picture as well as the day-to-day experience of using a theorem prover, assuming no prior knowledge. This is joint work with Edward Lee and Mathieu Guay-Paquet.

1 thought on “Online talk: Peter Nelson

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.