How can I help?

Stream: Seymour

[Tristan Figueroa-Reid]

I'll try to [arbitrarily] attack some of the sorries not in Sum3, but if there something that isn't a sorry that would be nice (e.g. a particular issue), let me know! :+1:

[Martin Dvořák]

The most important (and, unfortunately, very difficult) task is to prove VectorMatroid.exists_standardRepr_isBase_isTotallyUnimodular as it is the only lemma that is missing for Matroid.Is1sumOf.isRegular and Matroid.Is2sumOf.isRegular being finished. It would be amazing if you somehow found a way to prove it as a corollary of VectorMatroid.exists_standardRepr_isBase but we are slowly coming to terms with the fact that VectorMatroid.exists_standardRepr_isBase_isTotallyUnimodular will probably require a lot of manual work, almost from scratch.

[Tristan Figueroa-Reid]

I'll see what I can do (though I should not be assigned to this like lemma1 since this is an important lemma), but I agree that reworking the proof to better suit the TU condition looks like a good idea from my initial attempts at proving this.