PyEuclid: A Versatile Formal Plane Geometry System in Python

Abstract

Abstract We introduce , a unified and versatile Python-based formal system for representing and reasoning about plane geometry problems. 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, enables human-like reasoning and supports generating concise reasoning steps (proofs), either fully automatically or through interactive guidance. Benchmark evaluations demonstrate that outperforms existing tools, solving a broader range of problems across both proof generation and calculation tasks. Moreover, holds significant potential for educational use and integration with advanced deep learning systems.