PyEuclid: A Versatile Formal Plane Geometry System in Python
摘要
We introduce PyEuclid, a unified and versatile Python-based formal system for representing and reasoning about plane geometry problems. PyEuclid designs a new formal language that faithfully encodes geometric information, including diagrams, and integrates two complementary components to perform geometric reasoning: (1) a deductive database with an extensive set of inference rules for geometric properties, and (2) an algebraic system for solving diverse equations involving geometric quantities. By seamlessly combining these components, PyEuclid enables human-like reasoning and supports generating concise reasoning steps (proofs), either fully automatically or through interactive guidance. Benchmark evaluations demonstrate that PyEuclid outperforms existing tools, solving a broader range of problems across both proof generation and calculation tasks. Moreover, PyEuclid holds significant potential for educational use and integration with advanced deep learning systems.