Wiki
Wiki

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

Updated


Claim. Let k(N)k(N) be the largest kk for which there are pairwise disjoint A1,…,Ak⊆{1,…,N}A_1,\ldots,A_k\subseteq\{1,\ldots,N\} with ∑n∈Ai1/n=1\sum_{n\in A_i}1/n=1 for every ii. Then k(N)=(1−o(1))log⁡Nk(N)=(1-o(1))\log N. The upper bound k(N)≤∑n≤N1/n≤1+log⁡Nk(N)\le\sum_{n\le N}1/n\le1+\log N is disjointness. For the lower bound, Bloom's Theorem 3 gives an absolute CC such that for all large NN every subset of {1,…,N}\{1,\ldots,N\} with reciprocal sum at least T(N)=Clog⁡Nlog⁡log⁡log⁡N/log⁡log⁡NT(N)=C\log N\log\log\log N/\log\log N contains a subset of reciprocal sum one; removing such a subset while the remaining reciprocal sum is at least T(N)T(N) produces more than log⁡N−T(N)\log N-T(N) pairwise disjoint sets. The deduction is written out on the problem page under "The estimate and its deduction". The question asks for an estimate and whether k(N)=o(log⁡N)k(N)=o(\log N): the estimate is exact to first order, so the value is solved, and since k(N)/log⁡N→1k(N)/\log N\to1 the answer to the closing question is no. With Liu and Sawhney's Theorem 1.1 in place of Theorem 3 the lower bound sharpens to k(N)>log⁡N−(log⁡N)4/5+εk(N)>\log N-(\log N)^{4/5+\varepsilon} for large NN.

Sources. The input theorem is Bloom's Theorem 3 (arXiv:2112.03726v2; Theorem 1.3 of J. Eur. Math. Soc. 27 (2025), no. 11, 4563--4589), for which the library holds a complete rewritten proof, not independently reviewed; the sharpening is Liu and Sawhney's Theorem 1.1. The greedy step needs nothing beyond Theorem 3 and the size of the harmonic sum.

Depends on. Bloom's reciprocal-mass threshold supplies Theorem 3; the greedy removal is the only further step. The sharpening of the error term rests on Liu and Sawhney's threshold.

Acceptance. The observation appears in no publication: the site's commentary records it, crediting Hunter and Sawhney. An archived copy of the problem page captured on 16 June 2024 (the record link above) already shows the remark, the thanks to Zachary Hunter and Mehtaab Sawhney and the label SOLVED, so the remark predates that date, which dates this page; the site's revision history begins only with a version of 20 October 2025 and records no finer date. The site's curator, Thomas Bloom, labels the problem proved on the strength of the estimate and credits the observation to Hunter and Sawhney; the curator is not one of them, and that credit is the reviewed evidence. The curator is the author of Theorem 3, which is refereed, but the deduction itself is unpublished, so refereed is not listed. Three Lean files declare themselves formalizations of the estimate and are linked above: the file in plby/lean-proofs that the formal-conjectures statement tags as its proof names Bloom, Hunter and Sawhney as informal authors and the prover Aristotle and John Jennings as formal authors, and proves the two-sided statement without sorry, its closing comment listing the axioms propext, Classical.choice and Quot.sound; the gist of 22 April 2026, produced by Aristotle, is conditional on one declared axiom standing for Theorem 3; the standalone file in Jayyhk/erdos-lean of 26 May 2026 vendors the Lean 4 port of the Bloom–Mehta formalization and proves the lower bound unconditionally with the same three axioms. None was built or audited by this corpus, so formalized is not listed; the formal-conjectures file is a statement with a sorry body and is not a formalization.