Let us consider the beginning of the proof given in Diophante site. Three new unknowns appear, defined by:
M/N=(C-A)/B=B/(C+A) the parities of M and N being different. This gives:
A/(M2-N2)=B/(2*M*N)=C/(M2+N2)=D
D is an integer because two denominators have never a common factor.
Therefore, one has to solve:
2*M*N*(N-M)*(N+M)*D2=311850*P
As either M or N is even, P is an even prime, therefore P=2:
M*N*(N-M)*(N+M)*D2=2*34*52*7*11, thus D is a divisor of 32*5=45.
The end of the proof is given in the site. After several skilled deductions, and some local backtracks, both solutions are found. Clearly, both proofs are completely different.
This is an excellent proof. The value of P is found without backtracking; the mathematician who discovered it is very clever. However, I had some difficulties to understand it, and more importantly, I cannot see how I could have found it. On the contrary, I easily understood CAIA’s proof, and I see how it could be possible to generate a meta-explanation, which indicates how it can be found. For the present time, CAIA can automatically create explanations, but it cannot yet create meta-explanations: I have more important problems to solve for bootstrapping AI, and I cannot spend my time on a problem that will not help to advance the bootstrap.
However, I will indicate some elements of a meta-explanation, easily taken from CAIA’s explanation. When it solves a problem, CAIA may have to choose one of the three following actions:
To decide to backtrack, and to choose a disjunction.
To choose a deduction that will enable it to create a new constraint from the already known constraints.
To normalize a new constraint. To do that it applies the simplification rules. For instance, it replaces by 0 a product where one of the factors has a zero value. No meta-explanation is given for this step: the simplification rules are always applied to a new constraint.
CAIA backtracks when no deduction is in its to-do list. Then, for choosing a disjunction, it selects the most interesting disjunction. The interest of a disjunction depends on the number of its choices, and the interest of its less interesting element: an equality with one unknown is better than one with several unknowns, an equality is better than a congruence, when there is an AND inside the ORs, creating several new constraints is better than creating only one, etc.
During the initial phase of the Saint-Exupéry problem, CAIA does not find the value of an unknown, although it tried all the possible deductions. At that time, it had generated 12 disjunctions. One of them considers the parity of two unknowns, another one, [22], defines the parity of three unknowns; therefore, it prefers the second disjunction. Most of the other disjunctions are not so interesting, for instance: A is a multiple of 11 OR B is a multiple of 11, which add a congruence for only one unknown. However, another promising candidate was: P is odd OR P=2. It was not chosen, but it would have given a completely different proof.
When a rule has been executed, the conditions of this rule indicate why it has been chosen. Naturally, many constraints have been created, which are not used in the explanation. In that situation, I add nothing to the meta-explanation.
Let us consider some steps of the explanation given by CAIA, described in the preceding blog.
After creating [39] where a product is equal to a constant, one considers the rule that creates a disjunction indicating all the possible correspondences between the elements of the product and the factors of the constant. This is also used after [73] and [104]. No meta-explanation is necessary: when the conditions of this rule are satisfied, one executes it.
When a constraint such as [48], [82], or [115] is a disjunction of the values of N unknowns, and if another constraint gives the value of another unknown from the values of some of the N unknowns, one creates a new disjunction which defines the values of N+1 unknowns. Naturally, one checks that this element satisfies the other constraints of the problem that may exist on these N+1 unknowns, for instance B<=A. For the first two cases, one has a contradiction: for every element, there is no possible value for the new unknown. For [115], this gives the two solutions. In this case, there is no meta-explanation to give: one considers all the disjunctions satisfying the conditions, and for each one, one applies successively all the constraints that could define the value of a new unknown.
The use of the rule leading to the proof of [62] and [94] is more difficult to meta-explain, because CAIA has to make a choice. This rule indicates that, if one has a constraint A=B, one also has A ≡ B (mod L) for any integer L greater than 1. The difficulty is that there is an infinite number of possible values for L. In the definition of this rule, an algorithm generates a set of possible values for modulo L. Then, one only tries these modulo, and one keeps a result when it is interesting.
For instance, if an equality constraint includes an unknown V to the power 5, and if V≡ 3 (mod 15), then one considers L=45. The new constraint will be simplified since V5 ≡ 18 (mod 45) when V≡ 3 (mod 15). This table, giving the modulo to consider depending of the power of an unknown and its congruences, was automatically generated. In the present proof, when B is odd, one considers for L the values 2, 4, and 8. With L=8, and when B and C are odd, we have B2≡ 1 (mod 8), and C2≡ 1 (mod 8); after simplification, A2+B2≡C2 (mod 8) becomes A2≡0 (mod 8), simplified into A≡0 (mod 4).
In the next blog, I will add more comments on meta-explanations, based on CAIA’s solution for the Saint-Exupéry problem.