Autoformalizing Euclidean Geometry

Understand

Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable.

• Euclidean geometry provides an interesting and controllable domain for studying autoformalization.
• In this paper, we introduce a neuro-symbolic framework for autoformalizing Euclidean geometry, which combines domain knowledge, SMT solvers, and large language models (LLMs).
• One challenge in Euclidean geometry is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize.