It is interesting, to compare the solutions found by CAIA with those found by a human mathematician. Diophante is a very useful site, which proposes many mathematical problems, with one, and sometimes several, solution. I will consider the solution found by CAIA, and the one given by Diophante for the same problem. One finds it by clicking in sequence on « problèmes par thème », then « A. Arithmétique et algèbre », « A1. Pot pourri », and finally « A10168. Le défi de Saint-Ex ». This problem was found by Antoine de Saint-Exupéry a few days before he was shot down with his plane during ww2. Rated 3 out on 5 by the site, it is of medium difficulty.

CAIA has to solve the following problem: Find the value of four unknowns A, B, C, and P, which are positive integers satisfying 3 constraints:

[1] P is prime

[2] A*B=311850*P

[3] A² + B² = C²

CAIA begins with looking for symmetries, that are permutations of the unknowns that lead to the same set of constraints. This meta-problem, finding symmetries, has been defined for CAIA; it solves it using the same methods as for the other problems. It finds, very easily, that there is only one symmetry that transforms A, B, C, P into B, A, C, P. As it does not want to generate symmetrical solutions, CAIA adds the constraint:

[4] B<=A

CAIA performs many deductions for solving a problem. When it is completed, it extracts the deductions that are necessary for justifying it: it is the explanation. I will now give the explanation found by CAIA for the Saint-Exupéry problem. Before each new constraint, I indicate, between brackets, their number as it is given by CAIA. The missing numbers were for constraints that are not necessary for the explanation. The first useful constraint that it generates is:

[22] [A even AND B even AND C even] OR [A even AND B odd AND C odd] OR [A odd AND B even AND C odd]

Then, it decides to backtrack, successively considering the three possibilities of [22].

No1 case. A even AND B even AND C even

In [2], A and B are even, A*B is at least a multiple of 4, 311850 is not a multiple de 4. Therefore, P is even; the only even prime is 2.

[34] P=2

[39] A*B=623700

[48] [A=3850 AND B=162] OR [A=2310 AND B= 270] OR [A=1650 AND B= 378] OR ………..]

There are 30 possibilities in this disjunction. CAIA finds them from the factors of 623700, keeping only the values that satisfy the three conditions: A and B are even, and B<=A.

From [48], CAIA creates a new constraint where, for each couple of values for A and B, it adds the value of C obtained from [3]. If C² is not a square, there is nothing for it in this new constraint. In this case, this happens for the 30 couples of values for A and B. Therefore, the new constraint is FALSE, there is a contradiction.

No2 case. A even AND B odd AND C odd

From [3], CAIA generates the constraint A² + B² ≡ C² (mod 8). CAIA simplifies it, first using that if x is odd, then x² ≡ 1 (mod 8). The constraint becomes A² ≡ 0 (mod 8), which becomes:

[62] A ≡ 0 (mod 4)

Then, A*B is a multiple 4, so:

[70] P=2

[73] A*B=623700

[82] [A=623700 AND B=1] OR [ A=1540 AND B=405] OR [A=1100 AND B=567] OR …..]

36 possibilities are in this disjunction, coming from the factors of 623700, checking for each one A even, B odd and B<=A. For each couple, one determines, if possible, the value of C, using [3]. Here again, the value for C² is never a square. Therefore, the new constraint is FALSE: there is a contradiction.

No3 case. A odd AND B even AND C odd

CAIA still considers A² + B² ≡ C² (mod 8) which becomes this time:

[94] B ≡ 0 (mod 4).

Following the same steps that in the preceding case, CAIA finds:

[101] P=2

[104] A*B=623700

[113] [A=1925 AND B=324] OR [A=1155 AND B=540] OR [A=825 AND B=756] OR …..]

24 couples are in this disjunction. Computing C for each couple, one has only:

[115] [A=825 AND B=756 AND C=1119] OR [A=1155 AND B=540 AND C=1275]

This gives the two basic solutions for this problem. There are also two symmetrical solutions, where one swaps the values of A and B.

In the next blog, I will compare a human method for solving this problem with CAIA’s one.