Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Let assign to every real a closed set of Lebesgue measure less than . Then there is an infinite set with for all distinct (Corollary (1), p. 338, of the Theorem on p. 336). No boundedness is assumed. An infinite independent set contains one of size , so the second question of Problem 501 has a positive answer; the paper presents the corollary as the answer to Problem 38(B) of the Erdős–Hajnal list. Gładysz had earlier found a free pair under an integral condition on the sets, as the paper describes it on p. 335 (the site states his result under the second question's hypotheses; Acta Math. Acad. Sci. Hungar. 13 (1962), 199–201; not held).
Covers. The second question only: closed sets of measure force an independent set of size , and in fact an infinite one. The first question, about bounded sets of outer measure that need not be closed, lies outside the Theorem's closed-sections hypothesis and is settled on Glazer's claim page.
Source. L. Newelski, J. Pawlikowski and W. Seredyński, Infinite free set for small measure set mappings, Proc. Amer. Math. Soc. 100 (1987), no. 2, 335–339, received by the editors 1986-01-06. Its Lemma, Theorem and Corollaries (1)–(4) are recorded clause by clause on the source card, the proofs followed and not verified. This page is dated by the issue month, June 1987; the issue prints no day.
Acceptance. Refereed: the Proceedings of the American Mathematical Society. Reviewed: the curator of erdosproblems.com (T. F. Bloom) credits [NPS87] in the problem's commentary with an infinite independent set under the second question's hypotheses, and so with the answer to that question; the page's label NOT DISPROVABLE composes this part with the independence of the first question. The curator is independent of the authors.
Formalization. The conclusion is proved in Lean, from Mathlib, as
erdos501_closed_infinite, and the question as asked (an independent set of
size at least ) as erdos501_closed_size3, inside Glazer's development,
whose comparator targets state this theorem under the authors' names; the
development and the copy of it in Boris Alexeev's repository are linked
above at their pinned commits, and
formal-conjectures 501.lean
marks its variants closed_size3 and
newelski_pawlikowski_seredynski research solved with formal-proof links
to that copy. The development's own axiom audit and comparator record are
described on
Glazer's claim page.
Neither copy was built in this corpus, so the formalization is a link and
not formalized evidence.