> Theres nothing difficult about formalizing a proof you understand.

What are you basing that on? It's completely false.

If that were true, we would have machine proofs of basically everything we have published proofs for. Every published mathematical paper would be accompanied by with its machine-provable version.

But it's not, because the kind of proof suitable for academic publication can easily take multiple years to formalize to the degree it can be verified by computer.

Yes of course a large part depends on formalizing prior authors' work, but both are hard -- the prior stuff and your new stuff.

Your assertion that there's "nothing difficult" is contradicted by all the mathematicians I know.