3 ms·
> Makes you wonder what will happen when instead of the rules of chess, you put in the axioms of logic and natural numbers. And give it 8 months of compute. Ho
by chx 9y ago
> Makes you wonder what will happen when instead of the rules of chess, you put in the axioms of logic and natural numbers. And give it 8 months of compute.
How do you score this computation? What's your goal? There's no checkmate here.
- mortenjorck 9y agoI think the idea here is for life to imitate art.
- thomasahle 9y ago> How do you score this computation? What's your goal? Maybe give it a list of problems of varying degree of hardness, and tell it to either prove or disprove as many as possible?
- Will_Parker 9y agoYou could even train it with random theorem expressions run through a conventional theorem prover. And then let it loose on the problems that are left.
- criddell 9y agoI would assume you have to come up with some scoring function. For example, give it a number and tell it to factor it into the prime factors. The score might be the solution with the smallest time or storage requirements. Or maybe find a way to generate a hash where the last n digits are zero. I also remember a RadioLab episode where they talked about electronic theorem solvers and they would do something like show it a video of a double pendulum and it would come up with equations to model the behavior of that system.