All in all, the explanation given for CAIA’s solution of the Saint-Exupéry problem is very simple. It includes only two important choices: what disjunction for the backtrack, and what value for L. For all the other steps of its proof, CAIA uses a combinatorial method: it applies every of its mathematical rules that can be executed, and it examines the result. Either it removes this result because it does not seem interesting (and this step never appears in the explanation), or it keeps it for later use with its mathematical rules (and it appears in the explanation only if it is used). For the simplest kind of meta-explanation, it is sufficient to indicate the deduction rules appearing in the explanation: their conditions indicate why they could be executed.
For instance, in the proof given in Part 1, one applies to constraint [3] a rule that leads to the disjunction [22]. To do that, CAIA seeks information on the possible power of a prime N in the factorization for every variable: V is not a multiple of N, or V may be a multiple of N, of N2, but not of N3, and so on. P, which is prime, is in our problem either odd or a multiple of 2, but not of 4. It considers the combinations of these values for all the variables of the constraint that do not give a false result. It tries it for N=2 (which gives [22]), 3, and 5. The conditions of this rule indicate that is applied to equality constraints with at most 3 variables and a degree greater than one. For N=3 or 5, this gives no useful result for the Saint-Exupéry’s problem. Therefore it does not appear in the explanation.
The same rule will be also applied with N=2 to constraint [2], which satisfies the necessary conditions. In the various branches, it shows that P=2, in [34], [70], and [101].
The generation of disjunctions, and the choice of one disjunction when it decides to backtrack are important for the success and the simplicity of the proof. However, it often has consequences only on the quality of the proof, rather than on the existence of the proof. For Saint-Exupéry, CAIA found twelve disjunctions before backtracking. When CAIA chooses any of them, it always finds the solutions. The difference is in the size of the tree: with the chosen disjunction, the tree has 4 leaves. It has 11 leaves for the worst case, when it uses the following disjunction:
P≡4 (mod 5) OR P≡3 (mod 5) OR P≡2 (mod 5) OR P≡1 (mod 5) OR P=5
We can notice that another aspect could be added to meta-explanations: why one has found the result quickly? Many derivations can be made, and it is better to make first those that are most likely to succeed. CAIA knows why it has given a high or a low priority to a deduction, but I did not include its reasons in the present meta-explanation: this would complicate it too much, and it would not be easy to give CAIA the ability to create such a kind of meta-explanation.
One could also add another possibility to a meta-explanation: present some derivations that have been made, that it was reasonable to try and which fail. For other problems, this could lead to the solution. One would have Why not? meta-explanations. It could be good for the students, encouraging them to add such method to their tools, and helping them to define more accurately when it is useful.
Therefore, it is possible to associate to each step of a solution a meta-explanation that indicates why one has considered this step. This is essential for teaching mathematics: the student must learn how one can find a proof. Unfortunately, this step is often missing in the teaching of mathematics. As a result, many students believe that one must have a gift to do mathematics. As they believe that they are not gifted, they do not even try to find the solution.
However, it is a difficult task for a mathematician to indicate why they have found a proof, such as Poincaré, who had an illumination while he boarded a train for Coutances, but he did not know why. The unconscious plays a significant role in the discovery, and we do not know why we have considered the key of a proof.
AI systems may have a huge advantage on us. Certainly, as for the Saint-Exupéry problem, it does not always find a solution as subtle as the one found by a mathematician. However, this solution may be easier to understand, and one can meta-explain it more easily. With little effort, it would be possible that CAIA creates the meta-explanations by itself.
AI systems have a huge advantage over ourselves: one can manage to design them so that there are conscious of the reasons of their acts far better than ourselves. Consciousness is an important reason why we are more clever than animals; therefore, meta-explanation is an extraordinary source of improvement for future AI systems.
However, solving problems is only a part of the activities of a mathematician. For the present time, CAIA is not able to do most of them for instance, receiving the description of a new theory, and trying to find interesting results in this theory. I began working on this problem 60 years ago, for my thesis. For the present time, CAIA cannot do it.