37
$\begingroup$

There are notable examples of computers "proving" results discovered by mathematicians, what about the opposite:

Are there interesting conjectures "discovered" by computers and proved by humans?

Possible example in graph theory is "Some Conjectures of Graffiti.pc (2004-07)," suggested by Joseph O'Rourke in another answer.

The question might not be well defined because "discovered" is controversial.

Added This question may be a duplicate (or refinement) of (2) in Experimental Mathematics as Kristal Cantwell pointed out.

I am mainly interested in examples where the program is designed to make conjectures which are not known identities to the program and later proved.

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ A related MO question: mathoverflow.net/questions/28651/… $\endgroup$
    – Andrey Rekalo
    Commented Mar 25, 2012 at 11:44
  • 4
    $\begingroup$ Several of the 26 finite sporadic simple groups were first constructed on computer, and only later proved to exist without a help of computer. Does this qualify? $\endgroup$
    – Dima Pasechnik
    Commented Mar 25, 2012 at 13:48
  • 1
    $\begingroup$ It might be more revealing to talk about how presentation of data leads to insight. The result mentioned here mathoverflow.net/questions/11885/… occurred because the program Roger wrote displayed results in a certain lexicographic order. Since then I have often wondered on automated ways of rearranging and displaying data to allow conjectures to be formed. Gerhard "Ask Me About System Design" Paseman, 2012.03.25 $\endgroup$
    – Gerhard Paseman
    Commented Mar 26, 2012 at 0:59
  • $\begingroup$ Gerhard, refined the question so the program must be designed to make conjectures as the Graffiti example. $\endgroup$
    – joro
    Commented Mar 26, 2012 at 6:19
  • $\begingroup$ fyi similar to tcs.se, "Where and how did computers help prove a theorem?" cstheory.stackexchange.com/questions/82/… $\endgroup$
    – vzn
    Commented Sep 20, 2012 at 17:23

12 Answers 12

Reset to default
22
$\begingroup$

Much of the early work on the Mandelbrot set was of this type. You see something strange in the computer images, then you try to prove that it really happens.

Here is one example: Pi and the Mandelbrot set. From conjecture in 1991 to paper in 2001.

Improve this answer
$\endgroup$
19
$\begingroup$

Lovasz told me the following interesting story. He had read a paper containing a long list of computer generated conjectures, did not like most them, but suddenly found one, which turned out to be an interesting and deep question. Then he realized that the same question had been asked earlier by humans. See http://oldwww.cs.elte.hu/~lovasz/berlin.pdf.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ The story is on pages 7-8 and footnote 2 of the paper? $\endgroup$
    – joro
    Commented Mar 25, 2012 at 14:53
  • $\begingroup$ Yes, exactly that one. $\endgroup$
    – Péter Komjáth
    Commented Mar 26, 2012 at 5:23
  • $\begingroup$ Link seems to no longer work. $\endgroup$
    – JoshuaZ
    Commented Jan 21 at 2:30
15
$\begingroup$

About 1960 Ed Lorenz observed the "sensitive dependence on initial conditions" in a very simple weather model he was running on a computer. He later coined the term "butterfly effect" for this phenomenon.

Improve this answer
$\endgroup$
14
$\begingroup$

The starting point of the mathematical theory of solitons for the Korteweg-de Vries equation was the numerical experiment of Kruskal and Zabusky in 1965, showing that solitons of different amplitudes, hence traveling at different speeds, crossed each other and reemerged (almost) undisturbed. I think this is an appropriate example in this thread, since this is an actual new phenomenon, totally unespected, discovered by computer simulation, then rigorously proved and widely generalized to constitute a whole new mathematical theory.

Improve this answer
$\endgroup$
12
$\begingroup$

This is not precisely a conjecture, but the Fermi-Pasta-Ulam experiment seems to be the first time mathematicians and physicists realized that lack of integrals of motion does not necessarily lead to chaos or ergodicity, thus paving the way for KAM theory.

Improve this answer
$\endgroup$
11
$\begingroup$

No one has mentioned the case of commutative algebra. The appearance of computer algebra systems allowed researchers in commutative algebra and/or algebraic geometry to generate lots of examples which then lead to conjectures, later proved by hand. Look at this quote from Eisenbud's home page, for instance:

"Ever since the early 70s I've used computers to produce examples in algebraic geometry and commutative algebra, and I've developed algorithms to extend the power of computation in this area. I recently joined Mike Stillman and Dan Grayson in the project to (further) develop the Macaulay2 system for symbolic computation. "

Improve this answer
$\endgroup$
2
  • $\begingroup$ Interesting. To what extent generation of conjectures is automated? $\endgroup$
    – joro
    Commented Mar 26, 2012 at 13:21
  • $\begingroup$ Ok, maybe this doesn't correspond exactly to what you wrote in the last gray box. It is to a rather primitive extent, since there should be some conjecture already. Then examples may be generated (which would be too lengthy/tedious to compute by hand) that could support or refute the conjecture. $\endgroup$
    – Camilo Sarmiento
    Commented Mar 26, 2012 at 14:41
9
$\begingroup$

In our paper The numerical measure of a complex matrix (Comm. Pure and Appl. Math. ,65 (2012), pp 287--336), T. Gallay and I proved that the restriction to some zones of the numerical density of an $n\times n$ matrix is polynomial of degree at most $n-3$. The only reason why we were led to this result is because of numerical experiments shown some evidence. Does it qualify ?

Later on, we found that this polynomiality is related to the so-called lacunas for hyperbolic differential operators.

Improve this answer
$\endgroup$
0
9
$\begingroup$

In Automated conjecture making in number theory using HR, Otter and Maple, the HR program discovered the following conjecture:

Paraphrased,... if you take an integer and add up the divisors, then if the result is a prime, the number of divisors you have just added up will also be prime

And formally:

all a (isprime(sigma(a)) -> isprime(tau(a)))

Where sigma(a) and tau(a) are the sum of the divisors of a, and the number of divisors of a, respectively.

They then proved that this conjecture is true. To me this seems very interesting and non-obvious. But I have no idea if this theorem is significant, or if it was totally unknown before this program discovered it.

EDIT: I'm told that specific conjecture might not be particularly interesting to mathematicians. Here are some more conjectures the program discovered, from that paper:

It conjectured (and then the author proved) that sum of the divisors of square numbers is always odd, i.e.:

issquare(a) → odd(σ (a))

Probably not new either, but still cool that it was automatically discovered.

The program also discovered (invented?) a new concept called "refactorable numbers", and then made some surprising and interesting conjectures about this new concept:

HR invented the concept of refactorable numbers, which are such that the number of divisors is itself a divisor, e.g., 9 is refactorable, because 9 has three divisors (1, 3 and 9) and 3 divides 9.

...

This left us with 26 open conjectures, which we present in Appendix C. We have not yet fully investigated these remaining conjectures, and it seems likely that the majority may be false. Of particular interest to us are the conjectures about refactorable numbers: amongst others, HR made the conjectures that: (i) for even numbers, if σ (a) is refactorable, then τ (a) and σ (a) will be even, (ii) for odd numbers, if σ (a) is even and refactorable, then τ (τ (a)) and σ (τ (a)) will both be prime, (iii) if τ (a) is refactorable and τ (τ (a)) is prime, then σ (τ (a)) will also be prime, and (iv) if both σ (a) and σ (σ (a)) are refactorable, then τ (σ (a)) will be refactorable and σ (τ (a)) will be odd.

The author has a number of other papers on this program and things it's discovered. I'm just now reading through Automatic Invention of Integer Sequences, where they claim it invented 17 novel integer sequences that were accepted into OEIS. Including the refactorable numbers mentioned above.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Even if not obvious, this is quite a simple theorem: since $\sigma(n)$ is multiplicative, $n$ must be a prime power $p^k$ and $\sigma(p^k)=(p^{k+1}-1)/(p-1)$. If $\tau(p^k)=k+1$ had a nontrivial divisor $m$, then $\sigma(p^k)$ would have a nontrivial divisor $(p^m-1)/(p-1)$. $\endgroup$
    – Wojowu
    Commented May 1, 2016 at 8:28
  • 3
    $\begingroup$ I think it's not that interesting if you understand multiplicative functions. $\endgroup$
    – Douglas Zare
    Commented May 1, 2016 at 8:29
  • $\begingroup$ @Wojowu Sorry, I have no education in number theory. I'm reading these papers because of my interest in AI and automated conjecture making. I edited my post to include more examples from the paper, which are perhaps more interesting. $\endgroup$
    – Houshalter
    Commented May 2, 2016 at 7:22
  • $\begingroup$ @DouglasZare see last comment. $\endgroup$
    – Houshalter
    Commented May 2, 2016 at 7:22
8
$\begingroup$

One problem that perhaps fits in this category is the exact solution of the hard hexagon model by Rodney Baxter. In this case computer calculations revealed surprising patterns which suggested that the model was solvable, but it required someone like Rodney Baxter to first recognise these patterns, and then go ahead and find the solution. A large grey area in the nature of the question is the extent to which the computer "discovered" the solution.

This discovery is described in Ch. 14 of Rodney Baxter's book "Exactly Solved Models in Statistical Mechanics".

There must be other examples of computer discoveries in the field of solvable models in statistical mechanics, as to some extent this is the nature of field. However, to me this example stands out, as to the best of my knowledge there was no a priori expectation that the model was solvable before the computer calculations were performed.

Improve this answer
$\endgroup$
5
$\begingroup$

You seem to be asking about computers formulating conjectures later proved by humans. As one not having had much exposure to the issue, I wonder how to teach a computer (maybe with some form of heuristics?) assessing it has found a plausible conjecture: in this case computer misses the comfort of knowing a result is true for it has proven it's true, while human mathematicians can use instinct or some kind of common sense. However, I found this:

A Symbolic Finite-State Approach For Automated Proving of Theorems in Combinatorial Game Theory

Improve this answer
$\endgroup$
0
5
$\begingroup$

I agree that it may be difficult to program a computer to find conjectures which it can't then prove, but can then be proven by humans. Much easier seems to be to find and prove theorems, or to search for counterexamples to conjectures.

That's why I am thinking at another possibility: explore mathematical constructions using computer programs, and from the observed patterns and regularities, suggest conjectures. So, not the program will be the one which suggest the conjecture, but he human user. Exploring mathematical constructions is done in experimental mathematics. On this Wikipedia page there are some examples of patterns observed when using numerical and graphical simulations, under the titles "Finding serendipitous numerical patterns" and "Visual investigations".

Improve this answer
$\endgroup$
4
$\begingroup$

There is a related question on experimental mathematics here.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thank you, haven't seen this question. This one may be a duplicate/refinement of 2). $\endgroup$
    – joro
    Commented Mar 26, 2012 at 5:54

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .