Papers With

← All papers
First page of Braid Groups in Lean : Formalizing Dehornoy's Subword Reversing Algorithm

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

Hannah Fechtner

math.GR Nov 6, 2026 · v1
formalization mathlib algebra
Read PDF arXiv abstract Code
TL;DR
Formalizes Artin braid groups in Lean and implements Dehornoy's subword reversing algorithm, proving its termination and correctness, building on Mathlib's Coxeter groups and Ore localization.
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.
Problem

Artin's braid groups had not been formalized in Lean or any other theorem prover. The literature only sketches the proof linking rectangular grids (a form of van Kampen diagram) to braid equivalence, which is needed to justify Dehornoy's subword reversing algorithm.

Approach

Braid groups are defined in Lean as Artin–Tits groups, adapting Mathlib's Coxeter group development, with finite and infinite variants and maps between them. The braid monoid is embedded into the braid group via Mathlib's Ore localization, which requires proving common multiples and cancellativity; cancellativity is proved using grid diagrams. A novel three-stage proof connects grids to reversing using partial grids and size metrics, with Type-valued derivations supplying well-founded termination measures. The reversing procedure is then implemented as an executable solver for the braid monoid and braid group word problems.

Results

The development gives a machine-checked Lean formalization of finite and infinite braid groups and a polynomial-time, executable subword reversing algorithm with proofs of termination and correctness. The code is available on GitHub, and the braid group definition has been submitted to Mathlib as a pull request.