I've heard of many examples of statements that have been proven to be independent of a formal system, meaning that they can't be proven within that formal system (for example, the Continuum Hypothesis is independent of ZFC). I've also heard of examples of proofs showing that certain proof techniques are not powerful enough to prove certain results, such as the result that proofs that relativize cannot resolve P versus NP.
This Stack Overflow question (which might be soon closed or migrated) asks whether we know whether it's possible to resolve P versus NP or not. That got me thinking of whether there are any examples of conjectures where we know that the conjecture can either be proven or disproven within some formal system, but where we don't actually know whether the conjecture is true or not. In other words, are there any conjectures where we can nonconstructively argue that the conjecture is either provable or disprovable, but where we don't know which of these is the case?
I apologize if this is a silly question - I don't have much background in proof theory or model theory.