POPL 2024 (series) / CPP 2024 (series) / CPP 2024 /
Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Mon 15 Jan 2024 16:30 - 17:00 at Kelvin Lecture - Formalizing Mathematics Chair(s): Kuen-Bang Hou (Favonia)
We describe a formalization in Lean 4 of Giles Gardam’s disproof of Kaplansky’s Unit Conjecture. This makes use of a combination of deductive proving and formally verified computation, using the nature of Lean 4 as a programming language which is also a proof assistant.
Our goal in this work, besides formalization of the specific result, is to show what is possible with the current state of the art and illustrate how it can be achieved. Specifically we illustrate \emph{real time} formalization of an important mathematical result and the \emph{seamless integration} of proofs and computations in Lean 4.
Mon 15 JanDisplayed time zone: London change
Mon 15 Jan
Displayed time zone: London change
16:00 - 17:30 | Formalizing MathematicsCPP at Kelvin Lecture Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota | ||
16:00 30mTalk | A Formalization of Complete Discrete Valuation Rings and Local Fields CPP María Inés de Frutos-Fernández Universidad Autónoma de Madrid, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio Université Jean Monnet Saint-Étienne Pre-print | ||
16:30 30mTalk | Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture CPP Siddhartha Gadgil Indian Institute of Science, Anand Rao Tadipatri Indian Institute of Science Education and Research | ||
17:00 30mTalk | Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Argumentsremote presentation CPP Joseph Eremondi University of Regina Pre-print | ||