Document Open Access Logo

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

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

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.9.pdf
  • Filesize: 0.81 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.9.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Symbolic and algebraic manipulation
  • Theory of computation → Expander graphs and randomness extractors
  • Software and its engineering → Formal methods
Keywords
  • Group presentations
  • term rewriting
  • metaprogramming
  • proof automation
  • the Lean theorem prover

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.ITP.2025.9

Author Details

Eric Wang
  • School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA
Arohee Bhoja
  • School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA
Cayden Codel
  • School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA
Noah G. Singer
  • School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

Our research was supported by the Hoskinson Center for Formalized Mathematics, and the last author was supported by an NSF Graduate Research Fellowship (Award DGE 2140739).

Acknowledgements

We thank members of https://leanprover.zulipchat.com/ for answering our metaprogramming questions. We also thank our paper’s ITP reviewers for their thorough and helpful feedback.

Supplementary Materials

References

  1. Noga Alon. Eigenvalues and expanders. Combinatorica, 6(2):83-96, June 1986. URL: https://doi.org/10.1007/BF02579166.
  2. Michael Aschbacher. The status of the classification of the finite simple groups. Notices of the AMS, 51(7):736-740, 2004. Google Scholar
  3. Mitali Bafna, Noam Lifshitz, and Dor Minzer. Constant Degree Direct Product Testers with Small Soundness. In 65th Annual Symposium on Foundations of Computer Science (FOCS 2024), pages 862-869, Chicago, IL, USA, October 27-30, 2024, July 2024. IEEE Computer Society. URL: https://doi.org/10.1109/FOCS61266.2024.00059.
  4. Mitali Bafna and Dor Minzer. Characterizing Direct Product Testing via Coboundary Expansion. In Proceedings of the 56th Annual ACM Symposium on Theory of Computing (STOC 2024), pages 1978-1989, Vancouver, BC, Canada, June 24-28, 2024, February 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3618260.3649714.
  5. Cristina M. Ballantine. Ramanujan Type Buildings. Canadian Journal of Mathematics, 52(6):1121-1148, December 2000. URL: https://doi.org/10.4153/CJM-2000-047-4.
  6. Roger W. Carter. Simple Groups of Lie Type. Wiley, London, 1989. Google Scholar
  7. Donald I. Cartwright, Patrick Solé, and Andrzej Żuk. Ramanujan geometries of type ̃ A_n. Discrete Mathematics, 269(1-3):35-43, July 2003. URL: https://doi.org/10.1016/S0012-365X(02)00748-3.
  8. Claude Chevalley. Sur certains groupes simples. Tohoku Mathematical Journal, 7(1-2):14-66, January 1955. URL: https://doi.org/10.2748/tmj/1178245104.
  9. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In 28th International Conference on Automated Deduction, pages 625-635. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  10. Leonard Eugene Dickson. Linear Groups, with an Exposition of the Galois Field Theory. Leipzig B.G. Teubner, 1901. Google Scholar
  11. Leonard Eugene Dickson. Theory of Linear Groups in An Arbitrary Field. Transactions of the American Mathematical Society, 2(4):363-394, 1901. URL: https://doi.org/10.2307/1986251.
  12. Yotam Dikstein, Irit Dinur, and Alexander Lubotzky. Low Acceptance Agreement Tests via Bounded-Degree Symplectic HDXs. In 65th Annual Symposium on Foundations of Computer Science (FOCS 2024), pages 826-861, Chicago, IL, USA, October 27-30, 2024, October 2024. IEEE Computer Society. URL: https://doi.org/10.1109/FOCS61266.2024.00058.
  13. Irit Dinur, Shai Evra, Ron Livne, Alexander Lubotzky, and Shahar Mozes. Locally testable codes with constant rate, distance, and locality. In Proceedings of the 54th Annual ACM SIGACT Symposium on Theory of Computing (STOC 2022), pages 357-374, Rome, Italy, June 20-24, 2022, June 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3519935.3520024.
  14. Irit Dinur, Yuval Filmus, Prahladh Harsha, and Madhur Tulsiani. Explicit SoS lower bounds from high-dimensional expanders. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021), virtual, January 6-8, 2021, September 2020. URL: https://doi.org/10.4230/LIPIcs.ITCS.2021.38.
  15. Irit Dinur and Tali Kaufman. High Dimensional Expanders Imply Agreement Expanders. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS), pages 974-985, October 2017. URL: https://doi.org/10.1109/FOCS.2017.94.
  16. Dominic Dotterrer, Tali Kaufman, and Uli Wagner. On expansion and topological overlap. Geometriae Dedicata, 195(1):307-317, August 2018. Conference version in SoCG 2016. URL: https://doi.org/10.1007/s10711-017-0291-4.
  17. Shai Evra and Tali Kaufman. Bounded degree cosystolic expanders of every dimension. In Proceedings of the Forty-Eighth Annual ACM Symposium on Theory of Computing (STOC 2016), pages 36-48, Cambridge, MA, USA, June 19-21, 2016, June 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2897518.2897543.
  18. Mikhail Gromov. Singularities, Expanders and Topology of Maps. Part 2: From Combinatorics to Topology Via Algebraic Isoperimetry. Geometric and Functional Analysis, 20(2):416-526, August 2010. URL: https://doi.org/10.1007/s00039-010-0073-8.
  19. Anna Gundert and Uli Wagner. On eigenvalues of random complexes. Israel Journal of Mathematics, 216(2):545-582, October 2016. URL: https://doi.org/10.1007/s11856-016-1419-1.
  20. Shlomo Hoory, Nathan Linial, and Avi Wigderson. Expander graphs and their applications. Bulletin of the American Mathematical Society, 43(04):439-562, August 2006. URL: https://doi.org/10.1090/S0273-0979-06-01126-8.
  21. Max Hopkins and Ting-Chun Lin. Explicit Lower Bounds Against Ω(n)-Rounds of Sum-of-Squares. In 63rd Annual Symposium on Foundations of Computer Science (FOCS 2022), Denver, CO, USA, October 31-November 3, 2022, 2022. IEEE Computer Society. URL: https://doi.org/10.1109/FOCS54457.2022.00069.
  22. Camille Jordan. Traité des substitutions et des équations algébriques. Paris Gauthier-Villars, 1870. Google Scholar
  23. Tali Kaufman, David Kazhdan, and Alexander Lubotzky. Isoperimetric Inequalities for Ramanujan Complexes and Topological Expanders. Geometric and Functional Analysis, 26(1):250-287, February 2016. Conference version in FOCS 2014. URL: https://doi.org/10.1007/s00039-016-0362-y.
  24. Tali Kaufman and Izhar Oppenheim. Construction of new local spectral high dimensional expanders. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing (STOC 2018), pages 773-786, Los Angeles, CA, USA, June 25-29, 2018, June 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3188745.3188782.
  25. Tali Kaufman and Izhar Oppenheim. Coboundary and Cosystolic Expansion from Strong Symmetry. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198 of LIPIcs, pages 84:1-84:16, Glasgow, Scotland / virtual, July 12-16, 2021, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.ICALP.2021.84.
  26. Tali Kaufman, Izhar Oppenheim, and Shmuel Weinberger. Coboundary expansion of coset complexes. In 57th Annual ACM Symposium on Theory of Computing (STOC 2025), Prague, Czech Republic, June 23-27, 2025, November 2024. Association for Computing Machinery. Google Scholar
  27. Anthony Leverrier and Gilles Zémor. Quantum Tanner codes. In 63rd Annual Symposium on Foundations of Computer Science (FOCS 2022), Denver, CO, USA, October 31-November 3, 2022, April 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00117.
  28. Wen-Ching Winnie Li. Ramanujan hypergraphs. Geometric And Functional Analysis, 14(2):380-399, April 2004. URL: https://doi.org/10.1007/s00039-004-0461-z.
  29. Nathan Linial and Roy Meshulam. Homological Connectivity Of Random 2-Complexes. Combinatorica, 26(4):475-487, August 2006. URL: https://doi.org/10.1007/s00493-006-0027-9.
  30. Alexander Lubotzky, Beth Samuels, and Uzi Vishne. Explicit constructions of Ramanujan complexes of type ̃ a_d. European Journal of Combinatorics, 26(6):965-993, August 2005. URL: https://doi.org/10.1016/j.ejc.2004.06.007.
  31. Alexander Lubotzky, Beth Samuels, and Uzi Vishne. Ramanujan complexes of type ̃ a_d. Israel Journal of Mathematics, 149(1):267-299, December 2005. URL: https://doi.org/10.1007/BF02772543.
  32. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, January 2020. URL: https://doi.org/10.1145/3372885.3373824.
  33. P. S. Novikov. Algorithmic unsolvability of the word problem in group theory. Journal of Symbolic Logic, 23(1):50-52, 1958. URL: https://doi.org/10.2307/2964487.
  34. Ryan O'Donnell and Kevin Pratt. High-Dimensional Expanders from Chevalley Groups. In Shachar Lovett, editor, LIPIcs, Volume 234, CCC 2022 (37th Computational Complexity Conference), volume 234 of LIPIcs, pages 18:1-18:26, Philadelphia, PA, USA, July 20-23, 2022, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPICS.CCC.2022.18.
  35. Ryan O'Donnell and Noah G. Singer. Coboundary expansion inside Chevalley coset complex HDXs. In submission, November 2024. URL: https://doi.org/10.48550/arXiv.2411.05916.
  36. Rimhak Ree. On Some Simple Groups Defined by C. Chevalley. Transactions of the American Mathematical Society, 84(2):392-400, 1957. URL: https://doi.org/10.2307/1992821.
  37. Alireza Sarveniazi. Ramanujan Regular Hypergraphs Based on Special Affine Bruhat-Tits Buildings. PhD thesis, Göttingen University, February 2004. URL: https://doi.org/10.53846/goediss-2467.
  38. John Steenbergen, Caroline Klivans, and Sayan Mukherjee. A Cheeger-type inequality on simplicial complexes. Advances in Applied Mathematics, 56:56-77, May 2014. URL: https://doi.org/10.1016/j.aam.2014.01.002.
  39. Robert Steinberg. Variations on a theme of Chevalley. Pacific Journal of Mathematics, 9(3):875-891, January 1959. URL: https://doi.org/10.2140/pjm.1959.9.875.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact