Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture

Explore a conference talk detailing the formalization of Giles Gardam's disproof of Kaplansky's Unit Conjecture using Lean 4. Delve into the combination of deductive proving and formally verified computation, showcasing the capabilities of Lean 4 as both a programming language and proof assistant. Discover how the speakers demonstrate real-time formalization of a significant mathematical result and the seamless integration of proofs and computations. Gain insights into the current state of the art in formal verification and its practical applications in mathematical research.

[CPP'24] Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture