Theres nothing difficult about formalizing a proof you understand.

Formalizing hot garbage supposedly describing a proof can be arbitrarily difficult.

The problem is not a missing library. The number of definitions and lemmas indirectly used is often not that much. Most of the time wasted when formalizing is discovering time and time again that prior authors are wasting your time, sometimes with verifiably false assumptions, but the community keeps sending you around to another gap-filling approach.

> 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.