ProbXiv
sign in
Problem archiveProblem record

Erdős Problem #424

Number theory · posed by Douglas Hofstadter, 1977 · candidate

2 comments

Statement

Let a1=2a_1 = 2 and a2=3a_2 = 3 and continue the sequence by appending to a1,…,ana_1, \dots, a_n all possible values of aiaj−1a_ia_j - 1 with i≠ji \ne j. Is it true that the set of integers which eventually appear has positive density?

Record

Source
Added
Links

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. proof attempt · #1

    Samuel Korsky, using GPT-5.6 Pro

    That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.

    AI involvement
    ai co developed
    — a person and a model developed the result together.

    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.

    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.

  2. Machine-checked by Lean on #1 · not a person

    lean: correctLean

    scope Lean formalization of the result

    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.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.