Skip to main content
2 of 2
Clarified language.
Joseph O'Rourke
  • 150.8k
  • 36
  • 358
  • 958

This is somewhat tangential to your specific query, but perhaps not entirely irrelevant. There has been considerable progress in the subdomain of geometry theorems, some of whose provers proceed by searching for and eliminating possible counterexamples. I am no expert, but permit me to cite three references, separated by about a decade each, to indicate the continued progress in this subarea:

1988: Chou, Shang-Ching. Mechanical geometry theorem proving. Vol. 41. Springer, 1988. (Springer link)
   GaussPoint
   p.109: Five Gauss lines are concurrent: A "possibly new theorem" [in 1988].

2001: Jacques Fleuriot. "Geometry Theorem Proving." 2001, pp 11-30. A survey. (Springer link)

2011: Stojanović, Sana, Vesna Pavlović, and Predrag Janičić. "A coherent logic based geometry theorem prover capable of producing formal and readable proofs." Automated Deduction in Geometry. Springer Berlin Heidelberg, 2011. 201-220. (Springer link)


    ![Geometries][5]
      Ulrik Buchholtz talk [slides PDF download][6], 2010.
Joseph O'Rourke
  • 150.8k
  • 36
  • 358
  • 958