The paper introduces AlphaGeometry, a theorem prover for Euclidean plane geometry that addresses the challenge of proving mathematical theorems at the olympiad level. Traditional machine learning approaches struggle with this task due to the high cost of translating human proofs into machine-verifiable formats, especially in geometry due to unique translation challenges and limited training data. AlphaGeometry overcomes these issues by synthesizing millions of theorems and proofs across different complexity levels, using a neuro-symbolic system that combines a neural language model and a symbolic deduction engine. The neural language model is trained on synthetic data generated from random theorem premises, allowing it to guide the symbolic deduction engine through infinite branching points in challenging problems. On a test set of 30 latest olympiad-level problems, AlphaGeometry solves 25 problems, outperforming the previous best method and approaching the performance of an average International Mathematical Olympiad (IMO) gold medalist. Notably, AlphaGeometry produces human-readable proofs and has successfully solved all geometry problems in the IMO 2000 and 2015 under human expert evaluation. The paper also discusses the challenges and limitations of current methods in geometry theorem proving, such as the scarcity of proof examples in general-purpose mathematical languages and the need for human-designed heuristics. AlphaGeometry's approach, which uses synthetic data and a neuro-symbolic framework, provides a promising solution to these challenges. The method is further demonstrated to be applicable to other mathematical domains facing similar data scarcity issues.The paper introduces AlphaGeometry, a theorem prover for Euclidean plane geometry that addresses the challenge of proving mathematical theorems at the olympiad level. Traditional machine learning approaches struggle with this task due to the high cost of translating human proofs into machine-verifiable formats, especially in geometry due to unique translation challenges and limited training data. AlphaGeometry overcomes these issues by synthesizing millions of theorems and proofs across different complexity levels, using a neuro-symbolic system that combines a neural language model and a symbolic deduction engine. The neural language model is trained on synthetic data generated from random theorem premises, allowing it to guide the symbolic deduction engine through infinite branching points in challenging problems. On a test set of 30 latest olympiad-level problems, AlphaGeometry solves 25 problems, outperforming the previous best method and approaching the performance of an average International Mathematical Olympiad (IMO) gold medalist. Notably, AlphaGeometry produces human-readable proofs and has successfully solved all geometry problems in the IMO 2000 and 2015 under human expert evaluation. The paper also discusses the challenges and limitations of current methods in geometry theorem proving, such as the scarcity of proof examples in general-purpose mathematical languages and the need for human-designed heuristics. AlphaGeometry's approach, which uses synthetic data and a neuro-symbolic framework, provides a promising solution to these challenges. The method is further demonstrated to be applicable to other mathematical domains facing similar data scarcity issues.