Erdős Problem #741
Erdős problem #741 · erdosproblems.com/741
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Additive Combinatorics
- Posed by
- Paul Erdős
- Year posed
- 1994
- Years open
- 32y
- Solved
- 2026-04-16
- Model
- DeepMind prover agent
- Vendor
- —
- Collaborators
- Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, Gregory Valiant
- Verification
- Lean-verified
- Publication
- Announced
- Significance
- 10 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
From "Short proofs in combinatorics and number theory": "In each case, the proof is due entirely to an internal model at OpenAI. The role of the human authors was simply to digest the proofs and modify the write-ups for clarity and elegance." Priority note: this paper (31 March 2026) constructs the basis of order two with no syndetic split that Burr and Erdos asked for, which is this problem. The solve recorded here is dated 16 April 2026 and credited to a DeepMind prover agent, so the Lean-verified resolution appears to follow the earlier OpenAI-model proof rather than to be independent of it. Both are linked; the priority has not been adjudicated here.
Verification
Listed as solved on erdosproblems.com and the proof is verified in Lean. Solve credited via Terence Tao's AI-contributions wiki.