Where is the proof of AdS/CFT? People have been using the AdS/CFT correspondence for some time now. But I have yet to see a formal proof. Does one exist? Or is it still a conjecture?
(Well I have seen claimed proofs).
I have seen rigorous mathematical statements of the conjecture but not a proof of it.
Or is the status of AdS/CFT more like the Goldbach conjecture. In that it is assumed to be true because no counter example/contradiction has been found?
People are using it and saying it is a "useful tool". But if it is still a conjecture then how is it useful? You can't know if you have the correct results unless you can do the calculation in the dual model. But if you have to check everything in the dual model then the correspondence seems kind of redundant.
Or, has it been shown to be true in a subset of cases, and so it is a "useful tool" as long as one restricts oneself to those cases? But again, unless there exists a proof for this subset of cases, it seems like the only way to know it works in this subset is to compare it with the results in the dual model.
 A: 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).
