There are lots of AdS/CFT correspondences, because there are lots of CFTs with the right properties to have a gravity dual. However, as far as I know, none of them have been proven.
Since we don't have any independent non-perturbative definition of quantum gravity on the AdS side of the correspondence$^\dagger$, the conjecture is basically saying this:
- The lower-dimensional CFT is equivalent to a higher-dimensional theory of quantum gravity whose perturbative expansion (in the appropriate parameter) is a string theory.
That's a non-trivial conjecture, because a lot is known about perturbative string theory, even if we don't have an independent non-perturbative definition of string theory.
Even without being proven, the conjecture is still useful for basically the same reasons that science is useful. We can't ever rigorously prove that a theory of how nature works is absolutely correct. We can only accumulate more and more evidence and continue failing to find any compelling counter-evidence. A good theory is still useful, though, because a good theory inspires specific experiments that we might not have thought to try otherwise. Similarly, the AdS/CFT correspondence inspires us to ask mathematical questions that we might not have thought to ask otherwise. This is the idea behind experimental mathematics. The linked Wikipedia article includes this quote attributed to the well-known mathematician Paul Halmos:
Mathematics is not a deductive science—that's a cliché. When you try to prove a theorem, you don't just list the hypotheses, and then start to reason. What you do is trial and error, experimentation, guesswork. You want to find out what the facts are, and what you do is in that respect similar to what a laboratory technician does.
Provisional results derived from the AdS/CFT correspondence may also inspire productive physical experiments in the same way that any theory does. Remember that even the illustrious Standard Model of Particle Physics hasn't been rigorously defined yet (non-perturbatively, not even on a lattice as far as I know$^{\dagger\dagger}$), but it has still been immensely fruitful.
Footnotes:
$^\dagger$ We do have defensible non-perturbative definitions of quantum gravity on the AdS side in the $2+1$-dimensional case. See Carlip, "Six ways to quantize $2+1$-dimensional gravity," https://arxiv.org/abs/gr-qc/9305020.
$^{\dagger\dagger}$ In the paper "Classifying gauge anomalies through SPT orders and classifying gravitational anomalies through topological orders", https://arxiv.org/abs/1303.1803, Wen claims to have constructed "a non-perturbative definition of any anomaly-free chiral gauge [theory]" (from the end of the Introduction).
