If something that looks obviously true is hard to prove using some given language, couldn’t that be a sign that we’re using the wrong language to construct the proof?

Could there exist a language where these sorts of proofs become easier to write, because that language captures the problem in a better way?