{"id":765,"date":"2025-04-01T10:47:48","date_gmt":"2025-04-01T10:47:48","guid":{"rendered":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/?page_id=765"},"modified":"2025-06-12T15:29:58","modified_gmt":"2025-06-12T15:29:58","slug":"formal-methods-in-mathematical-proof","status":"publish","type":"page","link":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/","title":{"rendered":"Formal methods in Mathematical proof"},"content":{"rendered":"\n

Monday 23rd June<\/strong>, Newman Collaborative (WSFM1)<\/p>\n\n\n\n

15:10 – 16:10 Bhavik Mehta<\/strong> (Imperial)
16:10 – 17:10 Athina Thoma<\/a> (Southampton)<\/p>\n\n\n\n

Tuesday 24th June<\/strong>, Newman Collaborative (WSFM2)<\/p>\n\n\n\n

15:40 – 16:40 Chris Birkbeck<\/a> (East Anglia)
16:40 – 17:40 Ya\u00ebl Dillies<\/strong> (Stockholm)<\/p>\n\n\n\n

Wednesday 25th June<\/strong>, Newman Red (WSNT3)<\/p>\n\n\n\n

Contributed talks<\/a><\/p>\n\n\n\n

Chris Birkbeck – Formalising modular forms and sphere packings in Lean
<\/strong>I will discuss some work on formalising modular forms in Lean and how it is used in our (ongoing) formalization of Maryna Viazovska\u2019s Fields Medal-winning paper proving that no packing of unit balls in Euclidean space \"\mathbb{R}^8\" has density greater than that of the \"\mathrm{E}_8\"-lattice packing. Part of this is joint work with Sidharth Hariharan, Gareth Ma, Bhavik Mehta, Seewoo Lee and Maryna Viazovska.<\/p>\n\n\n\n

Ya\u00ebl Dillies – Why should Mathlib know about toric varieties?
<\/strong>Varieties, the basic objects of study in algebraic geometry, form a vast and complex world which is a priori difficult to grasp. Toric varieties are a special class of varieties which can be understood through combinatorial (and therefore computational) means, they are a rich source of examples of varieties and an indispensable tool for modern research in algebraic geometry and moduli spaces. Mathlib, the large library of formal mathematics built using the Lean theorem prover, now contains most of a standard undergraduate curriculum, and in particular varieties (or more generally, schemes). In this talk, I will report on the current effort to teach Mathlib about toric varieties and the lessons we learned along the way. I will also outline how to contribute to the project. Basic knowledge of algebraic geometry will increase enjoyment, but won’t be assumed. Joint work with Micha\u0142 Mruga\u0142a (ENS Lyon), Andrew Yang (ICL) and the other Toric contributors.<\/p>\n\n\n\n

Athina Thoma – Using Lean in university mathematics teaching: Insights and challenges\u00a0<\/strong>
Interactive Theorem Provers (ITPs) like Lean are being integrated into university mathematics teaching, either as compulsory or optional addition.\u00a0This talk presents educational research on how first-year undergraduates engage with Lean, drawing on analysis from their pen-and-paper proofs, activity with Lean, and their reflections. I will discuss the challenges students encounter, the learning opportunities Lean affords, and insights from lecturers who integrated Lean into an introductory proof course.<\/p>\n","protected":false},"excerpt":{"rendered":"

Monday 23rd June, Newman Collaborative (WSFM1) 15:10 – 16:10 Bhavik Mehta (Imperial)16:10 – 17:10 Athina Thoma (Southampton) Tuesday 24th June, Newman Collaborative (WSFM2) 15:40 – 16:40 Chris Birkbeck (East Anglia)16:40 – 17:40 Ya\u00ebl Dillies (Stockholm) Wednesday 25th June, Newman Red (WSNT3) Contributed talks Chris Birkbeck – Formalising modular forms and sphere packings in LeanI will […]<\/p>\n","protected":false},"author":2141,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"page-sidebar-boxed-feature-img.php","meta":{"_acf_changed":false,"footnotes":""},"categories":[],"tags":[],"acf":[],"yoast_head":"\nFormal methods in Mathematical proof - BMC-BAMC 2025<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Formal methods in Mathematical proof - BMC-BAMC 2025\" \/>\n<meta property=\"og:description\" content=\"Monday 23rd June, Newman Collaborative (WSFM1) 15:10 – 16:10 Bhavik Mehta (Imperial)16:10 – 17:10 Athina Thoma (Southampton) Tuesday 24th June, Newman Collaborative (WSFM2) 15:40 – 16:40 Chris Birkbeck (East Anglia)16:40 – 17:40 Ya\u00ebl Dillies (Stockholm) Wednesday 25th June, Newman Red (WSNT3) Contributed talks Chris Birkbeck – Formalising modular forms and sphere packings in LeanI will […]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/\" \/>\n<meta property=\"og:site_name\" content=\"BMC-BAMC 2025\" \/>\n<meta property=\"article:modified_time\" content=\"2025-06-12T15:29:58+00:00\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"2 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/\",\"url\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/\",\"name\":\"Formal methods in Mathematical proof - BMC-BAMC 2025\",\"isPartOf\":{\"@id\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/#website\"},\"datePublished\":\"2025-04-01T10:47:48+00:00\",\"dateModified\":\"2025-06-12T15:29:58+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Formal methods in Mathematical proof\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/#website\",\"url\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/\",\"name\":\"BMC-BAMC 2025\",\"description\":\"\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"en-US\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Formal methods in Mathematical proof - BMC-BAMC 2025","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/","og_locale":"en_US","og_type":"article","og_title":"Formal methods in Mathematical proof - BMC-BAMC 2025","og_description":"Monday 23rd June, Newman Collaborative (WSFM1) 15:10 – 16:10 Bhavik Mehta (Imperial)16:10 – 17:10 Athina Thoma (Southampton) Tuesday 24th June, Newman Collaborative (WSFM2) 15:40 – 16:40 Chris Birkbeck (East Anglia)16:40 – 17:40 Ya\u00ebl Dillies (Stockholm) Wednesday 25th June, Newman Red (WSNT3) Contributed talks Chris Birkbeck – Formalising modular forms and sphere packings in LeanI will […]","og_url":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/","og_site_name":"BMC-BAMC 2025","article_modified_time":"2025-06-12T15:29:58+00:00","twitter_card":"summary_large_image","twitter_misc":{"Est. reading time":"2 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/","url":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/","name":"Formal methods in Mathematical proof - BMC-BAMC 2025","isPartOf":{"@id":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/#website"},"datePublished":"2025-04-01T10:47:48+00:00","dateModified":"2025-06-12T15:29:58+00:00","breadcrumb":{"@id":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/formal-methods-in-mathematical-proof\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/"},{"@type":"ListItem","position":2,"name":"Formal methods in Mathematical proof"}]},{"@type":"WebSite","@id":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/#website","url":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/","name":"BMC-BAMC 2025","description":"","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"en-US"}]}},"jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/pages\/765"}],"collection":[{"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/users\/2141"}],"replies":[{"embeddable":true,"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/comments?post=765"}],"version-history":[{"count":8,"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/pages\/765\/revisions"}],"predecessor-version":[{"id":1441,"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/pages\/765\/revisions\/1441"}],"wp:attachment":[{"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/media?parent=765"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/categories?post=765"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/sites.exeter.ac.uk\/bmc-bamc2025\/wp-json\/wp\/v2\/tags?post=765"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}