The program solved 25 geometry problems out of 30 from the International Mathematical Olympiad (IMO) under competition time limits—a performance almost as good as the average human gold medallist.
[4] Traditional geometry programs are symbolic engines that rely exclusively on human-coded rules to generate rigorous proofs, which makes them lack flexibility in unusual situations.
AlphaGeometry combines such a symbolic engine with a specialized large language model trained on synthetic data of geometrical proofs.
When the symbolic engine doesn't manage to find a formal and rigorous proof on its own, it solicits the large language model, which suggests a geometrical construct to move forward.
However, it is unclear how applicable this method is to other domains of mathematics or reasoning, because symbolic engines rely on domain-specific rules and because of the need for synthetic data.