3 ms·
Let me add to this. When you try to formalize a proof in a proof assistant, then almost all of the time, you will find numerous errors in the proof. But - and
by jlouis 14y ago
Let me add to this. When you try to formalize a proof in a proof assistant, then almost all of the time, you will find numerous errors in the proof.
But - and this is key - these errors are usually fixable or the area is not understood well enough and requires more attention to detail. The human intuition is quite powerful.
- scotty79 14y agoThat's similar to when you subject working software system to new batch of tests or test it in some new way. Usually a lot of previously known errors will crop up despite that the system already works mostly as intended.