ICARM Research Talk: Proof and Pictures : Formalizing Braids

Braids are entangled strings in space, fixed at the endpoints, never doubling back. Mathematically, they can be abstracted as infinitely stretchable, deformable curves, and thus a topological object. There is also an elegant method of discretizing them to give an algebraic definition. Due to braids' clear physical interpretation, images and diagrams have long played a role in both topological and algebraic proofs. How can we temper the intuitive understanding granted by this visual imagery with mathematical rigor? Modern mathematical tools, such as the Lean interactive theorem prover, help us in this quest. While often viewed as mere bookkeepers, proof-verification tools can grant us opportunity and license to explore -- and visualize -- new theorems, proofs, and conjectures, all with safe, enforced boundaries on correctness and rigor.