Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit Conjecture
Siddhartha Gadgil, Anand Rao Tadipatri · 2024
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.