VibeMathedMath problems solved by AI

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
—
Years open
—
Solved
2026-06-27
Model
ChatGPT, Aristotle
Vendor
OpenAI / Harmonic
Collaborators
Eric Li
Verification
Unreviewed
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.

Source

arXiv:2606.29062 - A Resolution of Erdos Problem 731 under Dyadic Regularity

Discussion