{"id":3886,"date":"2021-03-18T09:05:40","date_gmt":"2021-03-18T13:05:40","guid":{"rendered":"http:\/\/matroidunion.org\/?p=3886"},"modified":"2021-03-24T20:21:59","modified_gmt":"2021-03-25T00:21:59","slug":"online-talk-peter-nelson-2","status":"publish","type":"post","link":"https:\/\/matroidunion.org\/?p=3886","title":{"rendered":"Online talk: Peter Nelson"},"content":{"rendered":"\n<p><strong>Monday, March 22,<\/strong> <strong>3pm ET<\/strong> (7pm GMT, 8am Tue NZDT)<br \/><a href=\"http:\/\/www.math.uwaterloo.ca\/~apnelson\/\"><strong>Peter Nelson<\/strong><\/a>, University of Waterloo<br \/><strong>Formalizing matroids<\/strong><\/p>\n<div>\n<div><b>YouTube: <\/b><a href=\"https:\/\/youtu.be\/wMRrSWsZSFM\">https:\/\/youtu.be\/wMRrSWsZSFM<\/a> (sorry for the delay on this\/accidentally deleting the post!)<\/div>\n<\/div>\n<h5>\u00a0<\/h5>\n<h5><b><\/b><strong>Abstract:<\/strong><\/h5>\n<p>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&#8217; 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.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Monday, March 22, 3pm ET (7pm GMT, 8am Tue NZDT)Peter Nelson, University of WaterlooFormalizing matroids YouTube: https:\/\/youtu.be\/wMRrSWsZSFM (sorry for the delay on this\/accidentally deleting the post!) \u00a0 Abstract: Like in many areas of mathematics, long and technical proofs in combinatorics &hellip; <a href=\"https:\/\/matroidunion.org\/?p=3886\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":19,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-3886","post","type-post","status-publish","format-standard","hentry","category-matroids"],"_links":{"self":[{"href":"https:\/\/matroidunion.org\/index.php?rest_route=\/wp\/v2\/posts\/3886","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/matroidunion.org\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/matroidunion.org\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/matroidunion.org\/index.php?rest_route=\/wp\/v2\/users\/19"}],"replies":[{"embeddable":true,"href":"https:\/\/matroidunion.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=3886"}],"version-history":[{"count":5,"href":"https:\/\/matroidunion.org\/index.php?rest_route=\/wp\/v2\/posts\/3886\/revisions"}],"predecessor-version":[{"id":3901,"href":"https:\/\/matroidunion.org\/index.php?rest_route=\/wp\/v2\/posts\/3886\/revisions\/3901"}],"wp:attachment":[{"href":"https:\/\/matroidunion.org\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=3886"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/matroidunion.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=3886"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/matroidunion.org\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=3886"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}