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.