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