On August 14, 2024, Peter Nelson from the University of Waterloo gave a talk at the Discrete Math Seminar on formalizing the matroid theory on LEAN at the Discrete Math Seminar. The title of his talk was “Formalizing matroid theory in a proof assistant“.