2 ms·
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
by strangescript 26d ago
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.
- throwaway81523 26d agoThere 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.