4 ms·
> If AlphaProof generated a long and unreadable proof... Then how would anyone be sure it isn't wrong? It was great that while Goldston and Yıldırım were wron
by 8bitsrule 6y ago
> If AlphaProof generated a long and unreadable proof...
Then how would anyone be sure it isn't wrong?
It was great that while Goldston and Yıldırım were wrong, their work proved to be useful. A lot of people are glad that Riemann (and Fermat) didn't their problems!
- whatshisface 6y agoWe have automated proof checkers like CoQ. A proof machine would be designed to output proofs in a syntax that could be mechanically checked by an existing verifier.