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