I always believed that AI systems will become excellent mathematicians. Until now, AI focused its efforts on theorem proving, the most visible part of the mathematical activity. However, there are a lot of things to do other than proving theorems; one of them is to make conjectures, then he/she/it usually tries to prove it. This is not always the case, the main activity of EURISKO, developed by Douglas Lenat, was to make conjectures, which it did not prove. Ramanujan, a mathematician of genius, worked in an analogous manner: for many years after his death, distinguished mathematicians were still trying to prove some of his conjectures. Several conjectures are famous, such as Fermat’s last theorem that has been proved more than three centuries after it was stated. Goldbach suggested another well-known conjecture: any even integer greater than 2 can be written as the sum of two primes. Some conjectures, such as Riemann hypothesis, played a great role in the history of mathematics, theories have been developed in order to prove them.
In the February 2016 issue of Artificial Intelligence, C. Larson and N. Van Cleemput describe a system able to make conjectures in many mathematical domains. This system is not associated to a particular theory. Their work is based on a heuristic found and experimented since 1986 by S. Fajtlowicz. I did not know it, and this is not surprising, little was published about it: before this paper, it had never been referenced in Artificial Intelligence.
This heuristic may be used in many domains but not in all: the theory must include objects that have real number invariants, that are numbers linked to objects. For a graph, the invariants may be the number of vertices, of edges, the maximum degree of any of the vertices, etc. For a natural number, there are the number of factors, the number of distinct primes in its factorization, the number of its representations as sum of two primes, etc.
The system stores some objects of the theory under study; their number may be very low, for instance less than 10. For each object, it can find the value of all its invariants; therefore, it can check whether a new conjecture is true for all the given objects. The user indicates the name of an invariant I, for which he would like to conjecture the value of its lower or higher bound, using the other known invariants I1, I2, I3, …., In . The system knows a set of functions that can be applied to numbers such as addition, product, logarithm, etc. It will generate many conjectures such as C1 for I>I1+I2, C2 for I<=I1*I3, C3 for I<(I2-I4)², C4 for I>=log(I5+3),…The user may suggest other functions, especially those that are known to be useful in the present theory. In the different domains considered in the paper, it uses the following functions: frobenius norm, euler phi, mertens, next prime, and so on. This is the only situation in which the system is adapted to a particular domain.
When it has found a new conjecture, the system accepts it if it passes two tests:
Truth test: the conjecture is true for all the stored objects.
Significance test: for at least for one of the stored objects, the conjecture gives a stronger result than all the other known conjectures for the same object.
To clarify the interest of the second test, let us assume that we are looking for conjectures about the invariant G(n) when n is even: G(n) is the number of representations of n as sum of two primes. At the start, one has stored only two objects: 16 and 24. G(16)=2 (3+13 and 5+11) while G(24)=3 (5+19, 7+17, and 11+13). Conjecture C1 is: G(n) is greater than or equal to the number of digits in the binary representation of n less the number of its divisors. It is true for both objects: G(16)>=2 (5-3) and G(24)>=-1 (5-6). Now, conjecture C2 is: G(n) is greater than or equal to the number of digits of its decimal representation minus 1; this is also true since G(16)>=1 and G(24)>=1. However, C1 is stronger for 16 since it indicates that G(16)>=2 instead of 1 for C2; on the contrary, C2 is stronger for 24 where it predicts at least 1 instead of -1. Therefore, so far, one keeps both conjectures.
Naturally, finding a conjecture is not enough: one must prove it, and the conjecture must also be useful. For proving Goldbach conjecture (CG), that is G(n)>0 when n is even, one must find a new conjecture, which can be proved as a theorem, such that its value for G(n) is always at least 1. Even if C1 is true, it is not sufficient, since it only gives G(24)>-1. Therefore, it is certainly not a useful conjecture for proving CG, although it could give (if true) an interesting lower bound for some values of n. We are more lucky with C2: G is positive for both stored objects, and it has been also checked for many even numbers, but it has not yet been proved that the number of representations of n as sum of two primes is greater than or equal to the number of digits of n minus one. I give here only two very simple conjectures; the system found more of them, and checked them with much more than two stored objects. Perhaps, one day, it will find a conjecture predicting G(n)>0 that could be proved; then CG will also be proved.
The initial step in the research for a useful conjecture can be made with very few objects, then the system checks carefully that there is no trivial exception. For instance, after being discovered with few objects, conjecture C2 has been checked for n up to 1,000,000. After finding a useful and reasonably credible conjecture, a human or artificial mathematician has to prove it. Unfortunately, it may be impossible, even for a very clever artificial mathematician, to prove a conjecture because no proof exists although it is always true.
Anyway, I am impressed by the results from this system, particularly with conjecture C2. Firstly, this gives other ideas for proving CG; although it is much stronger, this could lead to consider new pathways. Moreover, if it is proved, it would be a satisfactory (although not very useful) result. For instance, C2 immediately states that:
G(1234567899876543210)>=18
which means that there exists at least 18 representations of this huge number as sum of two primes. With CG, we would only know that there is at least one representation. If I was a mathematician, I would be very proud if I could prove C2!
We can experiment this system, available at nvcleemp.github.io/conjecturing . Their program is implemented in the Sage open-source mathematical computing environment. Sage has a lot of built-in invariants for various mathematical objects. Therefore, it is easy to check with many instances, whether it is most likely that a promising conjecture is true.
This work does not solve all the problems linked to conjectures, but it shows that it is possible to add a new brick to the realization of what will someday be an artificial mathematician.