Formalization of Gardam's disproof of Kaplansky's conjecture

[Siddhartha Gadgil]

Dear All,

          About an year ago Giles Gardam (then a postdoc in Germany) disproved "Kaplansky's Unit Conjecture". Recently Anand Rao Tadipatri (student from IISER, Pune) and I formalised this in lean 4. Here is a blog post with some details: https://siddhartha-gadgil.github.io/automating-mathematics/posts/formalizing-gardam-disproof-kaplansky-conjecture/, 

regards,

Siddhartha