Post-quantum cryptography is the development of cryptographic protocols that are not easily crackable using a fault-tolerance quantum computer. I know that NIST has a competition to find the best post-quantum cryptography algorithm, and some of the proposed algorithms have already been shown to not be safe using classical computers. However has it been already proved that such an algorithm exists (not necessarily which one is it)? Or do we rely on our best attempts at it? Could it still be possible to prove mathematically that such a protocol may not exist?
No. Proving this requires (among other things) proving that P$\ne$NP.
 We have not proven that a post-quantum cryptographic protocol, satisfying all reasonable definitions, necessarily exists. In particular, we probably won't be able to prove the existence - or lack thereof - prior to conversion from RSA to, say, some version learning with errors (LWE). Such a proof necessarily requires splitting BQP from NP, and we can't even unconditionally split P from PSPACE yet.
 Indeed even when RSA started becoming the dominant standard for public-key cryptography, it was known that the security of RSA was contingent on the difficulty of factoring large itnegers. Back in the 1970's, Rivest, Shamir, and Adelman knew that (1) factoring is NP, and strongly believed that (2) factoring is not in P or BPP. Shor's great 1994 discovery, of course, is that factoring is not a difficult problem if we live in a world where fault-tolerant quantum computers (FTQC) exist.
 Ramping it up, NIST is actively engaged in finding the best candidate public-key protocols that (1) are in NP, but (2) are not likely to be in BQP. The protocol needs to be in NP because there needs to be a (classical) communication path to certify the messaging, and should be outside of BQP to preclude a quantum computing attack. This is the "post" in "post-quantum cryptography". But, we are far (far?) away from being able to affirmatively prove that there's necessarily such an interstitial problem between NP and BQP, much less that LWE is such a problem.
 If a candidate problem is "cracked", that could mean that the problem is shown to be in P (or BPP or even BQP) or else there exists a significant - e.g., quasipolynomial - speedup over the presumed naïve difficulty. But showing that one problem is not post-quantum secure, as has been done, doesn't prove that there is no such problem that is a suitable candidate for post-quantum cryptography.
 I'll refer to Boaz Barak's 2017 blog-post and essay on different worlds of quantum computing, see here. Barak refers to a world where FTQC exists and exponentially outperforms classical computers as "Superiorita". Barak notes that such a world most likely does have such interstitial problems, with LWE being a good candidate for post-quantum cryptography.
 Barak's article is a follow-up from an earlier famous mid-90's article by Impagliazzo and titled "A personal view of average-case complexity", see here among other places. In my version of Impagliazzo's article he asserts that "as far as we know, the RSA cryptosystem is secure" but doesn't mention Shor's algorithm. I guess this was because the article was written contemporaneously with Shor's discovery. Impagliazzo appeals to RSA to define a world called "Cryptomania" wherein public key cryptography exists - but emphasizes that this is a stronger assumption than even that P$\ne$NP!
 NIST is running under the assumption that we live in "Superiorita", that is, an FTQC capable of cracking RSA can be built. NIST also is running under the assumption that we live in a BQP-upgraded "Cryptomania", that is, public key cryptography, secure against quantum computers, can be performed. One of these is more mathematical than the other. But as of September 2023, both of these are fundamentally conjectures.