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?
Formal statementwhat was actually proved, as formalized
/-- The recursively generated set in Erdős Problem 424. Using an inductivepredicate makes the phrase "the smallest set" literal: its constructors areexactly the two seeds and the closure rule. -/inductive Generated : ℕ → Prop where | two : Generated 2 | three : Generated 3 | mul_sub_one {a b : ℕ} : Generated a → Generated b → a ≠ b → Generated (a * b - 1) /-- Number of generated positive integers at most `x`. -/noncomputable def countUpTo (x : ℕ) : ℕ := by classical exact ((Finset.Icc 1 x).filter Generated).card /-- The exact conclusion called "positive lower density" in the paper. -/def HasPositiveLowerDensity : Prop := ∃ c : ℝ, 0 < c ∧ ∀ᶠ x : ℕ in Filter.atTop, c * (x : ℝ) ≤ (countUpTo x : ℝ) theorem theorem_one : HasPositiveLowerDensity := … /-- The new numbers obtained from `A` by applying `x * y - 1` to distinctmembers of `A`. This agrees verbatim with the `formal-conjectures`definition. -/def nextGeneration (A : Set ℕ) : Set ℕ := {z : ℕ | ∃ x y, x ∈ A ∧ y ∈ A ∧ x ≠ y ∧ z = x * y - 1} /-- The finite-stage closure used by `formal-conjectures`. -/def sequenceSet : ℕ → Set ℕ | 0 => {2, 3} | n + 1 => sequenceSet n ∪ nextGeneration (sequenceSet n) /-- The union of all finite stages, as in `formal-conjectures`. -/def generatedSet : Set ℕ := ⋃ n : ℕ, sequenceSet n open Classical in/-- The intended problem statement in the staged-set formulation. -/theorem erdos_424_lower_density : ∃ c : ℝ, 0 < c ∧ ∀ᶠ x : ℕ in Filter.atTop, c * (x : ℝ) ≤ (((Finset.Icc 1 x).filter fun n ↦ n ∈ generatedSet).card : ℝ) := generatedSet_has_positive_lower_densityA machine checks that the proof entails this statement. Whether this statement is the problem is for you to judge. Source
- 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
- 10 / 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
Submitted by GoldenMongoose827