AlphaGeometry is a neuro-symbolic theorem prover for Euclidean plane geometry that solves 25 out of 30 olympiad-level problems, outperforming previous methods and approaching the performance of an average International Mathematical Olympiad (IMO) gold medalist. It generates human-readable proofs and solves all geometry problems in the IMO 2000 and 2015 under expert evaluation, and discovers a generalized version of a translated IMO theorem from 2004. The system avoids the need for human demonstrations by synthesizing millions of theorems and proofs across varying complexities. It uses a neural language model trained on synthetic data to guide a symbolic deduction engine through complex problem-solving, with the language model focusing on auxiliary constructions during proof search. AlphaGeometry uses a combination of symbolic deduction and language modeling to solve geometry problems. It generates synthetic data by sampling random theorem premises and using a symbolic deduction engine to derive conclusions. The system then uses a language model to generate auxiliary constructions, which are then used by the symbolic engine to deduce new statements. This process is repeated until a solution is found. The system is trained on 100 million synthetic theorems and proofs, many with over 200 proof steps, and is capable of solving complex geometry problems that were previously difficult for automated systems. The system outperforms existing methods, including computer algebra and search-based approaches, by using a combination of symbolic deduction and language modeling. It is able to solve 25 out of 30 olympiad-level problems, with the previous state-of-the-art method solving only 10. AlphaGeometry also solves a range of geometry problems from the IMO, including the 2015 problem, which requires the use of auxiliary constructions. The system's performance is evaluated by human experts, who find that AlphaGeometry's proofs are readable and accurate. The system's success is due to its ability to generate synthetic data and learn to solve the key challenge of auxiliary construction in geometry. It uses a neural language model trained on synthetic data to generate auxiliary constructions, which are then used by the symbolic engine to deduce new statements. This approach allows the system to solve complex geometry problems without the need for human demonstrations. The system's performance is evaluated on a test set of 30 geometry problems, with AlphaGeometry solving 25 of them. The system's success demonstrates the potential of neuro-symbolic approaches in solving complex mathematical problems.AlphaGeometry is a neuro-symbolic theorem prover for Euclidean plane geometry that solves 25 out of 30 olympiad-level problems, outperforming previous methods and approaching the performance of an average International Mathematical Olympiad (IMO) gold medalist. It generates human-readable proofs and solves all geometry problems in the IMO 2000 and 2015 under expert evaluation, and discovers a generalized version of a translated IMO theorem from 2004. The system avoids the need for human demonstrations by synthesizing millions of theorems and proofs across varying complexities. It uses a neural language model trained on synthetic data to guide a symbolic deduction engine through complex problem-solving, with the language model focusing on auxiliary constructions during proof search. AlphaGeometry uses a combination of symbolic deduction and language modeling to solve geometry problems. It generates synthetic data by sampling random theorem premises and using a symbolic deduction engine to derive conclusions. The system then uses a language model to generate auxiliary constructions, which are then used by the symbolic engine to deduce new statements. This process is repeated until a solution is found. The system is trained on 100 million synthetic theorems and proofs, many with over 200 proof steps, and is capable of solving complex geometry problems that were previously difficult for automated systems. The system outperforms existing methods, including computer algebra and search-based approaches, by using a combination of symbolic deduction and language modeling. It is able to solve 25 out of 30 olympiad-level problems, with the previous state-of-the-art method solving only 10. AlphaGeometry also solves a range of geometry problems from the IMO, including the 2015 problem, which requires the use of auxiliary constructions. The system's performance is evaluated by human experts, who find that AlphaGeometry's proofs are readable and accurate. The system's success is due to its ability to generate synthetic data and learn to solve the key challenge of auxiliary construction in geometry. It uses a neural language model trained on synthetic data to generate auxiliary constructions, which are then used by the symbolic engine to deduce new statements. This approach allows the system to solve complex geometry problems without the need for human demonstrations. The system's performance is evaluated on a test set of 30 geometry problems, with AlphaGeometry solving 25 of them. The system's success demonstrates the potential of neuro-symbolic approaches in solving complex mathematical problems.