Monday, March 22, 3pm ET (7pm GMT, 8am Tue NZDT)
Peter Nelson, University of Waterloo
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.