This is a short summary of the publication in Nature:
AlphaGeometry is a theorem prover for Euclidean plane geometry that uses a neural language model to guide a symbolic deduction engine through challenging problems. It synthesizes millions of theorems and proofs across different levels of complexity, sidestepping the need for human demonstrations.
AlphaGeometry outperforms the previous best method for solving olympiad-level geometry problems and produces human-readable proofs. It also discovers a generalized version of a translated IMO theorem in 2004.