alphaFeedback

WorksMathematics

Braid Groups in Lean : Formalizing Dehornoy's Subword Reversing Algorithm

AI contributions
  • GitHub Copilot
  • Claude Opus 5.5
  • ChatGPT 5
View details
Ancillary data
1 code link
View

Abstract

We formalize the group-theoretic definition of infinite and finite Artin braid groups in Lean. We implement a polynomial-time procedure for determining equivalence in the braid group known as Dehornoy's subword reversing algorithm. Termination and correctness of this algorithm are shown using rectangular grids, which are a specific form of van Kampen diagram. The literature only hints at a proof linking rectangular grids to braid equivalence. We present a novel, three-stage proof of this result, introducing partial grids and associated size metrics.

Introduction

We begin by defining the basic objects of study, including the algebraic definition of braids, the Lean theorem prover, and the subword reversing algorithm. At the end of this chapter, we give an overview of the entire project.

Mathematical Braids

Braids were given their first full definition and exposition as a mathematical object by Emil Artin in 1925 [2]. He gave both a topological and algebraic definition of these physical objects. A physical braid is a set of strings in three-dimensional space, affixed at top and bottom to the “floor” and “ceiling.” These strings can be twisted together or crossed, but must always flow downwards. No doubling-back is allowed. This is the sort of image to keep in mind:

A physical braid

Figure 6.

The topological definition lies outside the scope of this project. We work solely with Artin’s algebraic definition, occasionally using images of the corresponding physical objects to aid in exposition.

Definition 1.1 (Presented Group). Consider a set SS and a binary relation RR on elements of the free group over SS, FSF_S. The presented group ⟨S∣R⟩\langle S \mid R\rangle is the quotient of FSF_S by the congruence generated over RR (the reflexive, symmetric, transitive, multiplicative closure of RR).

Definition 1.2. Artin’s braid group on nn strands is given by the presentation

Bn:=⟨σ1,…,σn−1∣σiσj=σjσifor ∣i−j∣≥2,σiσjσi=σjσiσjfor ∣i−j∣=1⟩B_n := \left\langle\sigma_1,\ldots,\sigma_{n-1} \mathrel{\left| \begin{aligned} \sigma_i\sigma_j &= \sigma_j\sigma_i && \text{for } |i-j| \ge2,\\ \sigma_i\sigma_j\sigma_i &= \sigma_j\sigma_i\sigma_j && \text{for } |i-j| = 1 \end{aligned}\right.}\right\rangle

The infinite braid group B∞B_\infty can be defined as the direct limit B∞:=⋃n∈NBnB_\infty:= \bigcup_{n\in\mathbb{N}} B_n or equivalently by the presentation

B∞:=⟨σ1,σ2,σ3…σiσj=σjσifor ∣i−j∣≥2,σiσjσi=σjσiσjfor ∣i−j∣=1⟩B_{\infty} := \left\langle\begin{array}{c|c} \sigma_1,\sigma_2,\sigma_3\ldots& \begin{aligned} \sigma_i\sigma_j&=\sigma_j\sigma_i && \text{for } |i-j|\ge2,\\ \sigma_i\sigma_j\sigma_i&=\sigma_j\sigma_i\sigma_j && \text{for } |i-j|=1 \end{aligned} \end{array} \right\rangle

The generator σi\sigma_i represents the strand in position ii (1≤i<n1\le i<n) crossing over the strand to its right.

A braid crossing with the left strand crossing over the right strand

Figure 7 (PDF p. 4).

σi−1\sigma_i^{-1} represents the strand in position ii crossing under the strand to its right.

A braid crossing with the left strand crossing under the right strand

Figure 8.

For example, the braid at the opening of this chapter is coded σ1−1σ3σ2−1σ1σ2−1σ1σ3σ2\sigma_1^{-1}\sigma_3\sigma_2^{-1}\sigma_1\sigma_2^{-1}\sigma_1\sigma_3\sigma_2.

The physical representation shows how inverses untangle: here is σi−1σi\sigma_i^{-1}\sigma_i:

A braid and its inverse

Figure 9.

is equivalent to

Two parallel strands

Figure 10.

The defining relations of the braid group can be visualized as follows:

Crossings far apart can be slid up and down (if ∣i−j∣≥2|i-j|\ge2, σiσj\sigma_i\sigma_j is equivalent to σjσi\sigma_j\sigma_i):

Two braid diagrams with crossings far apart

Figure 11.

is equivalent to

Two braid diagrams with crossings far apart in the opposite order

Figure 12.

An adjacent strand can be pulled through a crossing (σiσi+1σi\sigma_i\sigma_{i+1}\sigma_i is equivalent to σi+1σiσi+1\sigma_{i+1}\sigma_i\sigma_{i+1}):

Three-strand braid diagram

Figure 13.

is equivalent to

Three-strand braid diagram with the crossing rearranged

Figure 14.

Of course, to rigorously show that these relations are sufficient to capture equivalence in the physical objects, one must give a topological definition and the proof that the algebraic and topological definitions coincide. The interested reader can find a modern exposition in Patrick Dehornoy’s textbook “The Calculus of Braids”, chapters one and two [16].

The Lean Theorem Prover

Lean is a functional programming language and interactive theorem prover based on dependent type theory. Leonardo de Moura launched Lean in 2013; the language is now on version 4 [8]. Mathematicians worldwide use Lean to formally verify proofs across mathematics, from undergraduate basics to the cutting edge of research. In Lean, one can implement algorithms and execute them using the #eval command along with stating and proving theorems about their properties, all in the same file. While algorithms of course must be computable in order to evaluate, Lean is not limited to computable functions or constructive proofs. One can choose to use Lean with constructive or classical logic. When proving correctness of an algorithm, for example, the algorithm must be computable but the proofs of correctness and termination need not be.

A large collaborative project to formalize mathematics in one central repository, named Mathlib, is ongoing, and currently counts 772 contributors [34].1 As far as we can tell, there has been no formalization of Artin’s braid group in Mathlib or elsewhere in Lean, nor in any other theorem prover. Coxeter groups, another type of presented group which is similar in structure to the braid groups, have recently been formalized in Lean.2 There has been work in formalized category theory which could be related to braid groups [33, 31, 6], including basic definitions in Lean3, but the major required theorem4 is not yet formalized, and the word problem in such categorical structures is as hard as that of the unknot problem [19], compared to polynomial-time complexity for braid groups [13]. Thus, a connection to category theory does not simplify the project, and lies beyond the scope of this paper. Knots and a few invariants thereof were formalized in Isabelle/HOL by Prathamesh in 2015 [32]. However, the mathematics used to study braids (presented groups, localizations, orderings) differs from that used for knots (polynomial invariants). There are also a number of computational packages for working with braids, for example in MATLAB [35], SAGE5, and GAP [29]. Lastly, two theorems about braid groups (unrelated to this project) recently appeared on Prove2Me,6 an AI-based website where users employ their agents to solve mathematical “missions” proposed by humans. Upon a brief perusal, we were unable to find the Lean code on the Prove2Me site, and so are unsure of what definition of the braid groups was used.7

As to the formalization of a word problem decision procedure, existing similar work is limited. A recent paper on decidability in presented monoids does offer a (slow) Rocq algorithm (homog_dec) which can be used for any presented monoid whose relations preserve length [7]. This could be applied to determine equivalence in braid monoids but cannot be extended to braid groups.

Word Problem Algorithm

The word problem in a group is to determine whether two representatives represent the same equivalence class. In general, the word problem of a presented group is unsolvable [5, 30]. For the braid group in particular, this problem is solvable in polynomial time. A large number of algorithms exist, in part prompted by the early-2000s hope that braid group problems could be used for post-quantum security protocols [27, 10]. Early algorithms with exponential complexity included Artin combing [1] and Garside’s method of universal denominators [21], although both methods have subsequently received updates which run in polynomial time [22, 36]. A more modern solution by Birman, Ko, and Lee introduced an alternative presentation of the braid group, yielding a normal form with computational advantages [4]. Other methods such as Dynnikov coordinates [20, 13] and the Lawrence-Krammer representation [26, 3] give exceptionally simple algorithms which work quite efficiently, but the proofs of correctness involve advanced topology. Dehornoy’s most recent algorithm is handle reduction, which is experimentally quite fast (but there is no proof of polynomial-time complexity) [13].

For this project, we have implemented Dehornoy’s earlier method: subword reversing (as introduced in a journal article [12] and elucidated in his textbook [16]). While this may not be the fastest method, it runs in quadratic time, relies on a manageable amount of theory, and could be generalized to larger classes of groups [15]. Moreover, this solution builds infrastructure that could be reused in a future implementation of other algorithms, such as handle reduction.

The primary contribution lies in the treatment of this algorithm’s termination. Dehornoy wrote about this algorithm over a period of approximately twenty-five years. Most of Dehornoy’s work presents a compelling sketch of why subword reversing terminates via associating rectangular grid diagrams to individual instances of reversing, but does not give a proof for this method. Bridging this gap required the development of a new proof of termination, done in three stages. It does appear that in one of Dehornoy’s earliest papers he gives a different proof which may be fully rigorous as written. This proof is quite delicate (we will discuss this further in Chapter § 6). It seems that Dehornoy preferred the visual intuition and simplicity of the grid-based method, so we are pleased to have been able to fill in this method.

The heart of the algorithm is a reversing procedure on braid words. To underscore that we are working with words and not braid group elements, we use σˉi\bar{\sigma}_i in place of σi−1\sigma_i^{-1}. The reversing procedure consists of repeatedly rewriting negative-positive pairs σˉiσj\bar{\sigma}_i\sigma_j as follows:

If ∣i−j∣=0|i-j|=0, σˉiσi\bar{\sigma}_i\sigma_i is deleted (more precisely, replaced by the empty word ε\varepsilon).

If ∣i−j∣>1|i-j|>1, σˉiσj\bar{\sigma}_i\sigma_j is replaced by σjσˉi\sigma_j\bar{\sigma}_i.

If ∣i−j∣=1|i-j|=1, σˉiσj\bar{\sigma}_i\sigma_j is replaced by σjσiσˉjσˉi\sigma_j\sigma_i\bar{\sigma}_j\bar{\sigma}_i.

Note that these rewritings preserve equivalence under the braid relations. The proofs are straightforward algebraic manipulations; here is an instance of the third case, with numerical indices for readability:

σˉ2σ3≡σˉ2σ3σ2σˉ2(as ε≡σ2σˉ2)≡σˉ2σ3σ2σ3σˉ3σˉ2(as ε≡σ3σˉ3)≡σˉ2σ2σˉ3σ2σ3σˉ2(as σ3σ2σ3≡σ2σ3σ2)≡σ3σ2σˉ3σˉ2(as σˉ2σ2≡ε)\begin{aligned} \bar{\sigma}_2\sigma_3 &\equiv\bar{\sigma}_2\sigma_3\sigma_2\bar{\sigma}_2 && \text{(as }\varepsilon\equiv\sigma_2\bar{\sigma}_2\text{)}\\ &\equiv\bar{\sigma}_2\sigma_3\sigma_2\sigma_3\bar{\sigma}_3\bar{\sigma}_2 && \text{(as }\varepsilon\equiv\sigma_3\bar{\sigma}_3\text{)}\\ &\equiv\bar{\sigma}_2\sigma_2\bar{\sigma}_3\sigma_2\sigma_3\bar{\sigma}_2 && \text{(as }\sigma_3\sigma_2\sigma_3\equiv\sigma_2\sigma_3\sigma_2\text{)}\\ &\equiv\sigma_3\sigma_2\bar{\sigma}_3\bar{\sigma}_2 && \text{(as }\bar{\sigma}_2\sigma_2\equiv\varepsilon\text{)} \end{aligned}

Now, let us show reversing in action. We begin with σ‾1σ0σ‾2σ1\overline{\sigma}_1\sigma_0\overline{\sigma}_2\sigma_1; here is the sequence of rewritings:

References

  1. [1]E. Artin. “Theory of Braids”. en. In: The Annals of Mathematics 48.1 (Jan. 1947), p. 101. ISSN: 0003486X. DOI: 10.2307/1969218. URL: https://www.jstor.org/stable/1969218?origin=crossref.DOI
  2. [2]Emil Artin. “Theorie der Zöpfe”. de. In: Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg 4.1 (Dec. 1925), pp. 47–72. ISSN: 1865-8784. DOI: 10.1007/BF02950718. URL: https://doi.org/10.1007/BF02950718.
  3. [3]Stephen Bigelow. “Braid groups are linear”. en. In: Journal of the American Mathematical Society 14.2 (Dec. 2000), pp. 471–486. ISSN: 1088-6834, 0894-0347. DOI: 10.1090/S0894-0347-00-00361-1. URL: https://www.ams.org/jams/2001-14-02/S0894-0347-00-00361-1/.DOI
  4. [4]Joan Birman, Ki Hyoung Ko, and Sang Jin Lee. “A New Approach to the Word and Conjugacy Problems in the Braid Groups”. en. In: Advances in Mathematics 139.2 (Nov. 1998), pp. 322–353. ISSN: 00018708. DOI: 10.1006/aima.1998.1761. URL: https://linkinghub.elsevier.com/retrieve/pii/S0001870898917613.DOI
  5. [5]William W. Boone. “The Word Problem”. In: The Annals of Mathematics 70.2 (Sept. 1959), p. 207. ISSN: 0003486X. DOI: 10.2307/1970103. URL: https://www.jstor.org/stable/1970103?origin=crossref.DOI
  6. [6]Robin Carlier. Unbiasing symmetric monoidal categories in Lean. Version Number: 1. 2026. DOI: 10.48550/ARXIV.2603.00896. URL: https://arxiv.org/abs/2603.00896.
  7. [7]Reinis Cirpons et al. “Certifying the Decidability of the Word Problem in Monoids at Large”. en. In: Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs. Rennes France: ACM, Jan. 2026, pp. 128–142. ISBN: 979-8-4007-2341-4. DOI: 10.1145/3779031.3779101. URL: https://dl.acm.org/doi/10.1145/3779031.3779101.DOI
  8. [8]Leonardo De Moura and Sebastian Ullrich. “The Lean 4 Theorem Prover and Programming Language”. en. In: Automated Deduction – CADE 28. Ed. by André Platzer and Geoff Sutcliffe. Vol. 12699. Series Title: Lecture Notes in Computer Science. Cham: Springer International Publishing, 2021, pp. 625–635. ISBN: 978-3-030-79875-8 978-3-030-79876-5. DOI: 10.1007/978-3-030-79876-5_37. URL: https://link.springer.com/10.1007/978-3-030-79876-5_37.DOI
  9. [9]Patrick Dehornoy. A cancellativity criterion for presented monoids. arXiv:1802.04607. Sept. 2018. URL: http://arxiv.org/abs/1802.04607.
  10. [10]Patrick Dehornoy. “Braid-based cryptography”. en. In: Contemporary Mathematics. Ed. by Alexei G. Myasnikov and Vladimir Shpilrain. Vol. 360. Providence, Rhode Island: American Mathematical Society, 2004, pp. 5–33. ISBN: 978-0-8218-3444-2 978-0-8218-5695-6 978-0-8218-7950-4. DOI: 10.1090/conm/360/06566. URL: https://www.ams.org/conm/2004/360/06566.DOI
  11. [11]Patrick Dehornoy. “Complete positive group presentations”. en. In: Journal of Algebra 268.1 (Oct. 2003), pp. 156–197. ISSN: 00218693. DOI: 10.1016/S0021-8693(03)00326-0. URL: https://linkinghub.elsevier.com/retrieve/pii/S0021869303003260.DOI
  12. [12]Patrick Dehornoy. “Deux propriétés des groupes de tresses”. In: Comptes rendus de l’Académie des sciences. 1st ser. 315.6 (1992), pp. 633–638.
  13. [13]Patrick Dehornoy. “Efficient solutions to the braid isotopy problem”. en. In: Discrete Applied Mathematics 156.16 (Sept. 2008), pp. 3091–3112. ISSN: 0166218X. DOI: 10.1016/j.dam.2007.12.009. URL: https://linkinghub.elsevier.com/retrieve/pii/S0166218X080000437.DOI
  14. [14]Patrick Dehornoy. “On completeness of word reversing”. en. In: Discrete Mathematics 225.1-3 (Oct. 2000), pp. 93–119. ISSN: 0012365X. DOI: 10.1016/S0012-365X(00)00149–7. URL: https://linkinghub.elsevier.com/retrieve/pii/S0012365X00001497.DOI
  15. [15]Patrick Dehornoy. “The Subword Reversing Method”. en. In: International Journal of Algebra and Computation 21.01n02 (Feb. 2011), pp. 71–118. ISSN: 0218-1967, 1793-6500. DOI: 10.1142/S0218196711006091. URL: https://www.worldscientific.com/doi/abs/10.1142/S0218196711006091.DOI
  16. [16]Patrick Dehornoy, Danièle Gibbons, and Greg Gibbons. The Calculus of Braids: an introduction, and beyond. London Mathematical Society student texts 100. Cambridge ; New York, NY: Cambridge University Press, 2022. ISBN: 978-1-108-84394-2.
  17. [17]Patrick Dehornoy and Emilie Tesson. “Garside combinatorics for Thompson’s monoid F+ and a hybrid with the braid monoid B∞+”. In: Algebraic Combinatorics 2.4 (2019), pp. 683–709. DOI: 10.5802/alco.52.DOI
  18. [18]Patrick Dehornoy and Bert Wiest. “On Word Reversing in Braid Groups”. en. In: International Journal of Algebra and Computation 16.05 (Oct. 2006), pp. 941–957. ISSN: 0218-1967, 1793-6500. DOI: 10.1142/S021819670600327X. URL: https://www.worldscientific.com/doi/abs/10.1142/S021819670600327X.DOI
  19. [19]Antonin Delpeuch and Jamie Vicary. “The Word Problem for Braided Monoïdal Categories is Unknot-Hard”. en. In: Electronic Proceedings in Theoretical Computer Science 372 (Nov. 2022), pp. 72–87. ISSN: 2075-2180. DOI: 10.4204/EPTCS.372.6. URL: http://arxiv.org/abs/2105.04237v2.
  20. [20]I. A. Dynnikov. “On a Yang-Baxter map and the Dehornoy ordering”. In: Russian Mathematical Surveys 57.3 (June 2002), pp. 592–594. ISSN: 0036-0279, 1468-4829. DOI: 10.1070/RM2002v057n03ABEH000519. URL: https://www.mathnet.ru/eng/rm519.DOI
  21. [21]F. A. Garside. “The Braid Group and Other Groups”. en. In: The Quarterly Journal of Mathematics 20.1 (1969), pp. 235–254. ISSN: 0033-5606, 1464-3847. DOI: 10.1093/qmath/20.1.235. URL: https://academic.oup.com/qjmath/article-lookup/doi/10.1093/qmath/20.1.235.DOI
  22. [22]Juan González-Meneses and Marithania Silvero. “Polynomial braid combing”. en. In: Mathematics of Computation 88.318 (Nov. 2018), pp. 2027–2045. ISSN: 1088-6842, 0025-5718. DOI: 10.1090/mcom/3392. URL: https://www.ams.org/mcom/2019-88-318/S0025-5718-2018-03392-0/.
  23. [23]Nathan Hurtig et al. “Polynomial-Time Program Equivalence for Machine Knitting”. en. In: Proceedings of the ACM on Programming Languages 9.ICFP (Aug. 2025), pp. 371–399. ISSN: 2475-1421. DOI: 10.1145/3747517. URL: https://dl.acm.org/doi/10.1145/3747517.DOI
  24. [24]A. Joyal and R. Street. “Braided Tensor Categories”. en. In: Advances in Mathematics 102.1 (Nov. 1993), pp. 20–78. ISSN: 00018708. DOI: 10.1006/aima.1993.1055. URL: https://linkinghub.elsevier.com/retrieve/pii/S0001870883710558.DOI
  25. [25]Egbert R. van Kampen. “On Some Lemmas in the Theory of Groups”. In: American Journal of Mathematics 55.1/4 (1933), p. 268. ISSN: 00029327. DOI: 10.2307/2371129. URL: https://www.jstor.org/stable/2371129?origin=crossref.DOI
  26. [26]Daan Krammer. “Braid Groups are Linear”. In: The Annals of Mathematics 155.1 (Jan. 2002), p. 131. ISSN: 0003486X. DOI: 10.2307/3062152. URL: https://www.jstor.org/stable/3062152?origin=crossref.DOI
  27. [27]Eonkyung Lee. “Braid Groups in Cryptology”. In: IEICE TRANSACTIONS on Fundamentals E87-A.5 (2004), pp. 986–992.
  28. [28]Roger C. Lyndon and Paul E. Schupp. Combinatorial Group Theory. eng. Classics in Mathematics 89. Berlin, Heidelberg: Springer Berlin Heidelberg, 2001. ISBN: 978-3-540-41158-1 978-3-642-61896-3. DOI: 10.1007/978-3-642-61896-3.DOI
  29. [29]Jean Michel. The development version of the CHEVIE package of GAP3. arXiv:1310.7905 [math]. Oct. 2013. DOI: 10.48550/arXiv.1310.7905. URL: http://arxiv.org/abs/1310.7905.
  30. [30]Pyotr Sergeyevich Novikov. “On the Algorithmic Unsolvability of the Word Problem in Group Theory”. In: Trudy Matematicheskogo Instituta imeni V. A. Steklova 44 (1955).
  31. [31]Damien Pous. “String Diagrams for Monoidal Categories, in Rocq”. en. In: LIPICs, Volume 382, ITP 2026 382 (2026). Ed. by Ekaterina Komendantskaya and Tobias Nipkow. Artwork Size: 20 pages, 810898 bytes ISBN: 9783959774369 Medium: application/pdf, 28:1–28:20. ISSN: 1868-8969. DOI: 10.4230/LIPICs.ITP.2026.28. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPICs.ITP.2026.28.DOI
  32. [32]T. V. H. Prathamesh. “Formalising Knot Theory in Isabelle/HOL”. In: Interactive Theorem Proving. Ed. by Christian Urban and Xingyuan Zhang. Cham: Springer International Publishing, 2015, pp. 438–452. ISBN: 978-3-319-22102-1. DOI: 10.1007/978-3-319-22102-1_29.DOI
  33. [33]Bhakti Shah et al. ViCARe: Visualizing Categories with Automated Rewriting in Coq. Version Number: 2. 2024. DOI: 10.48550/ARXIV.2404.08163. URL: https://arxiv.org/abs/2404.08163.
  34. [34]The Mathlib Community. “The lean mathematical library”. en. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. New Orleans LA USA: ACM, Jan. 2020, pp. 367–381. ISBN: 978-1-4503-7097-4. DOI: 10.1145/3372885.3373824. URL: https://dl.acm.org/doi/10.1145/3372885.3373824.DOI
  35. [35]Jean-Luc Thiffeault and Marko Budisic. Braidlab: A Software Package for Braids and Loops. arXiv:1410.0849 [math]. Nov. 2019. DOI: 10.48550/arXiv.1410.0849. URL: http://arxiv.org/abs/1410.0849.
  36. [36]William Thurston. “Braid Groups”. In: Word processing in groups. Boston: Jones and Bartlett Publishers, 1992. ISBN: 978-0-86720-244-1.
  37. [37]Nicholas Touikan. van Kampen diagrams and the geometry of the word problem. Sept. 2024. URL: https://ntouikan.ext.unb.ca/MATH6022/IntroCGGT/html_output/section-14.html.

Paper details

vlnc:W_9zrazn8u
v1 · latestHistory (1)

published · Fresh — added to the Hub within the last 30 days

added ·

Usage

views · 2

downloads · 0

A view counts once per browser per day, a download each time the PDF is requested.

CC BY 4.0

Original source

  • Mathematics

GitHub Copilot, Claude Opus 5.5, ChatGPT 5 · View statement →

Looking for related papers…
Contents