Geometry proofs stop relying on the model alone: retrieve structurally similar solved problems, then let a symbolic verifier correct each step
When a general-purpose model writes a geometry proof, it first retrieves structurally similar solved problems as examples, and a symbolic verifier then points out errors round by round. On 50 SAT-level Euclidean geometry problems from FormalGeo-7k, the full pipeline reaches 68%–96% proof accuracy, against 10%–44% for baselines that use neither analogical retrieval nor verifier feedback. Under the same verifier feedback and inference budget, analogical guidance alone lifts GPT-5 from 88% to 96% and o1 from 52% to 80%.