Nico Van Cleemput at Ghent University has been working on a program that can make conjectures about any Sage object-type (or any user-added type). It is currently being tested and then it will be included in Sage!
The conjectures have the form of an inequality between invariants of the object. The user specifies the invariant of interest, other invariants that are allowed to appear in expressions, the objects the program “knows” about, and the kind of inequality (<=,>=,<, or >). The produced conjectures are guaranteed to be true for all of the user-supplied objects.
Here’s an example. I am interested in the distribution pi(n) of primes up to n. I want upper bounds in terms of phi(n), the sum of the divisors of n, the number of base-10 digits of n, and the number of divisors of n. I initially give the program just the numbers 5,15, and 25 to calculate data about.
Here’s the input to the program:
invariants = [prime_pi, euler_phi, digits10, sum_divisors, count_divisors]
objects = [5, 15, 25]
Here’s the output from the program:
pi <= ((phi) – 1)
pi <= ((count_divisors) ^ 2)
pi <= ((phi) – (digits10))
The program can use any conjecture-making heuristic. These conjectures were made using Fajtlowicz’s Dalmatian heuristic.
I expect this to be huge, and to go way beyond mathematics. I think humans are conjecture-making machines, that all sorts of intelligent behaviors can be modeled by making conjectures, acting using these conjectures as constraints, modifying conjectures in the face of contradictory incoming data, revising the conjectures, and then iterating. (I gave one example in this 2005 paper).