Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Let be the largest for which there are pairwise disjoint with for every . Then . The upper bound is disjointness. For the lower bound, Bloom's Theorem 3 gives an absolute such that for all large every subset of with reciprocal sum at least contains a subset of reciprocal sum one; removing such a subset while the remaining reciprocal sum is at least produces more than 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 : the estimate is exact to first order, so the value is solved, and since 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 for large .
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.