Written by J. David Smith Published on 27 December 2023 This year, one of my hobby projects has been implementing some basic properties and conversions between Matroids in Lean. My primary resource for doing this has been Theorem Proving in Lean 4 (TPiL), which is an incredibly detailed walk through using Lean as a proof assistant. While useful, it has...gaps—as does the main Lean documentation. A lot of this gap appears to be filled by the Zulip chat. The title of this post is a bit of a double...