alt Hacker NewsThis is a step beyond baseless predictions. Tao also had a "weird" "hypothetical" comment about LLMs solving complex proofs with impossible to human verify Lean.
This is a step beyond baseless predictions. Tao also had a "weird" "hypothetical" comment about LLMs solving complex proofs with impossible to human verify Lean.
There are theorems like that now, like de Grey's lower bound for the Hadwiger-Nelson (unit distance graph) problem. He used a SAT solver to check that a certain graph with 1581(?) vertices is not 4-colorable. There's no way for a human to check that.
Even simpler, imagine Anthropic announces Goldbach's conjecture is false and they have a billion digit counterexample. Anyone can download it (300MB compressed), but how do you check it?
Doron Zeilberger for decades has expected incomprehensible computer proofs to eventually take over mathematics.