Formalizing Gardam's disproof of a "Kaplansky Conjecture"

Stream: maths

[Siddhartha Gadgil]

A few months ago, Giles Gardam disproved a long-standing conjecture - often called Kaplansky's Unit conjecture. This is a very basic statement in Algebra, saying that the only units in the group ring over a field of a _torsion-free_ group are the _trivial_ ones - those of the form $a\cdot g$. Besides the simple and basic statement, what makes the question interesting is that it is one of a bunch of statements saying something is trivial for torsion-free groups (zero divisors, Whitehead groups, ...).

@Anand Rao and I have formalized this proof in lean 4 at https://github.com/siddhartha-gadgil/Polylean/tree/main/Polylean. The README in that folder gives an outline of the code. Our proof mixes proving with some computation, and part of our motivation was to use the nature of lean 4 as a theorem prover as well as a programming language with both aspects integrated.

More details will follow soon in a blog post or two. Comments and suggestions are very welcome.

[Siddhartha Gadgil]

In case anyone is interested, I have written a blog post with some details: https://siddhartha-gadgil.github.io/automating-mathematics/posts/formalizing-gardam-disproof-kaplansky-conjecture/