Request: Induction, Proof, Experimental mathematics
Suppose we made an algorithm capable of forming empirical conjectures for mathematics. How might such an algorithm discover the principle of mathematical proof?
I would like to see an article on the relevant philosophy and mathematical logic background for this problem. Since I currently lack the inclination to research and write up such an article, I instead made this post.
Recognizing and generalizing nontrivial mathematical patterns from the world, at the level you mean, seems (to me) to be AI-complete; on the other hand, in a domain with lots of variables and unreliable human intuition, Eurisko did pretty well at basically that.
Funny that you should mention Eurisko and not Automated Mathematician by the same guy, because the postulated agent sound pretty close to AM.
Huh, I hadn’t heard of that. The controversy around it is… interesting.
The controversy around AM is the same as around Eurisko, right? that it’s not clear how much was the AI and how much was Lenat. I believe that Lenat says the Traveller fleet design was 60% Lenat and 40% Eurisko. It’s not clear what it means to quantify that, so it’s not clear that he disagrees with the skeptics. In fact, his abandonment of Eurisko suggests that he agrees. Here’s the OB discussion of Lenat.
I was thinking that the downvotes were a reaction to the last sentence, though like prase I had a hard time figuring out what you were asking for. I’m reading “capable of forming empirical conjectures for mathematics” as capable of using evidence to make reasonable guesses about the answers to math problems and “discover the principle of mathematical proof” as figure out that mathematics principles can be proven. Is this close to your intended meaning?
The last sentence is annoying too, granted.
The downvotes probably reflect the fact that it is very hard to understand what you are precisely asking for. Perhaps you could explain what you mean by empirical conjectures for mathematics and principle of mathematical proof.
Suppose we made a program to hunt for possible natural-number identities, of the form f(k)=0. These identities are coded by symbolic strings such as “k-k”. The general goal of the program is to produce a large and diverse list of high-confidence identities. (Defining a specific function for specifying this goal is difficult.) The program begins with a law of induction which says: “if f(k)=0 for k=0...n, and there are no known counterexamples to f(k)=0, then f(k)=0 for all natural numbers with subjective probability (n-1)/n”
The program might direct its search with the use of heuristics, for example: generating new candidate identities f’(k)=0 by mutating previously investigated identities f(k)=0 which have high confidence. To take the program to the next level of complexity, we have it search for modification heuristics which always produce valid identities from other valid identities. I have not yet thought the precise formulation for the induction law for heuristics and for candidate identities generated by use of heuristics. However, it seems possible that a program could find a set of high-confidence modification heuristics which are equivalent to ZFC mathematics. Or perhaps it would be necessary to search for modification meta-heuristics.