Lean 4 formalization of infinitely many excluded minors for weakly orientable matroids and the Bland–Jensen conjecture.
combinatorics formal-verification formal-mathematics mathlib oriented-matroids lean4 ai4math matroid-theory weak-orientability excluded-minors bland-jensen-conjecture
-
Updated
Aug 14, 2026 - Lean