formal-verification
Posts tagged “formal-verification”.
-
AI Brief, 8 October 2026: 722 proofs, and the paper that says Lean cannot settle them
OpenAI published 722 machine-written mathematical manuscripts on 6 October, including a claimed proof of the Unique Games Conjecture. An hour before that release, three mathematicians posted a proof that faithful autoformalisation sits higher in the arithmetical hierarchy than the halting problem, and showed OpenAI's own Navier-Stokes Lean proof does not match its prose. Anthropic shipped Haiku 5.5 with a million-token window and a price cliff at 100k.