AI 'solved' famous maths problems. Read the asterisks.

Two claims, one week. OpenAI: an internal reasoning model disproved Erdős's 1946 unit-distance conjecture. DeepMind: AlphaProof Nexus solved nine open Erdős problems plus 44 conjectures. The dunk-tweet version — 'Google beat OpenAI nine to one' — is fun and almost entirely beside the point.

OpenAI's proof is human-checked and not yet through formal peer review. DeepMind's nine are machine-verified in Lean — which is the genuinely impressive part, but it also means the win comes from a tight generate-then-verify loop, not a model free-soloing genius. DeepMind even noted a basic agent solved the same nine; the fancier system mostly made it cheaper.

The tell is that the people closest to it are the most careful: Hassabis said straight out the system is 'still not AGI'. When the vendor undersells and the timeline oversells, trust the vendor. AI is now a real instrument for parts of maths — narrow parts, with a human or a checker holding the pen.