Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Cambie [Ca25b] proves (Theorem 1 of the paper) that g(n)≍(n/log⁡n)1/2g(n)\asymp(n/\log n)^{1/2}, which is the estimate the problem asks for. The two proofs give the explicit constants, which Remark 2 records:

(2−o(1))(nlog⁡n)1/2≤g(n)≤(22+o(1))(nlog⁡n)1/2.(2-o(1))\Bigl(\frac{n}{\log n}\Bigr)^{1/2}\le g(n) \le(2\sqrt2+o(1))\Bigl(\frac{n}{\log n}\Bigr)^{1/2}.

Cambie defines g(n)g(n) over chains 0<a1<⋯<at≤n0<a_1<\dots<a_t\le n, where the site's statement has 2≤ai<n2\le a_i<n; the two lengths differ by at most two, so the bounds hold for either definition. For the upper bound, write each term as ai=qiP(ai)a_i=q_iP(a_i); along a chain both the cofactors qiq_i and the primes P(ai)P(a_i) are pairwise distinct, and splitting the terms by whether qi≤(2n/log⁡n)1/2q_i\le(2n/\log n)^{1/2} or P(ai)≤(nlog⁡n/2)1/2P(a_i)\le(n\log n/2)^{1/2} bounds each class through the prime number theorem. For the lower bound, take the primes p1>⋯>prp_1>\dots>p_r in (n1/2,(nlog⁡n)1/2)(n^{1/2},(n\log n)^{1/2}) and set ai=qipia_i=q_ip_i with qiq_i minimal subject to ai>ai−1a_i>a_{i-1}; a partial-summation estimate for sums over primes shows that the chain has length (2−o(1))(n/log⁡n)1/2(2-o(1))(n/\log n)^{1/2}. Cambie asks whether g(n)∼c (n/log⁡n)1/2g(n)\sim c\,(n/\log n)^{1/2} for some constant cc, which Remark 2 confines to 2≤c≤222\le c\le2\sqrt2; that question is open and lies beyond the asked estimate. The source card digests the paper.

Acceptance. Refereed: Proc. Amer. Math. Soc. 153 (2025), no. 8, 3315--3317, doi:10.1090/proc/17279, published online 2025-06-12, the journal version of arXiv:2503.22691 (v1, 2025-03-13, three pages, CC BY 4.0), whose text thanks the referees. Reviewed: the site's curator, Thomas F. Bloom, records the problem as solved by this result, states the theorem and reports the open question about the constant (site page accessed; it carries no last-edited date); Bloom is independent of the author.

Lean. Not formalized evidence: this corpus has not built or audited the development, so it gives no formalized evidence. The site's Lean label follows the formalization of Cambie's proof that Boris Alexeev announced in the site's thread on 2026-02-04, a Lean proof by the Aristotle system; that version assumed the prime number theorem as an axiom. The file linked above at its pinned commit (2026-08-01), in the lean-proofs repository, names Cambie as its informal author and Aristotle and Alexeev as its formal authors, imports the prime number theorem from the PrimeNumberTheoremAnd project and derives the statement the earlier version assumed, declares g_upper_bound_asymptotic, the OO-bound, and erdos_648, the Θ\Theta statement, whose proof contains the lower bound, and records for erdos_648 the axioms propext, Classical.choice and Quot.sound, the file's own record. The formal-conjectures statement file ErdosProblems/648.lean records it as the formal proof of its own statement erdos_648, that g(n)g(n) is Θ(n/log⁡n)\Theta(\sqrt{n/\log n}), and notes three divergences, two of them mathematical: the hosted proof follows Cambie's range 0<m≤n0<m\le n where the problem text has 2≤ai<n2\le a_i<n, and it defines PP with the default value 11 for m=1m=1; the two definitions agree for m≥2m\ge2, and admitting 11 and nn changes the chain length by at most two, so the order of growth is unaffected. The third is packaging: a strictly monotone map on Fin t in place of the hosted file's list with IsChain.

Depends on. No page of this wiki: the result rests on the cited paper alone.