DeepMind's AI models AlphaProof and AlphaGeometry 2 solved four out of six problems at the International Mathematical Olympiad (IMO), reaching the level equivalent to a silver medalist. AlphaProof employs reinforcement learning for formal math reasoning, while AlphaGeometry 2 is a neuro-symbolic hybrid that solves complex geometry problems effectively.