4 ms·
If AlphaProof generated a long and unreadable proof with no discernible structure, it would not be such a large contribution to mathematics as if a human figure
by lacker 6y ago
If AlphaProof generated a long and unreadable proof with no discernible structure, it would not be such a large contribution to mathematics as if a human figured out "why" and wrote it in a way other humans could understand.
Maybe not directly. But if AlphaProof managed to prove the Riemann hypothesis, I bet it wouldn't be long before human mathematicians had managed to decipher the proof and explain it in a way that other mathematicians found useful. It's just a lot easier to re-explain something that other people have already proved, rather than proving it yourself.
- Jabbles 6y agoGödel's incompleteness theorem doesn't fill me with the same confidence as you that "a true theorem should have a useful explanation". In fact, looking at chess engines tells us that sometimes (though not always) brute-force calculation of many possibilities gives us better moves. In the same way some true statements might just be an exhaustive calculation. Perhaps the four color theorem is the most famous example of a proof that has lacked (still lacks) a lot of useful lemmas in relation to its length: https://en.wikipedia.org/wiki/Four_color_theorem https://en.wikipedia.org/wiki/Four_color_theorem
- lacker 6y agoYeah, it certainly isn't true that a true theorem should have a useful explanation. I only have my human intuition to go on, but I bet the Riemann hypothesis would not be like the four-color problem. Graph-type problems just seem to lend themselves to exhaustively checking a zillion cases in a boring way, whereas in fields like number theory or analysis that sort of proof hardly ever seems to exist. I hope we do get some famous theorems proved by computers so that we can see whether it's enlightening to humans. I am quite curious whether my intuition is correct and it is a shame to think I might never know....