3 ms·
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
by monkeyelite 1y ago
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 1y agoYou're wrong. The mistake could have been unfixable. That happens quite frequently (see: countless retracted claimed proofs of major results by professional mathematicians).