In plane geometry, it is customary to say that checking proofs is a mechanical process but that finding new theorems is a creative activity. Citing J. Hadamard, "logic only sanctions the conquests of intuition."

We have now computer programs that can check the correctness of geometric statements (at least first order statements) and interactive geometry softwares are used routinely in geometry classes to teach elementary geometry. We can use these programs to discover new theorems, but is there any program that is able to find new geometric statements on its own? More precisely,

Is there any new and interesting result in plane geometry that has been produced by a computer program without any human intervention?

The answer may state such a result together with the relevant reference.

Of course, the software is always made by humans, but the result output by the machine should not be known prior to the start of the program and no intervention should happen during the execution of the program. Also, new and interesting is subjective. By new, I mean some result that is not an easy corollary of some theorem prior to the XXIe century. By interesting, probably the real test would be to produce several results sufficiently different from each others to show creativity and fit the taste of the many geometers on mathoverflow.

  • 1
    $\begingroup$ Some keywords: Clark Kimberling's encyclopedia with its auto-calculated collinearities (I think they are only conjectured automatically on numerical evidence); June Lester's circle (not sure how much human intervention); Deko Dekov's journal of computer-generated results. My personal impression is that we could be using computers for far more than we are (even for AI-generated "nice" synthetic proofs), but people tend to prefer to solve things on their own. $\endgroup$ – darij grinberg Jun 20 '18 at 13:45
  • $\begingroup$ @darij. Thanks for the pointer to the journal. Grozdev-Dekov (2015) claim that the only program that has been able to discover new results in plane geometry is their own "Discoverer". Unfortunately, the software is not available and it seems that these results amount to building new points in the triangle by mating points from Kimberling's list using some well-known procedure. So, I am not convinced at the moment. $\endgroup$ – coudy Jun 20 '18 at 14:42
  • $\begingroup$ Yeah, all of these sources could be better -- synthetic geometry is a widely and easily accessible field; not everyone around is a professional. I'm just saying these things are there. $\endgroup$ – darij grinberg Jun 20 '18 at 18:08
  • 2
    $\begingroup$ It might help to define "without any human intervention." At the moment, a computer program won't run unless a human being types its name at the command line or double-clicks its icon. Computer programs are also written by human beings. Both of these involve "human intervention" at some level. This is not just a semantic quibble. A computer program has to be told by a human being to search for theorems, and the way the "search for theorems" is set up involves greater or lesser degrees of human intervention. $\endgroup$ – Timothy Chow Jun 20 '18 at 20:50

A new theorem discovered by computer prover (1989)

Concerning Pappus lines and Leisenring lines there exists a set of interesting theorems. Here we show that these theorems can be easily proved by our computer prover which is implemented on the basis of Wu's method for mechanical theorem proving in geometries. Using this prover we discovered, furthermore, a new theorem: The six intersection points of every Pappus line and its corresponding Leisenring line are collinear.

  • $\begingroup$ I don't think that the prover discovered the result by itself. As far as I know, a 1989 prover based on the Wu method is unable to produce any result without an human spelling out the desired output to the computer. $\endgroup$ – coudy Jun 20 '18 at 14:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.