Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 440
claims/: The 1 claim page of Problem 440, one per claimant's result; the problem's standing derives from them.
Statement. Let be infinite and let count the number of indices for which $\mathrm{lcm}(a_i,a_{i+1})\leq x$. Is it true that ?
How large can
be?
Formulation. The site's wording as of 2026-09-18 (page last edited 27 December 2025). counts the indices with ; for it counts the with , so . The source paper writes this count as inside a family counting blocks of consecutive terms whose least common multiple is at most ; the problem is the case , and the general case is the Monthly problem the paper's title refers to. The origin is printed p. 87 of the Erdős--Graham monograph: "Let be an infinite sequence of integers and denote by the number of indices for which . It seems likely that . It is easy to give a sequence with . How large can be (see [Er-Sz (xx)a])?", the "(xx)" being the monograph's placeholder for the then unpublished 1980 paper. The site's label SOLVED, which the site defines as a resolution other than a proof or a disproof, covers the two answers: yes to the first question, and the value for the second.
Status. Solved. Both questions are answered in Erdős and Szemerédi's 1980 paper (Mat. Lapok 28, 121--124, in Hungarian). Theorem I gives with , so and the answer to the first question is yes; Theorem II gives for every , and attains , so the largest possible value of the liminf is exactly . The printed proof of Theorem II ends with a false numerical assertion ( for a series equal to ) and does not close as printed; the theorem is true, by the authored averaging proof under Current assessment, which is a note of this corpus and not acceptance evidence. Mat. Lapok is the refereed journal of the Bolyai Society (the card records MR 82c:10066 and Zbl 476.10045). Claim page: Erdős and Szemerédi 1980 (accepted; refereed, and credited by the site's curator), which also links the public Lean file of August 2026 that declares itself a formalization of their result (not built or audited in this corpus).
Source. erdosproblems.com/440, accessed 2026-09-18: the problem page (SOLVED; last edited 27 December 2025; source key [ErGr80, p. 87], with [ErSz80] in the commentary), its eight-comment discussion thread (26 October and 27 December 2025) and its empty proof-claim tab. Cite as: T. F. Bloom, Erdős Problem #440, https://www.erdosproblems.com/440, accessed 2026-09-18.
References.
- [ErSz80] Erdős, P. and Szemerédi, E., Megjegyzések az American Mathematical Monthly egy problémájához (Remarks on a problem of the American Mathematical Monthly). Mat. Lapok 28 (1980), no. 1--3, 121--124 (Hungarian). Theorems I, II and III, printed p. 121; the proofs, pp. 122--124. Library home: erdos_1980_megjegyzesek_az_american_mathematical_monthly_egy.
- [ErGr80] Erdős, P. and Graham, R. L., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathématique 28, Université de Genève (1980), printed p. 87. Library home: erdos_1980_old_new_problems_results_combinatorial_number_theory.
- [vD] van Doorn, W., Sequences with bounded lcm for consecutive elements. A two-page note in the author's GitHub repository of mathematical shorts, Woett/Mathematical-shorts (the file last changed 12 August 2025, at the repository head of 2026-09-18), linked from the site's commentary. A lead, not a source of the status.
Formalization. Statement in
formal-conjectures,
added on 20 September 2026 and linked at that commit: the file
ErdosProblems/440.lean states the first question (erdos_440.parts.i, answer
yes), the second (erdos_440.parts.ii, the greatest liminf is ) and the
limsup constant (erdos_440.variants.erdos_szemeredi), each tagged research solved with a sorry body and a formal_proof attribute naming the
plby/lean-proofs file below, so the collection holds statements and no proof.
On 2026-09-18 no such file existed on the collection's main branch, the page's
formalized-statement indicator read no, and the community database
(teorth/erdosproblems,) recorded the problem solved (last changed 27 December
2025), not formalized, with no formal proof. Outside the collection, the
repository plby/lean-proofs at its head of 15 September 2026 (the commit the
claim page links) holds src/latest/ErdosProblems/Erdos440.lean with four
supporting files under Erdos440/, whose closing theorem erdos_440 asserts
five conjuncts: every counting function is , the Erdős--Szemerédi
series is the universal limsup coefficient, that coefficient is attained by some
sequence, every normalized liminf is at most one, and one is attained by the
positive integers. Its header calls the file a formalization of a solution to
the problem and names Erdős and Szemerédi as informal authors and Codex and
GPT-5.6 Sol as formal authors; it contains no sorry and no axiom. Nothing
was built or audited in this corpus, the site does not label the problem Lean,
and no kernel credit is claimed. Because the file declares itself a
formalization of Erdős and Szemerédi's result, it is recorded as a formalization
link on their claim page and has no page of its own.
Current assessment
The question (site formulation as of 2026-09-18). The statement above; SOLVED, last edited 27 December 2025; source key [ErGr80, p. 87]. The commentary: taking shows is possible, and [ErSz80] gives the bound for every ; Tao's thread comment gives a short proof of ; van Doorn proved with , a bound the commentary attributes to [ErSz80] already, adding that the authors showed the constant to be optimal; and [ErSz80] holds more related results, for . The thread: a question of 26 October 2025 whether the liminf bound holds for every , in which case solves the problem, and the site author's answer of 27 December 2025 that, going by a machine translation, it does; Tao's argument for (26 October 2025); van Doorn's note on the finite version with the constant and the exchange in which the site's author locates the same constant in [ErSz80] (first read as and corrected to by the rearrangement below), reads the paper as also proving , and is unsure whether it claims the constant is best possible. The proof-claim tab is empty.
The origin. Printed p. 87 of the monograph, quoted under Formulation; the same page states the finite neighbor, the largest set with pairwise least common multiples at most , which is Problem 441.
What the source proves. Erdős and Szemerédi (printed p. 121) take an infinite sequence , put and , recall the Monthly problem, to prove with depending only on , and say the proof for is very easy. Theorem I: , and if equality holds then . Theorem II: for every . Since , Theorem I answers the first question, and Theorem II with the example (an elementary check made in this corpus: , so ) answers the second: the largest possible value of is . Theorem III: for there is such that for every sufficiently large a suitable has , so the Monthly bound is false for ; the paper adds the bounds for all and infinitely often for suitable (pp. 121--122 and 124). These are the related results the site's commentary mentions and are not part of the problem. Read depth: claims checked for the three statements; the proof of Theorem I (pp. 122--123) was read for its structure and not checked step by step, and the proof of Theorem II (p. 123) was read to its final display, where the error recorded below was found.
Theorem II: the printed proof and an authored repair. The proof of Theorem II on printed p. 123 ends by asserting that is less than and concluding along the chosen , where is the lower density of . But (summed for this corpus to two million terms with an integral estimate of the tail; the term alone is , and the partial sums first pass at ), so for every the displayed bound exceeds by a constant factor, and the printed argument does not give . The theorem is true, by the following averaging argument, an authored note of this corpus and not acceptance evidence. Write and ; since divides , . For and , counting each index over the part of where it is counted,
The indices on the right fall into four classes. Those with number at most and contribute at most each, so at most in all. Those with and contribute at most each; for this is at most , and for it exceeds by at most , so these terms telescope to at most . At most one index has , contributing at most . Finally, for the indices with , take the dyadic block with : the condition forces , so the block holds at most such indices, and their gaps, apart from the last index of the block, are disjoint subintervals of with total length at most ; by the Cauchy--Schwarz inequality their terms sum to at most , and the last index contributes at most . Summed over this class contributes at most . Altogether, for ,
If held for all , the integral would be at least ; so for with every interval with contains an with , and .
The constant, reconciled (an authored one-line summation by parts). The paper's and the site's are the same number. Since ,
and . Both series were summed for this corpus to two million terms with an integral estimate of the tail: (the partial sums agree to all printed digits for ). Van Doorn's thread comment gives the same rearrangement. The site's sentence that Erdős and Szemerédi showed the constant to be optimal is not confirmed by the paper: Theorem I says only that equality would force the liminf to zero, and the paper exhibits no sequence attaining the constant; the thread records the same uncertainty. Attainment is asserted by the external Lean file described under Formalization, which was not built in this corpus and is linked from the accepted claim page as a self-declared formalization, and by van Doorn's recollection in the thread.
Forum items (leads with provenance, not status). Tao's comment of 26 October 2025: if and then and hence , so there are such indices with , and summing over gives . Van Doorn's note [vD]: for with for all , with , by bounding the last element of the sequence whose gap to the element before it is at most by ; the note's author writes in the thread that this finite version is not the monograph's question, although the proof carries over. Neither item is needed for the status; the paper already covers both.
Search scope. None of the routes below found a source contradicting the two answers or a proof claim.
- The site: problem page, discussion thread and proof-claim tab on 2026-09-18; the full directory listing and tree of formal-conjectures on its main branch (no file for this problem on that date); the community database entry.
- Crossref: a bibliographic query for the title of [ErSz80] (no record for the Mat. Lapok article; Mat. Lapok is not indexed).
- GitHub API:
plby/lean-proofs(head commit, the twoErdosProblemsdirectory listings, the 440 files' headers and closing theorem); the author's repository of mathematical shorts (head commit, the note's last commit, the note itself). - arXiv API:
abs:"consecutive" AND abs:"least common multiple" AND abs:sequence(two records, on least common multiples of progressions and of divisibility sequences) andabs:"least common multiple" AND abs:Erdős(four records, none on this problem); the API searches titles and abstracts only, so these zeros are weak. - Semantic Scholar: the search endpoint answered HTTP 429 to the query for [ErSz80] and was not retried.
- The primary sources: [ErSz80] pp. 121--124 and [ErGr80] p. 87.
Not searched: MathSciNet, zbMATH, Google Scholar, X.
Remaining gaps. (1) Proof coverage is statements only: Theorems I and II are compiled at claims checked with proof sketches; nothing is independently reviewed. The printed proof of Theorem II does not close as printed (its final step asserts where ); the averaging proof above is an authored note of this corpus and not evidence, and the accepted standing rests on the refereed publication and the curator's credit, with the flaw disclosed. (2) Whether the constant of Theorem I is attained by some sequence is not settled by the paper; the site's sentence is recorded as the site's. (3) The general Monthly problem is not this problem. At the paper records (pp. 121--122, arguments on p. 124) that for every , and that some has for infinitely many . So the Monthly bound fails at too. The paper leaves open whether some has for every . At the authors expect for some but give no proof.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.
- erdos_1980_megjegyzesek_az_american_mathematical_monthly_egy
- erdos_1980_megjegyzesek_az_american_mathematical_monthly_egy / theorem_i
- erdos_1980_megjegyzesek_az_american_mathematical_monthly_egy / theorem_ii
- erdos_1980_megjegyzesek_az_american_mathematical_monthly_egy / theorem_iii
- erdos_1980_megjegyzesek_az_american_mathematical_monthly_egy / theorem_p121
- erdos_1980_old_new_problems_results_combinatorial_number_theory