A Machine-Checked Proof that Gardam's Ã_2 Lattice Does Not Have Unique Products

Abstract

Kaplansky's zero-divisor conjecture asserts that the group ring of a torsion-free group over a field has no zero divisors. It holds for every group with the unique-product property, so a counterexample can only come from a torsion-free group without unique products. In lectures in 2021, Gardam announced that the torsion-free Ã₂ lattice Γ= ⟨ a, b | a b a² b⁻¹ a² b⁻², a b³ a b⁴ a⁻¹ b ⟩ does not have unique products and presented it as a new candidate group: it has property (T), and the known methods for proving the conjecture do not apply to it. To our knowledge, no proof of the announcement has been published. We give a proof checked by the Lean 4 kernel and stated against Mathlib's UniqueProds class. The witness is an explicit pair of finite subsets with |A| = 32 and |B| = 28 in which each of the 896 products coincides with another product. For 658 products the certificate is an identity in the free group; the other 238 certificates are explicit products of conjugated relators, 970 conjugates in all, checked by free reduction. A homomorphism onto ℤ/42 shows that each pair (u,v) differs from its partner (u',v') as a pair of group elements, which is all the theorem requires. Together with a homomorphism onto the alternating group A₄ it also shows that the listed words are pairwise distinct, so the sets have exactly 32 and 28 elements. The witness and certificates come from an untrusted search program and are re-checked by Lean. The development uses only the axioms propext, Classical.choice and Quot.sound, with no sorry and no native_decide. The mathematical statement is Gardam's. To our knowledge this is the first verification in a proof assistant of a unique-product failure in a torsion-free group; torsion-freeness of Γ is taken from Gardam and is not formalized here.

Localizing the Gardam unit: the support geometry of units in F_2[P] and its non-unique-product relatives
Moe Tabei
arXiv21 Sep 2026PreprintCC BY 4.0Full textAlgebra & number theoryarXiv
A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs
Shenghao Yang, Yanyan Dong
arXiv5 Sep 2026PreprintCC BY-NC-SA 4.0Full textGeneral mathematicsarXiv
The triangular lattice minimises the planar Yukawa energy at every density and for every finite mixture of screening lengths: kernel-checked corollaries of planar universal optimality, a human proof, and an exact-potential CVODE consistency study
Xavier Callens
Zenodo (CERN European Organization for Nuclear Research)25 Oct 2026PreprintCC BY11 citedNumerical analysis & scientific computingOpenAlex
The bilayer dipolar-exciton interaction is completely monotone in r^2: kernel-checked triangular-lattice corollaries at every density and an exact-Ewald CVODE consistency study
Xavier Callens
Zenodo (CERN European Organization for Nuclear Research)25 Oct 2026PreprintCC BY9 citedMathematical physicsOpenAlex
The unique extremal threemodular lattice of rank 26, the generalized hexagon (2,8), and the tight Cayley-plane $5$-design
Gerald Höhn
arXiv19 Sep 2026PreprintarXiv licenceFull textAlgebra & number theory Combinatorics & discrete mathematicsarXiv

Cite

BibTeX RIS

BibTeX

@misc{mian2026machinechecked,
  title = {{A Machine-Checked Proof that Gardam's $\tildeA_2$ Lattice Does Not Have Unique Products}},
  author = {Ibrahim Mian and Shayaan Siddique},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.22380},
  eprint = {2609.22380},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.22380},
  note = {CC BY 4.0},
}

RIS

TY  - UNPB
TI  - A Machine-Checked Proof that Gardam's Ã_2 Lattice Does Not Have Unique Products
AU  - Ibrahim Mian
AU  - Shayaan Siddique
PY  - 2026
DA  - 2026/09/17
PB  - arXiv
DO  - 10.48550/arxiv.2609.22380
UR  - https://arxiv.org/abs/2609.22380
AB  - Kaplansky's zero-divisor conjecture asserts that the group ring of a torsion-free group over a field has no zero divisors. It holds for every group with the unique-product property, so a counterexample can only come from a torsion-free group without unique products. In lectures in 2021, Gardam announced that the torsion-free Ã_2 lattice Γ= ⟨ a, b | a b a^2 b^−1 a^2 b^−2, a b^3 a b^4 a^−1 b ⟩ does not have unique products and presented it as a new candidate group: it has property (T), and the known methods for proving the conjecture do not apply to it. To our knowledge, no proof of the announcement has been published. We give a proof checked by the Lean 4 kernel and stated against Mathlib's UniqueProds class. The witness is an explicit pair of finite subsets with |A| = 32 and |B| = 28 in which each of the 896 products coincides with another product. For 658 products the certificate is an identity in the free group; the other 238 certificates are explicit products of conjugated relators, 970 conjugates in all, checked by free reduction. A homomorphism onto ℤ/42 shows that each pair (u,v) differs from its partner (u',v') as a pair of group elements, which is all the theorem requires. Together with a homomorphism onto the alternating group A_4 it also shows that the listed words are pairwise distinct, so the sets have exactly 32 and 28 elements. The witness and certificates come from an untrusted search program and are re-checked by Lean. The development uses only the axioms propext, Classical.choice and Quot.sound, with no sorry and no native_decide. The mathematical statement is Gardam's. To our knowledge this is the first verification in a proof assistant of a unique-product failure in a torsion-free group; torsion-freeness of Γ is taken from Gardam and is not formalized here.
ER  -

A Machine-Checked Proof that Gardam's Ã₂ Lattice Does Not Have Unique Products

Abstract

Related

Cite