For the past few years, I've been working on formalizing proofs in matroid theory using the Lean proof assistant. This has led me to many interesting and unexpected places. I'll …