Does the purported proof of Rota's conjecture provide an algorithm for calculating the forbidden minors of matroids over arbitrary finite fields?

Question

About six years ago there was a proof announced and later outlined in a notice from AMS. However right now I can only seem to find forbidden minor characterizations for matroids linearly representable over $\mathbb{F}_2,\mathbb{F}_3,\mathbb{F}_4$ and some for $\mathbb{F}_5$. Now understanding the outline given by Geelen, Gerards, and Whittle is hard enough for me as I am not well versed in matroid theory, also a full proof hasn"t even been written yet so to go further I'd have to scour through the 20 something papers they wrote and used results from (most of which I don't even partially understand). However I'm curious as to how constructive their proof was and if it was in such a way that an algorithm can be derived from it as a collaroy allowing one to just run it over all finite fields up to some very large prime power on a super computer so we can get insight at least empirically as to what they look like.

I think this would be interesting because unlike other minor theorems for graphs like say the most famous Robertson–Seymour theorem, these give us insight to the class of graphs closed under the graph minor operation, yet this class is so large that it lacks any real 'neat structure' - its just graphs closed under minors. In contrast the class of matroids linearly representable over finite fields is much smaller then say the class of matroids closed under the matroid minor operation (also we know that an analogue of the Robertson–Seymour theorem for minors is false e.g. there exists matroids closed under minors without any finite set of forbidden minors) so id guess these adhere to some kind of general structure. Also knowing the minors of the first say 100 finite fields explicitly might give better insight into them and allow for interesting theorems to be derived from those particular matroids. For example the matroids representable over the first finite field $\mathbb{F}_2$ are called binary matroids and there are all sorts of special theorems for them e.g. an Euler theorem and factor critical theorem graph theory analogue which doesn't necessarily hold for matroids over other finite fields.

Answer 1

As far as I understand, the purported proof does not give an algorithm that given a finite field $\mathbb{F}$, computes the excluded minors for $\mathbb{F}$-representability. This is because it relies on well-quasi-ordering arguments, and therefore does not yield explicit upperbounds on the size of the excluded minors. Note that if one could prove that there exists a computable function $c: \mathbb{N} \to \mathbb{N}$ such that every excluded-minor for $\mathbb{F}$-representability has size at most $c(|\mathbb{F}|)$, then this would give a naive brute force algorithm, but it is unknown if such a computable function exists. Indeed, even for minor-closed classes of graphs, it is known that the problem of computing excluded minors is undecidable. So it may be that such a computable function $c$ does not exist.

See my other answer for more information about the undecidability results for computing the excluded minors of a minor-closed class of graphs. Finally, you might be interested in this recent post by Rutger Campbell on the Matroid Union Blog about a strategy to compute the excluded minors for the five element field.