VibeMathedMath problems solved by AI
All problems

Erdős Problem #346

Erdős problem #346 · erdosproblems.com/346

Let A={1≤a1<a2<⋯ }A=\{1\leq a_1< a_2<\cdots\} be a set of integers such that A\BA\backslash B is complete for any finite subset BB and not complete for any infinite subset BB. If an+1/an≥1+ϵa_{n+1}/a_n \geq 1+\epsilon for all nn, must lim⁡nan+1/an=(1+5)/2\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI co-developed
Method
Argument
Field
Number Theory, Complete Sequences
Posed by
Paul Erdős, Ronald Graham
Year posed
1980
Years open
46y
Solved
2026-06-21
Model
ChatGPT, Codex
Vendor
OpenAI
Collaborators
Kenta Kitamura
Verification
Lean-verified
Publication
Announced
Significance
10 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

The problem statement is ambiguous: the limit-exists reading is claimed proved (Lean), while the convergence-from-hypotheses reading was disproved by a Lean-checked construction of Price that the community classes as a variant

What the AI did

Kitamura's affirmative Lean 4 formalization of the limit-exists reading was produced with ChatGPT and Codex; days earlier, GPT Pro with Codex had produced a Lean-checked disproof of the literal reading (Liam Price), which the forum classes as solving a variant with precursors in Burr-Erdős 1981.

Verification

A community screening found the Lean of the variant disproof correct and corresponding to its paper (one typo); the affirmative limit-exists formalization reports standard axioms only. erdosproblems.com still lists the problem open.

Sources

erdosproblems.com/346

Discussion