Title: Gaussian elimination in Lean

Abstract: 'The goal of the talk is to present a formal implementation of Gaussian elimination algorithm in the Lean theorem prover. While there already is a definition of matrices in Lean's mathematical library Mathlib, our approach consists in first converting a matrix in the sense of Mathlib to a list of lists, then performing Gaussian elimination on this list of lists before converting it back to a matrix in the sense of Mathlib. Since Gaussian elimination is a recursive process, a termination proof is required to implement this algorithm in Lean. A key step in the construction is to prove that the process preserves the size of the list of lists when the latter comes from a matrix.'