The Unit Conjecture
The Unit Conjecture is a fundamental and well-known question about group rings that goes back to Graham Higman and Irving Kaplansky in the mid-twentieth century. It is a part of a collection of several conjectures posed by Kaplansky - most notably the Zero-divisor conjecture and the Idempotent conjecture. These are collectively known as Kaplansky's conjectures.
The statement
Consider a field $K$ and a group $G$. In the group ring $K[G]$, the elements of the form $k \cdot g$, where $k \in K \backslash \{0\}$ and $g \in G$, are clearly invertible - with the inverse being $k^{-1} \cdot g^{-1}$. These are known as the trivial units of the group ring $K[G]$.
Furthermore, suppose now that the group $G$ is torsion-free, i.e., there are no elements of finite order other than the identity element. Then the Unit Conjecture states
The only units in the group ring $K[G]$, where $K$ is a field and $G$ is a torsion-free group, are the trivial units.
Gardam's disproof
In 2021, Giles Gardam finally settled the Unit conjecture in the negative. The proof was constructive, in the sense that Gardam provided an explicit field ($\mathbb{F}_{2$}, the finite field on two elements) and a torsion-free group (the Promislow or Hantzsche-Wendt group, denoted $P$), along with two non-trivial elements that are inverses of each other.
Formalising Gardam's disproof
A complete formal proof of Gardam's disproof would involve two broad components:
- A proof that the group $P$ is torsion-free
- A proof that the given elements multiply to one.
This is an interesting target for formalisation not only because it is an important mathematical result and is self-contained, but also because formalising this requires a blend of proofs and computation.
Siddhartha Gadgil and I recently formalised this result in Lean4, the latest release of the Lean theorem prover that is designed from the ground up as both a programming language as well as a theorem prover.
A detailed account of the formalisation is available on Siddhartha Gadgil's blog. This post will explore some of the design choices we made in our formalisation.
The group $P$
Central to Gardam's counter-example is the group $P$, a virtually Abelian group with the presentation $\langle a, b \vert a^{-1}b^{2}a = b^{-2}, b^{-1}a^{2}b = a^{-2}\rangle$. Earlier work by Promislow shows that $P$ is an example of a torsion-free group that does not satisfy the unique-product property, a purely combinatorial property of a group that is known to imply the unit conjecture for any group ring over that group.
The two components of the proof mentioned above deal with different aspects of the group $P$:
- the first is a mathematical proof, which requires a detailed analysis of the structure of $P$
- the second is a computation, which depends on algorithmic properties of $P$, such as being able to efficiently decide when two elements are equal
The group $P$ admits several descriptions - algebraic, topological, as well as combinatorial. Given our dual requirements of computing and proving, the description of $P$ that was most suitable was as a Metabelian group.