Thomas Bloom: Erdős problems in the OpenAI proofs

Bloom lists the 25 Erdős problems with significant claims in OpenAI’s 6 Oct release (12 on the FrontierMath Erdős list; 21 with Lean formalizations; 1,347 PDF pages). He gives short notes on each, with two disclaimers: he has not seriously checked any proof, and there are open attribution and plagiarism questions. He calls the papers “very poorly written, in the usual AI fashion” but expects most to be “(a) correct yet (b) capable of being substantially simplified”. He urges mathematicians to treat them as “raw material”, not as closing the problems. On #3 he notes that the Lean challenge states only Erdős’s qualitative conjecture and that the Lean code seems to prove a weaker bound than the PDF claims.