I will discuss the formalization, in Lean, of braid groups : from their definition to the ongoing implementation and verification of a polynomial-time algorithm for the braid isotopy problem (Patrick Dehornoy’s subword reversing). Braids, inherently physical objects, were first abstracted to a nascent sort of topology by Vandermonde in the 18th century, and then to a proto-algebraic structure by Gauss in the 19th. More modern authors, from Artin to Markov (Jr.) to Dehornoy, have wrestled with the notion of rigor in this setting, as the associated visual imagery can suggest intuitive leaps. I will discuss one such example, and present a novel, formalized proof, which forms part of the work for the braid isotopy problem.

Formalization is based on Dehornoy’s The Calculus of Braids, 2019 [original] / 2021 [English version]