filmov
tv
[CPP'24] Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Показать описание
[CPP'24] Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Siddhartha Gadgil, Anand Rao Tadipatri
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.
Siddhartha Gadgil, Anand Rao Tadipatri
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.