> Now, if they have a bound on n, or if it's possible to derive a bound from their proof, then this could eventually become a proof of the full conjecture, by computer checking all smaller n. But if it's nonconstructive, then it can't be.

Actually, if they could somehow embed the small hypergraphs into the large ones so that the coloring on the small ones is the same, they could prove it completely. I wonder why is this not the case, but I suspect they are gonna do it, see:

“There is still the assumption in the paper that the number of nodes must be very large, but that’s probably just some additional work,” said Lovász. “Essentially, the conjecture is now proved.”