Abstract:  Mathematical theorem proving has long been a goal in artificial intelligence (AI), but progress has been slow due to the scarcity of human-generated proofs that can be translated into machine-readable formats. Geometry, in particular, poses unique challenges due to the difficulty of representing geometric figures and relations in a symbolic format that machines can easily process. Researchers at Google DeepMind have recently proposed a novel architecture, AlphaGeometry, which utilizes a neuro-symbolic approach. This system integrates a neural language model trained on a large corpus of synthetic theorems and proofs with a symbolic reasoning engine that ensures logical deductive correctness. On the IMO-AG-30 benchmark, AlphaGeometry achieved remarkable accuracy, solving 25 out of 30 problems, nearly matching the gold medalist benchmark of 25.9/30. In this talk, I will provide an overview of the construction and integration of the symbolic reasoning engine and the neural language model in AlphaGeometry. Specifically, I will detail how the symbolic reasoning engine, comprising the Deductive Database (DD) and Algebraic Reasoning (AR), operates. The DD manages formal geometric deductions by applying predefined theorems and axioms, while AR complements this by resolving complex algebraic expressions inherent in geometric proofs. Furthermore, I will explain the Neural Language Model utilized in AlphaGeometry, highlighting how it differs from known large language models such as GPT-4. This comparison will shed light on the potential of general-purpose language models in solving mathematical problems, offering insights into the broader capabilities of large language models in Math.