A blueprint for the formalization of Seymour's matroid decomposition theorem
I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, P. Monticone, ArXiv (n.d.).