If a proof is understandable only by a few people in the world, I would say it fails as a proof, according to your definition. There are many such proofs out there right now. It doesn't help that many of them are wrong, albeit usually in a fixable way.
Making a proof formal doesn't mean it is not understandable any more. First, certainly a machine can "understand" it now. I think with AI improving what exactly such an understanding is worth, and what you can do with it, will increase a lot.
Secondly, the inscrutable tactics-based proofs featured in Lean (I have written such proofs in Isabelle in 1996) are actually quite old-fashioned for such a "modern" prover. Isabelle has long featured human-friendly syntax, and these proofs are certainly as understandable as English text, if written with care.
What we will soon get are proof assistants which allow you to write your proofs (and definitions) in English, but which are still fully formal and checkable.
That is an immense help if you are producing new knowledge, because usually nobody else looks at your work with sufficient scrutiny in the first place. If you understand it, and in addition the machine "understands" it, I think that will be the gold standard for proofs very soon.
It will also help mathematicians to clean up their act ;-)
