1. Sure, but verifying a spec is still much easier than verifying a whole proof (as we traditionally do).
2. In that example that you gave, you would have additional evidence: if you use your system and every sort returns an empty list, you'd probably notice it quite quickly. You can also do manual or automated testing to see that it does the right thing for example inputs. If you then consider it to be unlikely that someone writes code that would exactly only work for example inputs and only satisfy the specification in the dumbest possible way, then you get some really good evidence that your algorithm is actually correct. 100% certainty is never possible, but there are still degrees.
Agreed. I think the interviewee is a little pessimistic when he says "I’m just not sure it’s any more secure than most things done by humans." about computer assistance. If the ABC conjecture were to be proven in Lean, I'm pretty sure it would be accepted as true by an overwhelming majority of the mathematical community.
The proof is not rejected because people don't understand it, it's rejected because people don't think the proof is correct.
If the proof was translated to Lean, then it would mean a lot if it managed to prove the ABC conjecture because it would mean the proof was correct. It doesn't matter if the proof used crazy definitions. The statement of the ABC conjecture would still be understandable and so the ABC conjecture would be solved.
> The ABC conjecture "proof" is rejected because it uses definitions and arguments no one understands.
I would like to point out that it seems like the general consensus now is that Mochizuki's proof is incorrect.
And, as people pointed out early on, one of the problems with the Mochizuki paper is that it provides no new tools or results for other problems in the space. This is quite unusual and was a significant part of the skepticism about the proof being correct.
Contrast this to Wiles proof of the Taniyama-Shimura-Weil conjecture for semistable elliptic curves which proves Fermat's Last Theorem as a consequence and then led to a full proof which later became the "modularity theorem".
If Mochizuki used the tools from his paper come at something already proven from a different direction, that would have lent a lot more credence to his claims.
> 1. Sure, but verifying a spec is still much easier than verifying a whole proof (as we traditionally do).
I agree.
In the Metamath community, we also check all proofs with a collection of verifiers written by different people in different languages, all based on a very small kernel. That provides extremely high confidence in its correctness.
2. In that example that you gave, you would have additional evidence: if you use your system and every sort returns an empty list, you'd probably notice it quite quickly. You can also do manual or automated testing to see that it does the right thing for example inputs. If you then consider it to be unlikely that someone writes code that would exactly only work for example inputs and only satisfy the specification in the dumbest possible way, then you get some really good evidence that your algorithm is actually correct. 100% certainty is never possible, but there are still degrees.