It's an important problem and people in formal verification are aware of it. One example of tackling this is that the Lean LTE team accompanies the proof with "several files corresponding to the main players in the statement" and "[they] should be (approximately) readable by mathematicians who have minimal experience with Lean [...] to make it easy for non-experts to look through the examples folder, then look through the concise final statement in challenge.lean, and be reasonably confident that the challenge was accomplished".

Details in this blog post: https://leanprover-community.github.io/blog/posts/lte-exampl...