If you know more than you let on, can you summarize the positions of the Platonists versus the Formalists versus the Constructivists? And can you explain how th

If you know more than you let on, can you summarize the positions of the Platonists versus the Formalists versus the Constructivists? And can you explain how the word "exists" means very different things in each of those schools of mathematical philosophy? Skipping on... My point is substantively different from Chaitin's constant. Chaitin's constant is unknowable because it is built off of an infinite series of answers to the halting problem. Which we can't solve. It's no surprise that a construction which starts with something we can't do, could result in a number that we can't determine. What I'm talking about is a theorem that says that a certain completely finite thing must exist. But in general we have no way to find that thing, no way to put an upper bound on its size, and no way to verify that we were correctly given it if someone gave it to us. And I'm asking in what sense we can really say that this finite thing exists. Now to the specific example. A graph is just a list of vertices, and a list of connecting edges between them. A graph is called planar if you can draw it in the plane without any edges crossing each other. Obviously if a graph is planar, it remains planar if you delete a vertex, delete and edge, or merge two vertices together that were connected by an edge. Those are the graph minor operations, and so we say that the set of planar graphs are closed under the graph minor operation. Now as it happens, there are two important non-planar graphs. One has 5 vertices, all connected to each other. That's K5. The other is two groups of 3 vertices, all vertices in the first group connected to the second. That's K3,3. Every other graph that is non-planar will contain one of those two as a minor. Planar graphs are not the only class of graphs closed under graph minors. Toroidal graphs, graphs you can draw on a torus, are also. As well as many other more exotic classes of graphs. The Robinson-Seymour says that each such class has a finite set of forbidden minors. Just like K5 and K3,3 for planar graphs. But that set may be much larger. At last count, we have 17,523 forbidden minors for toroidal graphs. We don't know how many more there may be. We don't know if we have the full list. And we don't even know if the answers are provable in ZFC. They may not be. So my question is this. We have proven the unique existence of a finite thing. But as far as we know, it is impossible for us to say anything useful about it other than that it exists, it is finite, and here are a bunch of things that are in it. In what sense does it really exist?