Synthesis of Geometry Proof Problems


  • Chris Alvin Louisiana State University, Baton Rouge
  • Sumit Gulwani Microsoft Research
  • Rupak Majumdar Max Planck Institute for Software Systems
  • Supratik Mukhopadhyay Louisiana State University, Baton Rouge



Problem Synthesis, Automated Reasoning, Computer-Aided Education, Interesting Problem, Complete Problem


This paper presents a semi-automated methodology for generating geometric proof problems of the kind found in a high-school curriculum. We formalize the notion of a geometry proof problem and describe an algorithm for generating such problems over a user-provided figure. Our experimental results indicate that our problem generation algorithm can effectively generate proof problems in elementary geometry. On a corpus of 110 figures taken from popular geometry textbooks, our system generated an average of about 443 problems per figure in an average time of 4.7 seconds per figure.




How to Cite

Alvin, C., Gulwani, S., Majumdar, R., & Mukhopadhyay, S. (2014). Synthesis of Geometry Proof Problems. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1).