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

on YouTube ↗30m

" summary

Formalization in Lean 4 reproduces Giles Gardam’s counterexample to Kaplansky’s Unit Conjecture by building an explicit metabelian group P (K = Z^3, Q = (Z/2)^2), proving P is torsion free, and checking two concrete elements multiply to 1 over the field with two elements so they are a nontrivial unit. Work combines deductive proofs (associativity, torsion-freeness) with verified computation: a 64-case cocycle check, decidable equality on Z^3, free-module/group-ring construction, and native decide to confirm the inverse product equals 1.

AI-written summary · about

" chapters (6)

1. 0:00Gardam’s disproof of Kaplansky’s conjecture
2. 6:03Kaplansky’s unit conjecture
3. 13:25Formalizing the group
4. 17:39Gardam’s metabelian group
5. 22:38Non-trivial units in group ring
6. 24:21Q&A