As of: 2026-10-09 19:24 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/p/2026-10-08-bloom-erdos-problems-in-openai-proofs/

# Thomas Bloom: Erdős problems in the OpenAI proofs

Thomas Bloom (@thomasfbloom), Blog, 2026-10-08.
Source: https://www.erdosproblems.com/forum/thread/blog:10

## Why it matters

The erdosproblems.com maintainer's triage of OpenAI's release: claims on 25 Erdős problems, 21 formalized, plus a Lean-vs-PDF gap on problem #3.

## Summary

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.

## Archived text

Blog: summary and short quotes only

## Cited in

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/)