HEXAGONbeta

An Executable Stallings Recognizer for Finite Generating Lists in Lean

Primarily AI-generated textHuman understanding: some partsmath.GR — Group Theorymath.LO — Logic

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

We explain a Lean 4 construction of a finite inverse automaton recognizing the subgroup of the rank-two free group generated by any finite list of signed words. The implementation builds a flower multigraph and computes the least equivalence relation compatible with deterministic labelled transitions by exhaustive finite search over Boolean relations. Canonical representatives realize the folded graph on the original finite state type. A coset-potential invariant proves that folding introduces no additional subgroup elements; preservation of the input loops proves the opposite inclusion. A separate reduction argument shows that traversal of the canonical reduced representative decides membership. We distinguish the registered theorem, its executable witness, and classical reasoning used only in the proof. The construction retains unused states and has no formalized complexity, core-trimming, subgroup-basis, intersection, or index algorithm. This is an expository account of a classical recognition theorem and a pinned formal artifact, with no claim of mathematical novelty or formalization priority.

Provenance statement

The manuscript names Arthur Freitas Ramos (submitting contributor; ORCID 0009-0003-3568-0325), David Barros Hulak (0009-0002-8056-1774), and Ruy J. G. B. de Queiroz (0000-0003-1482-0977). The submitting contributor reports understanding some parts, but not all, of the work. OpenAI GPT-6.1 assisted with manuscript drafting, inspection of the pinned source, source cross-checking, exposition, bibliography, and typesetting. Historical pinned repository metadata separately reports GPT-6 Codex proof-engineering assistance. Historical Palomar verification is distinguished from the present source inspection; no fresh Lean, Comparator, or NanoDa replay was performed during manuscript preparation. The paper describes the executable exhaustive finite rank-two free-group folding recognizer and exact subgroup-membership correctness. It does not claim a complexity bound, core-trimming, subgroup-basis or rank extraction, intersection, or index algorithm. No mathematical novelty or formalization priority is claimed. Automated review is not independent human peer review.
FormalizationsPalomar

Tools used

OpenAI
ChatGPTVersion GPT 6.1 (manuscript)
OpenAI
CodexVersion GPT-6 (historical proof engineering)
Lean
LeanVersion 4.33.0 (registered artifact)

References

  1. Ilya Kapovich; Alexei Myasnikov. Stallings foldings and subgroups of free groups. Journal of Algebra, vol. 248, no. 2, pp. 608–668. 2002. DOI: \urlhttps://doi.org/10.1006/jabr.2001.9033. Preprint titled Stallings foldings and the subgroup structure of free groups, arXiv:math/0202285arXivDOI
  2. Palomar Registry. Verified finite automata for finitely generated subgroups of $F_2$. 2026. PALOMAR-2026-09-23-000004, version 1; registered September 23, 2026; accessed October 1, 2026
  3. Arthur Freitas Ramos. Verified finite automata for finitely generated subgroups of $F_2$. 2026. Immutable source commit 117dde0a8415d3da1787e15ad22a6223a744432d; accessed October 1, 2026
  4. John R. Stallings. Topology of finite graphs. Inventiones Mathematicae, vol. 71, no. 3, pp. 551–565. 1983. DOI: \urlhttps://doi.org/10.1007/BF02095993DOI
  5. The Mathlib Community. Mathlib free-group reduction library. 2026. Pinned commit db584cd6d46c92f209a44c0f1c829460d327499d; accessed October 1, 2026

Version history

  1. v1Initial depositCurrentOct 01, 2026