DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2025.9

Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups

Authors: Eric Wang, Arohee Bhoja, Cayden Codel, and Noah G. Singer

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract

Graded unipotent Chevalley groups are an important family of groups on matrices with polynomial entries over a finite field. Using the Lean theorem prover, we verify that three such groups, namely, the A₃- and the two B₃-type groups, satisfy a useful group-theoretic condition. Specifically, these groups are defined by a set of equations called Steinberg relations, and we prove that a certain canonical "smaller" set of Steinberg relations suffices to derive the rest. Our work is motivated by an application for building topologically-interesting objects called higher-dimensional expanders (HDXs). In the past decade, HDXs have formed the basis for many new results in theoretical computer science, such as in quantum error correction and in property testing. Yet despite the increasing prevalence of HDXs, only two methods of constructing them are known. One such method builds an HDX from groups that satisfy the aforementioned property, and the Chevalley groups we use are (essentially) the only ones currently known to satisfy it.

Cite as

Eric Wang, Arohee Bhoja, Cayden Codel, and Noah G. Singer. Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.ITP.2025.9,
  author =	{Wang, Eric and Bhoja, Arohee and Codel, Cayden and Singer, Noah G.},
  title =	{{Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.9},
  URN =		{urn:nbn:de:0030-drops-246071},
  doi =		{10.4230/LIPIcs.ITP.2025.9},
  annote =	{Keywords: Group presentations, term rewriting, metaprogramming, proof automation, the Lean theorem prover}
}

Search Results

Documents authored by Wang, Eric

Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups

Abstract

Cite as

Thanks for your feedback!

Could not send message