4 ms·
One perfect-information game that's at least as hard: constructive mathematics. (Proof assistants even give it a sort of videogame-style UI.) I've been wonderin
by abecedarius 11y ago
One perfect-information game that's at least as hard: constructive mathematics. (Proof assistants even give it a sort of videogame-style UI.) I've been wondering about some kind of neural net for ranking the 'moves' coupled with the usual proof search.
- seanwilson 11y agoI don't know much about Go but I'm guessing general proof automation would be many, many orders of magnitudes harder. The branching factor is huge (you can apply any theorem you want to the current goal and go down a bad path) and knowing if you're on the right track to finish a proof isn't obvious.
- abecedarius 11y agoYeah, I don't imagine this is easy. The applications for even incremental advances here should be obvious.
- canndrew2016 11y agoI asked about this in /r/dependent_types yesterday. Apparently there's already a fair bit or research going on in this area. See the links: https://www.reddit.com/r/dependent_types/comments/49z1uc/using_alphago_as_a_theorem_prover/ https://www.reddit.com/r/dependent_types/comments/49z1uc/usi...
- abecedarius 11y agoThanks, that's very helpful.