Formalization of diagram chasing in proof assistants

Diagram chasing is a kind of diagrammatic reasonning at the heart of many powerful tools in mathematics. Unfortunately, their usage requires a lot of tedious and technical calculations. This motivates the development of a formalized library to do diagram chasing on computer. On the other hand, proof assistants are not well suited a priori to perform diagrammatic reasonning easily. In this talk, after recalling the different notions, I will present the key points of such a library I am developing with Assia Mahboubi in Coq.

Speaker bio: Matthieu Piquerez is a postdoctoral researcher in computer science and mathematics at Nantes Université, France, in the Gallinette team (INRIA). He works on enabling the use of diagrammatic reasoning and other mathematical tools such as the commutativity of diagrams, diagram-chasing proofs, and spectral sequences, in formal proofs in the Coq proof assistant. He also works on tropical Hodge theory. He earned his PhD in 2021 from the École polytechnique, France, and his Master’s in 2017 from the École normale supérieure (ENS) Paris, France.