I have seen a lot of papers discussing whether various permutation classes are Wilf equivalent to each other. I wonder if we could solve such problems in general with computers.
More rigorously, let $\mathcal{L}$ be the language $$\{(S_1, S_2): \text{the permutation classes avoiding permutations in $S_i$ are Wilf Equivalent.}\}$$ This language is clearly recognizable by enumerating every permutation in the two classes. My question is whether we know anything about the decidability of this language.