AlphaGeometry
DeepMind's AlphaGeometry is a theorem prover that solves Olympiad-level geometry problems at near gold-medallist performance, and crucially, without needing any human demonstrations.
Ask this paper
Symbolic + neural hybrid: Combines a neural language model that proposes useful auxiliary constructions with a fast symbolic deduction engine that performs the actual proof search.
Synthetic data at scale: Trained entirely on ~100M synthetically generated theorem-proof pairs, sidestepping the extreme scarcity of labeled olympiad-geometry data.
IMO-level results: Solves 25 of 30 recent IMO geometry problems, matching the average IMO gold medallist (25.9) and far surpassing the previous computational state-of-the-art (10).
Broader implication: Demonstrates that deep learning can be used as a "bridge" to suggest useful constructs for symbolic engines - a general recipe for neurosymbolic reasoning beyond geometry.