Solving olympiad geometry without human demonstrations.

ABSTRACT: Proving mathematical theorems at the olympiad level represents a notable milestone in human-level automated reasoning^1-4, owing to their reputed difficulty among the world's best talents in pre-university mathematics. Current machine-learning approaches, however, are not applicable to most mathematical domains owing to the high cost of translating human proofs into machine-verifiable format. The problem is even worse for geometry because of its unique translation challenges^1,5, resulting in severe scarcity of training data. We propose AlphaGeometry, a theorem prover for Euclidean plane geometry that sidesteps the need for human demonstrations by synthesizing millions of theorems and proofs across different levels of complexity. AlphaGeometry is a neuro-symbolic system

SUBMITTER: Trinh TH 

PROVIDER: S-EPMC10794143 | biostudies-literature | 2024 Jan

REPOSITORIES: biostudies-literature