[monkeyelite]

So that patching is exactly what I’m referring to. The mathematicians can see the idea that’s true, they just need to re-engineer it. That’s why they could move forward with confidence on an unsolved problem.

Lean helps with none of that. It doesn’t help you find proof ideas and it doesn’t help you communicate them,

[okintheory]

You're wrong. The mistake could have been unfixable. That happens quite frequently (see: countless retracted claimed proofs of major results by professional mathematicians).