3 ms·

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 as

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.

hgsgm 3y ago
The ABC conjecture "proof" is rejected because it uses definitions and arguments no one understands. It would not necessarily be hard to program in those incoherent definitions and get them to prove a result. That wouldn't mean much. This is different from just programming in the conjecture and letting Lean find a complete proof.
- Pazzaz 3y ago
  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.
- bsder 3y ago
  > 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.

hgsgm 3y ago

The ABC conjecture "proof" is rejected because it uses definitions and arguments no one understands. It would not necessarily be hard to program in those incoherent definitions and get them to prove a result. That wouldn't mean much. This is different from just programming in the conjecture and letting Lean find a complete proof.

Pazzaz 3y ago
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.
bsder 3y ago
> 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.