alt Hacker News>>Incredible lack of curiosity
Maybe on your end because that's the exact point the author explained - these companies need to adhere to the scientific community rather than expecting the opposite.
If the write up - the natural language part - sucks - why are you expecting humans to waste their time on understanding the proof???
Replies
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.
>these companies need to adhere to the scientific community rather than expecting the opposite
Why? The pre-existing community doesn't own science.
Considering how hostile the community sometimes is to outsiders, how they frequently demand form over function and think connections are often more important than correctness of argument, perhaps it's good for them to be confronted with a new approach to science that does away with those things and returns to the real cornerstones: proof and empiricism.
If you don't want to engage with proofs that's your call, many of us are happy to see progress being made and don't need you specifically for the confirmation