Researchers have built an AI system that solves and proves geometry problems at Olympiad level, using far less computing power than rivals.
The system, called Euclid-Omni, pairs a symbolic geometry solver named Euclidea with large language models and vision-language models. Euclidea generates its own reasoning steps through deductive inference and algebraic computation, rather than leaning purely on pattern-matching. The team built a pipeline that uses Euclidea to synthesize geometry problems, render diagrams, and translate the solutions into natural language, producing large training datasets. Vision-language models trained on that synthetic data outperformed prior systems on calculation-style problems, while language models paired with Euclidea matched state-of-the-art systems on Olympiad-level proving problems.
Geometry is a good stress test for AI reasoning because it demands three things at once: reading a diagram, applying formal logic, and doing algebra - most systems handle one of those well, not all three. Euclid-Omni's trick is generating its own synthetic training data from a symbolic solver instead of scraping human-written proofs, which let it reach competitive results with orders of magnitude less compute and training data than typical large-scale runs.
It's a reminder that clever data generation can sometimes beat brute-force scale - though geometry's tidy axioms are a far easier target than the messier reasoning tasks AI still struggles with.