I know that there are a lot of unsolved conjectures, but it could possible for them to be independent of ZFC (see Could it be that Goldbach conjecture is undecidable? for example).
I was wondering if there is some conjecture for which we have proved that either a proof of it or a proof of its negation exists, but we just haven't found that proof yet.
Could such a proof of dependence even exist, or would the only way of proving that a statement is dependent be proving/disproving it?
On
Eric Wofsey's answer is certainly more comprehensive, but I thought I'd provide an example where the assurance that there's a proof of $P$ or $\neg P$ that's not of the form "there's a straightforward, if tedious, algorithm to check things" as there is in the case of Ramsey Theory or who wins a game like Chess.
The question is that of the "kissing number" for dimension 5 (or anything higher except 8 or 24). In 1d, two intervals of the same length can touch a third without overlapping. In 2d, 6 circles of a given radius can touch a 7th. We don't know the highest number of 5d spheres of a fixed radius that can all touch the same one, but the answer is between 40 and 44, inclusive. Since we're dealing with real numbers, I'd argue there's no obvious algorithm like with Ramsey Theory: we can't just test all of the possible centers of spheres.
However, because this kind of question can be translated into a simple statement about real numbers (think about using dot products to deal with the angles, for instance), it only depends on what things are true in any "real-closed field" (a field that acts like the real numbers for many algebraic purposes).
The thing is, the theory of real-closed fields is complete and decidable! Everything you can phrase in the language of real-closed fields can in theory be proven true or false with an algorithm, and they're even relatively efficient.
This example is not my own, and is discussed in a number of places, including these slides on "Formal Methods in Analysis" by Jeremy Avigad.
On
Could such a proof of dependence even exist, or would the only way of proving that a statement is dependent be proving/disproving it?
I'd like to address this specific question. It is not true in general that a existence of a proof of $P$ implies that $P$ itself is true. Neither is it true that existence of proof of provability of $P$ implies the provability of $P$. By Lob's theorem, each of these fails for some sentence $P$, if your foundational system is strong enough (ZFC set theory is certainly more than enough). To be 100% precise:
Take any formal system $S$ that satisfies the Hilbert-Bernays provability conditions, where $\def\box{\square}$"$\box_S P$" denotes the uniform arithmetical sentence representing "$S$ proves $P$", and we just write "$\box P$" if it is in the context of "$S \vdash \cdots$". Then the external form of Lob's theorem (L* in the linked post) asserts that if $S \vdash \box P \to P$ then $S \vdash P$. If $S$ is consistent, then $S \nvdash \bot$ and hence $S \nvdash \box \bot \to \bot$. Read in English, this shows that $S$ does not always prove that provability implies truth, even for individual sentences one at a time.
More can be said. If $S \vdash \box \box P \to \box P$ then by (L*) again we get $S \vdash \box P$. If $S$ is $Σ_1$-sound then $S \nvdash \box \bot$, so $S \nvdash \box \box P \to \box P$ does not hold when $P = \bot$. In English, S does not even prove that existence of proof of provability implies provability.
Strangely, it could even be possible (but no logician believes so) that ZFC is consistent but proves ¬Con(ZFC), which literally means that ZFC proves the existence of a proof of contradiction over ZFC even though there is no such proof...
More specifically, (in very weak meta-systems) we can easily prove that if ZFC is consistent then ZFC' = ZFC+¬Con(ZFC) is also consistent but yet ZFC' proves ¬Con(ZFC'). Of course, anyone who believes that ZFC is consistent ought to reject ZFC' because it denies its own consistency. But the problem is that we cannot ever figure out whether ZFC itself is already like ZFC' in being consistent but $Σ_1$-unsound, unless we actually find something like a concrete proof over ZFC of ¬Con(ZFC). But we actually hope that ZFC is $Σ_1$-sound, in which case we can never establish it non-circularly.
Now to explicitly answer the question interpreted externally, it is possible that $S \vdash \box P \lor \box \neg P$ and yet $S \nvdash P$ and $S \nvdash \neg P$, so 'proof of dependence' is not necessarily a reliable indicator of actual dependence! Here is one general explicit construction:
Take any $Σ_1$-sound formal system $S$ that satisfies the Hilbert-Bernays provability conditions. Let $S' = S + \box_S \box_S \bot$. Then we have:
$S' \vdash \box_{S'} \box_S \bot \lor \box_{S'} \neg \box_S \bot$, since $S' \vdash \box_S P \to \box_{S'} P$ for any sentence $P$ over $S$.
$S' \nvdash \box_S \bot$, otherwise $S \vdash \box_S \box_S \bot \to \box_S \bot$, and hence $S \vdash \box_S \bot$ by (L*), contradicting the $Σ_1$-soundness of $S$.
$S' \nvdash \neg \box_S \bot$, otherwise $S \vdash \box_S \box_S \bot \to \neg \box_S \bot$, but $S \vdash \neg \box_S \box_S \bot \to \neg \box_S \bot$ by (D3), and hence $S \vdash \neg \box_S \bot$, contradicting Godel's incompleteness theorem.
There are plenty of problems in mathematics which can be done by a finite computation in principle, but for which the computation is too large to actually carry out and we don't know of any shortcut to let us find the answer without (more or less) computing it by brute force. For instance, the value of the Ramsey number $R(5,5)$ is unknown, even though it is known that it must be one of the numbers $43,44,45,46,47,$ or $48$. We know that a proof of which number it actually is exists, since you can in principle find the answer by an exhaustive search of a finite (but very very large) number of cases.
Another example is solving the game of chess. We know that with perfect play, one of the following must be true of chess: White can force a win, Black can force a win, or both players can force a draw. A proof of one of the cases must exist, since you can just examine all possible sequences of moves (there are some technicalities about repeated positions but they don't end up mattering).
In fact, every example must be of this form, in the following sense. Suppose you have a statement $P$ and you know that either a proof of $P$ exists or a proof of $\neg P$ exists (in some fixed formal system). Then there is an algorithm which you can carry out to determine whether $P$ or $\neg P$ is true (assuming your formal system is sound, meaning that it can only prove true statements): one by one, list out all possible proofs in your formal system and check whether they are a proof of $P$ or a proof of $\neg P$. Eventually you will find a proof of one of them, since a proof of one exists. So this is a computation which you know is guaranteed to be finite in length which you know will solve the problem.