A Look into AlphaGeometry

Automated theorem proving represents a longstanding challenge in Artificial Intelligence research, in particular within the domain of Euclidean geometry, where the scarcity of training data and the difficulty of translating human proofs into formally verifiable languages have historically impeded the progress of learning-based methods. This thesis analyzes AlphaGeometry, a neuro-symbolic system developed by DeepMind in 2023 that achieved remarkable results in solving Euclidean geometry problems, producing proofs in a human-readable language. AlphaGeometry combines two components that operate iteratively: a symbolic deduction engine and a neural language model. The symbolic engine performs logical and algebraic deductions, while the neural language model proposes auxiliary geometric constructions whenever the symbolic reasoning process cannot reach a conclusion. Its most innovative feature lies in the creation of a fully synthetic dataset of over 100 million theorems and proofs, generated without translating any human-written results, effectively overcoming the traditional data scarcity problem. Through the analysis of its architecture, training process, and performance across problems of varying difficulty, this study highlights how AlphaGeometry established a new state of the art in automated geometric theorem proving, achieving performance comparable to that of an International Mathematical Olympiad (IMO) Silver medalist.