Do nonconstructive proofs of isomorphism exist? I'm interested in proofs of claims of the form "Finite objects $A$ and $B$ are isomorphic" which are nonconstructive, in the sense that the proof doesn't exhibit the actual isomorphism at hand.
A stronger (and more precisely specified) requirement would be a case in which it's computationally easy to write a proof, but computationally hard to extract the isomorphism given the proof, e.g. a class of graphs for which one can easily generate triples $(G,H,P)$ with $P$ a proof that $G$ and $H$ are isomorphic but for which there's no (known) efficient algorithm to take in $(G,H,P)$ and return a permutation of the vertices exhibiting the isomorphism.
Some examples of things that would fit the bill, were they to exist:

*

*(give a nonconstructive proof that) all objects of type $X$ are uniquely specified by their values on five specific measurements; observe that $A$ and $B$ align on all such measurements.


*The easy-to-compute function of graphs $f(G,H)$ turns out to be equal to the product, over all relabelings of $G$, of the number of edges in the symmetric differences between the edge sets of $H$ and the relabeled copy of $G$. (This occurs because of some cute algebraic cancellation or something, like how one can compute determinants in time $O(n^3)$.) Now we observe that $f(G,H) = 0$ via direct computation, and conclude that a relabeling with no difference at all to $H$ must exist.


*Groups $G$ and $H$ of order $n$, specified by their multiplication tables, can be easily shown to embed as subgroups of a larger group $K$, which we can classify and more easily prove things about. But the existence of two non-isomorphic subgroups of order $n$ in $K$ would imply something about its Sylow subgroups that we know to be false.
Are there good examples of this phenomenon? Reasons to think it doesn't happen? I would also be interested in any pointers to literature on related topics here.
 A: A particular example:
$\mathbb{P}$ : Set of all primes
$\mathbb{N}$ : Set of all positive interger.
$\mathbb{P}\subset \mathbb{N}$ and $\mathbb{P}$ is an infinite set $[$ a list of proofs$]$
Any infinite subset of $\mathbb{N}$ has the cardinality $|\mathbb{N}|=\aleph_0$.
Hence there is a bijection between $\mathbb{P}$ and $\mathbb{N}$.
But it's difficult to construct such bijection.
A: The simplest example I know: the existence of primitive roots tells us that if $p$ is a prime then the group $(\mathbb{Z}/p\mathbb{Z})^{\times}$ of units $\bmod p$ is cyclic, hence isomorphic to $C_{p-1}$. However, exhibiting such an isomorphism amounts to finding such a primitive root, and the proof does not do this, nor does it really supply an efficient algorithm to do it.
I don't know what the time complexity of finding a primitive root is. The "obvious" probabilistic algorithm is to factor $p - 1$, then pick a random $a \in (\mathbb{Z}/p\mathbb{Z})^{\times}$ and test whether it's a primitive root by computing $a^{\frac{p-1}{q}} \bmod p$ for all prime divisors $q$ of $p-1$. This should be pretty fast in practice although it will take at least as long as factoring $p - 1$ and I don't know what the deterministic time complexity is.
A: Here's a charmingly ugly example. Suppose $X$,$Y$, and $Z$ are simply-connected CW-complexes. Suppose each has the same homology groups as the others:
$H_0(X; \mathbb{Z}) \cong H_0(Y; \mathbb{Z}) \cong H_0(Z; \mathbb{Z}) \cong \mathbb{Z}$
$H_3(X; \mathbb{Z}) \cong H_3(Y; \mathbb{Z}) \cong H_3(Z; \mathbb{Z}) \cong \mathbb{Z}$
$H_5(X; \mathbb{Z}) \cong H_5(Y; \mathbb{Z}) \cong H_5(Z; \mathbb{Z}) \cong \mathbb{Z}$
$H_n(X; \mathbb{Z}) \cong H_n(Y; \mathbb{Z}) \cong H_n(Z; \mathbb{Z}) \cong 0$ for all $n\neq 0,3,5$.
Then at least two of the spaces $X$, $Y$, and $Z$ are homotopy-equivalent to one another. How do you know that? It's because the assumptions imply that the homotopy types of each of $X$, $Y$, and $Z$ have minimal CW-decompositions with:
a single basepoint 0-cell,
a single 3-cell, so each of $X$, $Y$, and $Z$ have 3-skeleton $S^3$,
and a single 5-cell, so the homotopy type is determined by the homotopy class of the attaching map of the 5-cell to the 3-skeleton.
But the boundary of a 5-cell is $S^4$. So the possible homotopy types of $X$, $Y$, and $Z$ are the homotopy classes of maps $S^4 \rightarrow S^3$, i.e., the fourth homotopy group of the three-sphere, $\pi_4(S^3)$.
A quick calculation yields that $\pi_4(S^3) \cong \mathbb{Z}/2\mathbb{Z}$. So there's only two homotopy-types of spaces of the kind that $X,Y$, and $Z$ are assumed to be. So at least two of the three have to be homotopy-equivalent to one another. But it's non-constructive: the information given isn't enough to pin down which two are homotopy-equivalent. So you get non-constructive isomorphism in the homotopy category of topological spaces.
It's more non-constructive than that, though. Even if you use an argument like this to figure out that $X$ and $Y$ have to be homotopy-equivalent to one another, that's a long way from having continuous maps between them, an explicit homotopy equivalence.
A: We know that any two finite fields with the same cardinality are isomorphic.  On the other hand, suppose you have two different polynomials $f, g \in \mathbb{F}_q[x]$ which are irreducible and have the same degree.  I'm not aware of any easy computation which would give an explicit isomorphism of fields $\mathbb{F}_q[x] / \langle f \rangle \simeq \mathbb{F}_q[x] / \langle g \rangle$, which would amount to finding a root of $g$ in the first field.
A: If a purely set theoretic example is acceptable:
The Cantor-Schröder-Bernstein theorem says that a bijection between two sets $A$ and $B$ exists when there are injections $i : A \rightarrow B$ and $j : B \rightarrow A$.
This theorem is not constructively valid. There is information on why this is the case in the answers at that link to a MathOverflow question. Cantor's original proof, for example, used the well-ordering theorem (which is equivalent to the axiom of choice).
Here is a recent paper which shows that Cantor-Schröder-Bernstein implies excluded middle.
A: Lovasz ["A note on the Line Reconstruction Problem", J Combinatorial Theory B, 13, 1972] proved that two finite simple graphs $G,H$ on $n$ vertices with the same collection of unlabeled proper subgraphs must be isomorphic if each has $m > \frac{1}{2}\binom{n}{2}$ edges. It is an attack on the well known edge-reconstruction conjecture. The proof uses inclusion-exclusion to count the set of monomorphisms $G\to H$, and shows that $|G\to H| = |H\to H|$, but $|H\to H|$ is of course greater than zero.
By inclusion-exclusion $|G\to H| = \sum_{X\subseteq G} (-1)^{|E(X)|}|X\to \overline{H}|$ where $X$ runs over all graphs with $V(X)=V(G)$ and $E(X)\subseteq E(G)$, and $\overline{H}$ is the complement of $H$. Similarly, $|H\to H| = \sum_{X\subseteq H} (-1)^{|E(X)|}|X\to \overline{H}|$. Since $G$ and $H$ have the same unlabeled proper subgraphs, the terms on the right hand side with $|E(X)| < m$ must be identical in both equations, and since $m > \frac{1}{2}\binom{n}{2}$, the terms with $|E(X)| = m$ must be zero. Hence, $|G\to H| = |H\to H|$ and so there is at least one isomorphism from $G$ to $H$.
I have never seen a way the proof can be modified to find an explicit isomorphism from $G$ to $H$ using known isomorphisms from $G-e$ to $H-\phi(e)$, where $e\in E(G)$ and $\phi :E(G)\to E(H)$ is some bijection.
A: A contrived example to link this to the law of excluded middle is to start with some proposition $p$ and then consider the set $\{0 \mid p\} \cup \{1 \mid \neg p\}$. It's immediate that classically, this set is isomorphic to $\{2\}$. However, actually having the isomorphism entails knowing whether $p$ is true or false.
A: There are non-constructive techniques for Graph Isomorphism, such as Weisfeiler--Leman (WL). While it is known that WL cannot place Graph Isomorphism into $\textsf{P}$, it serves as a complete invariant for a number of graph families including planar graphs, graphs of bounded tree width, graphs of bounded rank width, and graphs of bounded genus.
To use WL as an isomorphism test, we run WL on the disjoint union of our two input graphs $G, H$. If the multiset of colors for $G$ differ from that of $H$, then we know that $G$ and $H$ are non-isomorphic. For the above families of graphs, this is enough to decide isomorphism.
While the multiset of colors on its own does not in general yield an isomorphism, it is possible to use WL to compute a canonical labeling. Grohe & Neuen have a write-up of this in the appendix here (https://arxiv.org/abs/1901.10330).
