The Mathematical Intelligencer

, Volume 23, Issue 1, pp 9–15 | Cite as

“Russian killer” no. 2: A challenging geometric theorem with human and machine proofs

  • Xiaorong Hou
  • Hongbo Li
  • Dongming Wang
  • Lu Yang


In February 1998 Sergey Markelov [71 from the Moscow Center for Continuous Mathjematics Education sent a set of five geometric theorems to Dongming Wang for testing the capability of his GEOTHER package [8], with the aim of presenting a challenge to computer provers to prove really hard theorems. These theorems have been


Theorem Prove Mathematical Intelligencer Clifford Algebra Automate Reasoning Geometric Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Ekhad, S.B.: Plane geometry: An elementary school textbook (ca. 2050 AD).The Mathematical Intelligencer 21/3: 64–70 (1999).CrossRefMATHMathSciNetGoogle Scholar
  2. [2]
    Fèvre, S., Wang, D.: Proving geometric theorems using Clifford algebra and rewrite rules. In: Proc. CADE-15 (Lindau, Germany, July 5-10, 1998),LNA1 1421, pp. 17–32 (1998).Google Scholar
  3. [3]
    Hestenes, D., Sobczyk, G.:Clifford algebra to geometric calculus. D. Reidel, Dordrecht Boston (1984).CrossRefGoogle Scholar
  4. [4]
    Gao, X.-S.: Transcendental functions and mechanical theorem proving in elementary geometries.J. Automated Reasoning 6: 403–417 (1990).CrossRefMATHGoogle Scholar
  5. [5]
    Li, H.: Vectorial equations solving for mechanical geometry theorem proving.J. Automated Reasoning 25: 83–121 (2000).CrossRefMATHGoogle Scholar
  6. [6]
    Li, H., Cheng, M.: Clifford algebraic reduction method for automated theorem proving in differential geometry.J. Automated Reasoning 21: 1–21 (1998).CrossRefMathSciNetGoogle Scholar
  7. [7]
    Markelov, S.: Geometry solver. E-mail communication of February 11, 1998 from ( Scholar
  8. [8]
    Wang, D.: GEOTHER: A geometry theorem prover. In: Proc. CADE-13 (New Brunswick, USA, July 30-August 3, 1996),LNAI 1104, pp. 166–170 (1996).Google Scholar
  9. [9]
    Wang, D.: Clifford algebraic calculus for geometric reasoning with application to computer vision. In: Automated deduction in geometry (Wang, D., ed.),LNAI 1360, pp. 115–140 (1997).Google Scholar
  10. [10]
    Wu, W.-T: Some recent advances in mechanical theorem-proving of geometries. In: Automated theorem proving: After 25 years (Bledsoe, W.W., Loveland, D.W., eds.),Contemp. Math. 29, pp. 235–241 (1984).Google Scholar
  11. [11]
    Wu, W.-t.:Mechanical theorem proving in geometries: Basic principles. Springer, Wien, New York (1994).CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media, Inc. 2001

Authors and Affiliations

  • Xiaorong Hou
    • 1
  • Hongbo Li
    • 2
  • Dongming Wang
    • 3
  • Lu Yang
    • 4
  1. 1.Chengdu Institute of Computer ApplicationsAcademia SinicaChengduChina
  2. 2.Institute of Systems ScienceAcademia SinicaBeijingChina
  3. 3.Laboratoire d’Informatique de Paris 6Université Pierre et Marie Curie-CNRSParis Cedex 05France
  4. 4.Chengdu Institute of Computer ApplicationsAcademia SinicaChengduChina

Personalised recommendations