Hacker News new | ask | show | jobs
by Pazzaz 1021 days 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.