Erdős Problem #424
Erdős problem #424 · erdosproblems.com/424
Let and and continue the sequence by appending to all possible values of with . Is it true that the set of integers which eventually appear has positive density?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Number Theory, Integer Sequences
- Posed by
- Douglas Hofstadter
- Year posed
- 1977
- Years open
- 49y
- Solved
- 2026-07-20
- Model
- GPT-5.6 Pro
- Vendor
- OpenAI
- Collaborators
- Samuel Korsky
- Verification
- Lean-verified
- Publication
- Announced
- Significance
- 13 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Proves positive lower density. The Formal Conjectures encoding asks for Set.HasPosDensity, a density that exists and is positive; erdosproblems.com says Erdos most likely meant lower density.
What the AI did
GPT-5.6 Pro developed the argument together with Samuel Korsky, in particular searching for the transition matrices the interval-partition argument needs. The Lean formalization was produced separately, with Codex, by Boris Alexeev.
Verification
Lean 4.32.0 and Mathlib v4.32.0 formalization by Boris Alexeev, produced with Codex, from the informal argument of Samuel Korsky and GPT-5.6 Pro. Rebuilt independently on 2026-08-02 against Lean 4.32.0 and Mathlib v4.32.0 (the file as published, sha256 ca4a2371918b1a7c66dccfe324305298): all 6,394 lines compile in 1,215 s with no sorry and no admit, and #print axioms reports the top theorem depending on exactly [propext, Classical.choice, Quot.sound], the three standard Lean axioms, with no sorryAx and nothing assumed. The formalized conclusion is positive lower density, stated against the same nextGeneration, sequenceSet and generatedSet definitions the Formal Conjectures statement of #424 uses. Status is candidate rather than resolved because erdosproblems.com has not accepted the claim: its proof-claims page states plainly that appearing there is no guarantee of correctness and does not mean anyone associated with the site examined any part of the proof.
Sources
- PaperManuscript (PDF)
- Lean proofLean proof (Erdos424.lean)
- Lean statementFormal Conjectures statement of #424
- Problem recordProblem 63 of Ben Green's 100 Open Problems
- Discussionerdosproblems.comProof claim on erdosproblems.com
Submitted by GoldenMongoose827 on
Recording a change to this entry's score, prompted by a reader.
This problem is also Problem 63 on Ben Green's *100 Open Problems*. Both ends check out: erdosproblems.com/424 closes with "See also Problem 63 of Green's open problems list", and Problem 63 of that PDF reads "Let A be the smallest set containing 2 and 3 and such that a1a2−1∈A if a1,a2∈A. Does A have positive density?" - the same question, with Green's own comment linking back here.
The significance note previously said the reference trail was modest. It is not. Together with section E31 of Guy's *Unsolved Problems in Number Theory*, OEIS A005244, the Formal Conjectures entry and two Erdős source citations, this is a well-attended problem by numbered-Erdős standards, and Green's list is a curated signal rather than a compendium - he writes that he steered clear of both notorious problems and ones that look hopeless.
Significance moves 10 to 13, level with Erdős #390 and below #1196 at 15. The score describes how much mathematics cared about the problem before it was solved, so this is a correction to an under-informed judgment, not a reaction to the solution. Green's list is now linked on the entry.