Is there any conjecture that we know is provable/disprovable but we haven't found a proof of yet?

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?

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.

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.