Comment by antonvs

> A Lean proof has a much higher probability of being correct

Define “correct” in this context. That’s the real problem here.