geometry_prove
Proves geometry theorems using symbolic reasoning. Input a problem in AG2 format and get proof status and deduction steps.
Instructions
Prove a geometry theorem using AlphaGeometry2's DDAR engine.
Input format (AG2 problem string):
Points with coordinates: "a@x_y = ;"
Constraints: "coll a b c" (collinear), "cong a b c d" (congruent), "perp a b c d" (perpendicular), "para a b c d" (parallel), "cyclic a b c d" (concyclic), "eqangle a b c d e f g h" (equal angles)
Goal after "?": "cong e p e q" (prove EP = EQ)
Example (IMO 2000 P1): "a@-0.52_0.11 = ; b@-0.19_0.19 = ; ... cong a g1 g1 m, ... ? cong e p e q"
Returns proof status and number of deduction steps.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| problem | Yes | Geometry problem in AG2 format |