logoalt Hacker News

canjobear • yesterday at 6:39 PM • 0 replies • view on HN

Because there is a proof! If you are interested in the conjecture, then you would be interested in the proof. If you are not interested in the proof, then you weren't really interested in the conjecture. You were interested in the good style of articles about the conjecture, or the friends you made along the way, etc.

It is of course possible that either (1) the statement of the theorem in Lean is busted or (2) there is a bug in Lean. But both of these seem to me to be lower probability than that the proof is correct. It's not just an e-mail from a crackpot. For someone who is actually interested in the problem, the probability that the proof is correct is high enough to warrant effort to understand it, or at least to learn enough Lean to check the theorem statement.