VibeMathedMath problems solved with AI
Sign in

Erdos Problem #731

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

Let A(n)A(n) be the least positive integer not dividing (2nn)\binom{2n}{n}. Erdos asked for the behaviour of A(n)A(n) for reasonable nn. Under an explicit dyadic-regularity formalization of reasonable, the distribution is determined on dyadic intervals against the scale FX=2(log⁡2)1/4L1/4exp⁡(log⁡2)LF_X = \sqrt{2}(\log 2)^{1/4} L^{1/4} \exp\sqrt{(\log 2)L} with L=log⁡(2X)L = \log(2X).

Result
Proved(see note)
Status
Partial result
AI contribution
AI co-developed
Method
Argument
Field
Number theory
Posed by
Paul Erdos
Year posed
1975
Years open
51y
Solved
2026-06-27
Model
ChatGPT, Aristotle
Vendor
OpenAI / Harmonic
Collaborators
Eric Li
Verification
Lean-checked, statement unaudited
Publication
Preprint
Significance
10 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Resolved under an explicit formalization of 'reasonable', not in full generality.

What the AI did

The declaration says large language models, primarily ChatGPT, were used extensively throughout the research while the author originated the ideas, and that the accompanying Lean formalization was developed by the author with Aristotle.

Verification

A Lean formalization accompanies the paper; we have not compiled it. The result is conditional on the paper's own formalization of Erdos's informal word 'reasonable', which the entry's resolution status reflects. arXiv preprint, not peer-reviewed, and problem still marked open on the Erdos problems database.

Sources

Changelog1 change
  • Matarisvanchanged What was actually shown from “resolved under an explicit formalization of 'reasonable', not in full generality” to “Resolved under an explicit formalization of 'reasonable', not in full generality.”, also More links, Year posed, Verification, Significance note, Verification note

Discussion