Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to Problem 401 is yes, by a second route. Nat Sothanaphan reported in the site's discussion thread on 11 January 2026 that ChatGPT had noticed that the construction solving Problem 729 also solves this problem; the claimant posted the deduction with their own check of it, and their write-up of the Lean proof of Problem 728, Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof (arXiv:2601.07421, version 5 of 26 January 2026; carded at sothanaphan_2026_resolution_erdos_problem_728_writeup_aristotle), gives the deduction in its appendix "beyond this proof", which first appears in version 3 of 15 January 2026. The appendix's Theorem 2 states that there are absolute constants such that the set of for which
for every prime and every has asymptotic density . For Problem 729 one takes and checks that primes above a threshold depending on do not divide the denominator of ; for this problem the paper says the same examples work, with the extra requirement for the small primes that , which Legendre's formula makes easy since the left side is . In the thread post the examples are , , , and is defined from the thresholds at which the small primes are absorbed, so that .
Standing. The claim is claimed. The appendix proves Theorem 2 only in
outline, by pointing to the lemmas of the main proof and saying which
parameter must change, and the deduction for this problem is a paragraph; no
outside reviewer has accepted this route, the paper is not refereed, and the
site credits the problem to Barreto and Leeham, whose proof is recorded on
their page.
The paper itself says the two problems were solved first by the other route
and that the connection to its argument was noticed afterwards. The write-up
was prepared with ChatGPT, as the paper states.
Depends on. [[problems/factorials_binomials/E0729/claims/2026_01_10_barreto_price|Barreto and Price's proof of Problem 729]], whose construction the thread deduction starts from, and [[problems/factorials_binomials/E0728/claims/2026_01_06_barreto|Barreto's proof of Problem 728]], whose lemmas the appendix reruns to prove its Theorem 2; the Lean development behind both, in Boris Alexeev's repository, is cited by the paper and not built here.