Skip to main content
SpringerLink
Log in

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

  • Article
  • Published:
The Mathematical Intelligencer Aims and scope Submit manuscript

Abstract

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

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Ekhad, S.B.: Plane geometry: An elementary school textbook (ca. 2050 AD).The Mathematical Intelligencer 21/3: 64–70 (1999).

    Article  MATH  MathSciNet  Google Scholar 

  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. Hestenes, D., Sobczyk, G.:Clifford algebra to geometric calculus. D. Reidel, Dordrecht Boston (1984).

    Book  Google Scholar 

  4. Gao, X.-S.: Transcendental functions and mechanical theorem proving in elementary geometries.J. Automated Reasoning 6: 403–417 (1990).

    Article  MATH  Google Scholar 

  5. Li, H.: Vectorial equations solving for mechanical geometry theorem proving.J. Automated Reasoning 25: 83–121 (2000).

    Article  MATH  Google Scholar 

  6. Li, H., Cheng, M.: Clifford algebraic reduction method for automated theorem proving in differential geometry.J. Automated Reasoning 21: 1–21 (1998).

    Article  MathSciNet  Google Scholar 

  7. Markelov, S.: Geometry solver. E-mail communication of February 11, 1998 from (markelov@dnttm.ru).

  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. 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. 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).

  11. Wu, W.-t.:Mechanical theorem proving in geometries: Basic principles. Springer, Wien, New York (1994).

    Book  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Chengdu Institute of Computer Applications, Academia Sinica, 610041, Chengdu, China

    Xiaorong Hou

  2. Institute of Systems Science, Academia Sinica, 100080, Beijing, China

    Hongbo Li

  3. Laboratoire d’Informatique de Paris 6, Université Pierre et Marie Curie-CNRS, 4 place Jussieu, 75252, Paris Cedex 05, France

    Dongming Wang

  4. Chengdu Institute of Computer Applications, Academia Sinica, 610041, Chengdu, China

    Lu Yang

Authors
  1. Xiaorong Hou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hongbo Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Dongming Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lu Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hou, X., Li, H., Wang, D. et al. “Russian killer” no. 2: A challenging geometric theorem with human and machine proofs. The Mathematical Intelligencer 23, 9–15 (2001). https://doi.org/10.1007/BF03024512

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF03024512

Keywords

Search

Navigation