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.
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.