GenesisGeo: Technical Report
This advances automated reasoning for complex geometry problems, with potential applications in education and AI research, though it builds incrementally on existing neuro-symbolic methods.
The researchers tackled automated theorem proving in Euclidean geometry by creating GenesisGeo, which solves 24 of 30 IMO silver medal-level problems with a single model and 26 with an ensemble, while accelerating the symbolic engine DDARN by 120x and releasing a dataset of 21.8 million problems.
We present GenesisGeo, an automated theorem prover in Euclidean geometry. We have open-sourced a large-scale geometry dataset of 21.8 million geometric problems, over 3 million of which contain auxiliary constructions. Specially, we significantly accelerate the symbolic deduction engine DDARN by 120x through theorem matching, combined with a C++ implementation of its core components. Furthermore, we build our neuro-symbolic prover, GenesisGeo, upon Qwen3-0.6B-Base, which solves 24 of 30 problems (IMO silver medal level) in the IMO-AG-30 benchmark using a single model, and achieves 26 problems (IMO gold medal level) with a dual-model ensemble.