Interesting conjectures "discovered" by computers and proved by humans? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-19T17:15:34Z http://mathoverflow.net/feeds/question/92148 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans Interesting conjectures "discovered" by computers and proved by humans? joro 2012-03-25T09:26:33Z 2012-03-26T12:56:20Z <p>There are notable examples of computers "proving" results discovered by mathematicians, what about the opposite:</p> <blockquote> <p>Are there interesting conjectures "discovered" by computers and proved by humans?</p> </blockquote> <p>Possible example in graph theory is "<a href="http://www.math.uiuc.edu/~west/regs/graffiti.html" rel="nofollow">Some Conjectures of Graffiti.pc (2004-07)</a>," suggested by Joseph O'Rourke <a href="http://mathoverflow.net/questions/87114/87128#87128" rel="nofollow">in another answer</a>.</p> <p>The question might not be well defined because "discovered" is controversial.</p> <p><strong>Added</strong> This question may be a duplicate (or refinement) of (2) in <a href="http://mathoverflow.net/questions/12085/experimental-mathematics" rel="nofollow">Experimental Mathematics</a> as Kristal Cantwell pointed out.</p> <blockquote> <p>I am mainly interested in examples where the program is <em>designed to make conjectures</em> which are not known identities to the program and later proved.</p> </blockquote> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92149#92149 Answer by Marco Caminati for Interesting conjectures "discovered" by computers and proved by humans? Marco Caminati 2012-03-25T09:55:47Z 2012-03-25T10:09:55Z <p>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:</p> <p><a href="http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/tf1.html" rel="nofollow">A Symbolic Finite-State Approach For Automated Proving of Theorems in Combinatorial Game Theory</a></p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92152#92152 Answer by Cristi Stoica for Interesting conjectures "discovered" by computers and proved by humans? Cristi Stoica 2012-03-25T10:15:05Z 2012-03-25T10:15:05Z <p>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.</p> <p>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 <strong>experimental mathematics</strong>. On <a href="http://en.wikipedia.org/wiki/Experimental_mathematics" rel="nofollow">this Wikipedia page</a> there are some examples of patterns observed when using numerical and graphical simulations, under the titles "Finding serendipitous numerical patterns" and "Visual investigations".</p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92156#92156 Answer by Ralph for Interesting conjectures "discovered" by computers and proved by humans? Ralph 2012-03-25T11:44:16Z 2012-03-25T23:30:32Z <p>I agree with the preceding answers that a computer seldom says "I conjecture ... but I can't prove it". But there a results found by computers that were later on proved by humans to have some particular property or that were generalized by humans: </p> <p>McCune found with help of a computer the single-axiom in products and inverses for groups: </p> <p>$$x \cdot (y \cdot (((z \cdot z^{-1})\cdot (u \cdot y)^{-1}) \cdot x))^{-1} = u$$</p> <p>Later it was proved by Kunen (by hand and with computer) that there is no shorter axiom in terms of products and inverses. More on this can be found in the <a href="http://www.mcs.anl.gov/uploads/cels/papers/P901.pdf" rel="nofollow">paper</a>. </p> <p>Similarly, Kunen and Hart showed that $$f_m(x,f_m(x,(x \cdot y)\cdot z)\cdot g_m(z)) = y$$ is a single-axiom for groups of exponent $2m+1$ where $f_m(x,y) = x(x(...(xy)...))$ and $g_m(z) = z \cdot (\cdots (z\cdot z)...)$. For small $m$ the formulas where found and proved by a computer and by analyzing the computer's proof, the general result was obtained and proved by humans. </p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92165#92165 Answer by Gerald Edgar for Interesting conjectures "discovered" by computers and proved by humans? Gerald Edgar 2012-03-25T13:09:12Z 2012-03-26T07:21:13Z <p>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. </p> <p>Here is one example: <a href="http://www.math.osu.edu/~edgar.2/piand.html" rel="nofollow">Pi and the Mandelbrot set</a>. From conjecture in 1991 to paper in 2001.</p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92170#92170 Answer by Denis Serre for Interesting conjectures "discovered" by computers and proved by humans? Denis Serre 2012-03-25T14:09:01Z 2012-03-26T11:40:13Z <p>In our paper <em>The numerical measure of a complex matrix</em> (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 ?</p> <p>Later on, we found that this polynomiality is related to the so-called <em>lacunas</em> for hyperbolic differential operators.</p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92171#92171 Answer by Péter Komjáth for Interesting conjectures "discovered" by computers and proved by humans? Péter Komjáth 2012-03-25T14:32:55Z 2012-03-25T14:32:55Z <p>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 <a href="http://oldwww.cs.elte.hu/~lovasz/berlin.pdf" rel="nofollow">http://oldwww.cs.elte.hu/~lovasz/berlin.pdf</a>. </p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92184#92184 Answer by alvarezpaiva for Interesting conjectures "discovered" by computers and proved by humans? alvarezpaiva 2012-03-25T18:09:13Z 2012-03-25T18:21:28Z <p>This is not precisely a conjecture, but the <a href="http://en.wikipedia.org/wiki/Fermi%25E2%2580%2593Pasta%25E2%2580%2593Ulam_problem" rel="nofollow">Fermi-Pasta-Ulam experiment</a> 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.</p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92185#92185 Answer by Piero D'Ancona for Interesting conjectures "discovered" by computers and proved by humans? Piero D'Ancona 2012-03-25T18:28:52Z 2012-03-25T18:28:52Z <p>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.</p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92187#92187 Answer by Kristal Cantwell for Interesting conjectures "discovered" by computers and proved by humans? Kristal Cantwell 2012-03-25T18:37:07Z 2012-03-25T18:37:07Z <p>There is a related question on experimental mathematics <a href="http://mathoverflow.net/questions/12085/experimental-mathematics" rel="nofollow">here</a>. </p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92189#92189 Answer by Gerald Edgar for Interesting conjectures "discovered" by computers and proved by humans? Gerald Edgar 2012-03-25T19:07:39Z 2012-03-25T19:07:39Z <p>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.</p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92205#92205 Answer by Nathan Clisby for Interesting conjectures "discovered" by computers and proved by humans? Nathan Clisby 2012-03-25T22:03:55Z 2012-03-25T22:03:55Z <p>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.</p> <p>This discovery is described in Ch. 14 of Rodney Baxter's book "Exactly Solved Models in Statistical Mechanics". </p> <p>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.</p> http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans/92260#92260 Answer by Camilo Sarmiento for Interesting conjectures "discovered" by computers and proved by humans? Camilo Sarmiento 2012-03-26T12:56:20Z 2012-03-26T12:56:20Z <p>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 <a href="http://www.msri.org/~de/" rel="nofollow">home page</a>, for instance:</p> <p>"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. "</p>