Formal foundations of AlphaGeometry: A Lean 4 mechanization

Beyond the Plane: Abstracting Away Geometry from AlphaGeometry Skip to main You are using an outdated browser. Please upgrade your browser to improve your experience. Published March 11, 2026 | Version v1 Preprint Open Beyond the Plane: Abstracting Away Geometry from AlphaGeometry Authors/Creators Bordg, Anthony (Project leader) Jafarrahmani, Farzad (Project member) Description While AlphaGeometry has achieved gold-medalist performance on International Mathematical Olympiad geometry problems, its success remains largely confined to a specialized domain. Developing a cross-domain successor requires that we first determine the underlying logical substrate of AlphaGeometry’s domain-specific language. In this paper, we identify and propose the logic of observation as a mathematically principled language designed to serve as AlphaGeometry's foundation. We present a formal implementation of this logic within the Lean 4 programming language. By explicitly embedding Euclidean geometry into this logic and providing a machine-checked proof of its soundness, we demonstrate how the reasoning patterns of specialized solvers can be generalized across a wide class of mathematical theories. Files AB_AlphaGeometry.pdf Files (213.7 kB) Name Size Download all AB_AlphaGeometry.pdf md5:b8578ef385a4d93a20c721ec22c629f9 213.7 kB Preview Download Additional details Related works Is supplemented by Preprint: 10.5281/zenodo.18961053 (DOI) 110 Views 9 Downloads Show more details All versions This version Views Total views 110 110 Downloads Total downloads 9 9 Data volume Total data volume 4.3 MB 4.3 MB More info on how stats are collected.... Versions External resources Indexed in OpenAIRE Communities Keywords and subjects EuroSciVoc Artificial intelligence Mathematical logic Machine learning Mathematics Details DOI DOI Badge DOI 10.5281/zenodo.18959740 Markdown [](https://doi.org/10.5281/zenodo.18959740) reStructuredText .. image:: https://zenodo.org/badge/DOI/10.5281/zenodo.18959740.svg :target: https://doi.org/10.5281/zenodo.18959740 HTML Image URL https://zenodo.org/badge/DOI/10.5281/zenodo.18959740.svg Target URL https://doi.org/10.5281/zenodo.18959740 Resource type Preprint Publisher Zenodo Rights License Creative Commons Attribution 4.0 International The Creative Commons Attribution license allows re-distribution and re-use of a licensed work on the condition that the creator is appropriately credited. Read more Citation Export Technical metadata Created March 11, 2026 Modified March 11, 2026 Jump up This site uses cookies. Find out more on how we use cookies Accept all cookies Accept only essential cookies