The types say exactly what is proved. There's no real room for confusion. With a written proof you could accidentally make some assumption in the middle (like using some lemma that assumes a thing is finite or compact or whatever when you did not state that assumption), but a computer proof cannot do this. It won't typecheck.
Reading mathematical sentences (types, basically) is like step one in maturing from baby to toddler in math.
> The types say exactly what is proved.
To whom? Fully formalized mathematics is extremely dense and difficult, and few mathematicians actually practice it, especially for complex problems. Just because the symbols are theoretically unambiguous doesn't mean that any human can actually understand what they mean, and whether they accurately encode some less formal system you were hoping to study.
And this becomes much more problematic once you go from the realm of pure mathematics into other realms, like engineering or economics or anything else that is seeking to model real-world phenomena. A model can be perfectly self-consistent and still be a very bad and even useless model of a real-world thing. And it can be highly non-trivial to figure out to which extent and under what constraint a model actually matches the phenomenon you intended.
For examples of both kinds of issues, look at theoretical physics. Lots of major physics theories are only partly formalized, and rely on unproven or sometimes even known to be unsound mathematical foundations (like the Dirac delta at the time it was first introduced, or like renormalization in quantum physics). And, of course, there are still open questions on how well these theories actually model various physical phenomena (like GR and black hole curvature singularities).
Sometimes, and for some people, the right language can actually simplify problems and hide complexity that isn't immediately necessary to the problem at hand. The whole idea is to abstract away models and worry about them separately. This is one of the motivations for the various synthetic theories that are getting researched in the last several years - the one mentioned here happens to be for Category Theory.
This doesn't work for everyone though; some people find it easier to stay grounded in specific models.
I replied to the other stuff elsewhere, but FWIW for the amount I've played with typing up undergrad tier knowledge in Lean, I've found it to be pretty straightforward. Fully formalized math isn't dense. Actually it's the opposite: full of tedious bookkeeping that you learn how to formalize in an intro logic/proofs course. The hard part is making it more dense so that you can read it, and something like Lean actually makes things surprisingly less tedious than you'd expect.
> The types say exactly what is proved. There's no real room for confusion.
Since Lean code isn't the same as natural language or even unobservable human intention, there might always be a mismatch between what the author of a Lean proof claims (or believes) it proves, and what it actually proves.
Anyone capable of reading and writing proofs can also read/write propositions. That's step one. Writing propositions in formal language is exactly why there's no mismatch: it proves what it says it proves. There is no ambiguity. There's nothing else to believe.
Like if you have some f:R->R, a:R in context and write ∀ϵ>0,∃δ>0 s.t. x: R, |x−a|<δ ⟹ |f(x)−f(a)|<ϵ, no one is confused about what you mean.
If you instead write ∃δ>0 s.t. ∀ϵ>0 x: R, |x−a|<δ ⟹ |f(x)−f(a)|<ϵ, you've written something different. Everyone in the field knows this, and actually it's even more obvious when you look at types in something like Lean: roughly ϵ -> (δ, h) vs. (δ, ϵ->h).
Since it's clearly not always trivial to translate conjectures (let alone whole proofs) into Lean code, translating Lean code into understandable conjectures can't be always trivial either.