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

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.