Self-evident Automated Geometric Theorem Proving Based on Complex Number Identity

Authors：Peng, Xicheng; Zhang, Jingzhong; Chen, Mao^*; Liu, Sannyuya^*

Source：JOURNAL OF AUTOMATED REASONING, 2023, 67(4): 38.

DOI：10.1007/s10817-023-09688-w

• Complex number identity
• Self-evident automated proving
• Complex number geometry
• Geometric theorems
• Elimination method

How to automatically generate short and easy-to-understand proofs for geometric theorems has long been an issue of concern in mathematics education. A novel automated geometric theorem proving method based on complex number identities is proposed in this paper, which acts as a bridge between geometry and algebra. According to the proposed method, the geometric relations in the given proposition are first transformed into a complex number expression, then the complex number identity is generated by the elimination method; finally, the closure property under all four operations of real numbers is employed to prove the proposition. A test on more than 300 geometric problems shows that the proposed method is highly effective, and the corresponding proofs are short, with obvious geometric meaning.

• Institution
  广州大学