I think the quote is about the fallibility of the humans who convert theorems into statements of type theory. You could end up with a valid theorem, but not the theorem you meant to prove. This would be a bug in the statement of the theorem, not the proof.
For example, you might want to prove that a certain sorting algorithm is correct. You formalize the specification as "for every two integers i, j, output[i] <= output[j]" and prove that outputs of the algorithm satisfy this spec. However, this is not a correct characterization of sorting, since the algorithm might return the empty list.
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.
It's an important problem and people in formal verification are aware of it. One example of tackling this is that the Lean LTE team accompanies the proof with "several files corresponding to the main players in the statement" and "[they] should be (approximately) readable by mathematicians who have minimal experience with Lean [...] to make it easy for non-experts to look through the examples folder, then look through the concise final statement in challenge.lean, and be reasonably confident that the challenge was accomplished".
For example, you might want to prove that a certain sorting algorithm is correct. You formalize the specification as "for every two integers i, j, output[i] <= output[j]" and prove that outputs of the algorithm satisfy this spec. However, this is not a correct characterization of sorting, since the algorithm might return the empty list.