A question that answers itself.
If P=NP could be proved in a formal language, then surely it would be as easy to verify the proof as it would be to discover/derive it? Couldn't a program just quickly check that every sentence/line obeyed the formal rules?
If P!=NP could be proved in a formal language, then it could take a while to do so.
Its taken a while to formally prove either P=NP or P!=NP.
-> So either our language isn't accurate, isn't formal enough or P!=NP?
Suppose that $\mathsf{P}=\mathsf{NP}$. Your argument seems to be the following: since there exists an algorithm $A$ that is able to check whether a given short proof of mathematical statement is valid then there must exist an algorithm $B$ that decides whether such a short proof exists. Let's use $B$ on the statement $\mathsf{P}=\mathsf{NP}$.
There are several problems with that. First it assumes that $\mathsf{P}=\mathsf{NP}$ in the first place. If we knew that this is true we would have no need to run $B$ on $\mathsf{P}=\mathsf{NP}$.
Second, it assumes that we know $B$ while the above argument only shows that some $B$ must exist. It might be the case that $B$ exists but we don't know it. Moreover, if $B$ existed and we knew it, then $B$ itself would be a proof that $\mathsf{P}=\mathsf{NP}$.
Third: Suppose that $\mathsf{P}=\mathsf{NP}$ (but we don't know it) and that we have some magic candidate algorithm $B$. $B$ is only able to decide whether an input statement admits short proofs. By short I mean proofs whose lengths are upper bounded by $n^c$, where $n$ is the length of the statement, and $c$ is a constant of choice. How do you pick $c$? We don't know how long a proof of $\mathsf{P}=\mathsf{NP}$ is.
Finally, notice that $\mathsf{P}=\mathsf{NP}$ is a specific statement. Therefore, if we assume that "$\mathsf{P}=\mathsf{NP}$" can be proved either true or false, then we already have a constant-time algorithm that settles the matter. Consider the shortest proof written in binary (in some proof language) of "$\mathsf{P}=\mathsf{NP}$" or "$\mathsf{P} \neq \mathsf{NP}$" and let $k$ be its length. Clearly $k$ is a fixed number. We can simply generate all possible proofs in lexicographic order and check whether each of them is a valid proof of either "$\mathsf{P}=\mathsf{NP}$" or "$\mathsf{P} \neq \mathsf{NP}$". Eventually we will reach the proofs of length $k$. There are only finitely many proofs of length at most $k$ (namely $2^{k+1}-1$) and checking each of them requires a time upper bounded by some function $f(k)$. Therefore the overall running time is $O(2^k f(k)) = O(1)$. This constant can be huge and this does not bring us any closer to settling the $\mathsf{P}$ vs $\mathsf{NP}$ question.
Sometimes a short and easily verifiable proof takes a long time to discover. This may be due to several reasons. Maybe the general consensus in the research community is that the claim is probably not true, and most people who work on it are trying to prove the converse. Maybe it's believed to be too difficult for current techniques, and most researchers prefer to work on easier problems where progress can be made. Maybe finding it requires computer searches that were out of reach of older (or even current) hardware. Maybe it requires some radical new idea.
For a concrete example, take Kaplansky's unit conjecture. It claims that certain classes of generalized polynomials $K[G]$ do not contain nontrivial invertible elements. If this conjecture is false, then there exists such a class $K[G]$ and a nontrivial invertible polynomial $f \in K[G]$. If we are given this $K[G]$ and $f$, it's easy to verify (by computer or on paper) that it disproves the conjecture. The conjecture was stated in 1940 and publicized in the 1950s, and a counterexample was found by Gardam in 2021 using a computer search. He has stated that it ran on his laptop, so it probably would have been in reach of much earlier supercomputers.
Then there's the possibility that $P = NP$ is provably true, but its simplest proof is very long and difficult. Maybe there is a polynomial time algorithm for Boolean satisfiability, but it's extremely intricate and has a running time of $n^{10000}$ or something even more outrageous.
It's important to address the elephant in the room:
Why has it taken so long to prove that P != NP?
This has not been proven.
The argument you have given "does not compute" - it uses terms that simply do not find together.
The one (the question of whether $P$ equals $NP$) and the other (the difficulty of finding a proof for it or its opposite) has nothing to do with each other whatsoever. Since the $O$ notation removes all multiplicative and additive constants, there can be P problems which are arbitrarily difficult to solve, so you can never use the perceived difficulty in finding a solution/proof to argue whether a problem is in $P$ or $NP$, both or none. As a fun example, by some definitions chess is an $O(1)$ problem in $P$.
