---

Claim. Kleitman's theorem: a family $\mathcal F$ of subsets of $[n]$ with no three distinct members $A,B,C$ satisfying $A\cup B=C$ has $|\mathcal F|<(1+o(1))\binom{n}{\lfloor n/2\rfloor}$. Erdős's reduction turns the weaker bound $f(n)=o(2^n)$ for the maximum size $f(n)$ of such a family into the answer to this problem: a set $A\subseteq\mathbb N$ of positive lower density contains three distinct members with $[a,b]=c$, and in fact infinitely many such triples. Erdős states the reduction in his 1965 survey (display (69)) as a consequence that "would follow from" the union-free bound, without carrying it out; the site's thread describes the implication as taking real work, and the Lean development linked below formalizes one route (pass to the odd parts of the members of $A$ with a fixed power of two, a class of positive upper logarithmic density; bound a counting quantity for an lcm-triple-free set by $o(N\log N)$ through Kleitman's theorem; show that positive upper logarithmic density forces it to be $\gg N\log N$ along a subsequence).

Postings. Kleitman, D., Collections of subsets containing no two sets and their union. Combinatorics (Proc. Sympos. Pure Math. XIX, Univ. California, Los Angeles, 1968), Amer. Math. Soc. (1971), 153--155. The paper is not held here and no open copy was found; its theorem is taken from the site's page for Problem 447, which it settles directly. The page is dated to the first day of 1971, the volume's year. The site's pages for Problems 447 and 487 carry the attribution from their earliest revisions in the site's history view (20 October 2025).

Formalization. The two formalization links are the file Erdos487.lean of the repository plby/lean-proofs, which declares itself a Lean formalization of a solution to this problem, names Daniel Kleitman as the informal author and Aristotle and Boris Alexeev as the formal authors, defines lowerDensity as the lower asymptotic density of a set of natural numbers and proves theorem erdos_487 (A : Set ℕ) (hA : lowerDensity A > 0) : ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ Nat.lcm a b = c, importing the repository's Erdos447.lean, which proves Kleitman's asymptotic bound erdos_447. The self-contained first version was added on 16 February 2026 and announced in the site's thread the same day by Boris Alexeev, who wrote that the implication from Problem 447 takes a decent amount of work and that the result had been formalized by Aristotle; the current path is linked at its committer date of 2026-06-30. At the pinned commits neither file contains a sorry or an axiom declaration, and each has a closing comment recording the axioms propext, Classical.choice and Quot.sound. Neither file was built or kernel-checked here, the hypothesis lowerDensity A > 0 was not bridged to the formal-conjectures statement's HasPosDensity, and no statement-fidelity review exists here, so the development is a link, not formalized evidence. The site's PROVED (LEAN) label, fed from the community database, refers to it; the database lists the problem as proved (Lean) as of its last update on 16 February 2026.

Acceptance. The site's documented acceptance: the site's curator, Thomas Bloom, marks the problem proved and names Kleitman's solution of Problem 447 in the commentary as the reason the statement is true, and the Problem 447 page records both the theorem and its consequence for this problem; that is the reviewed evidence. The paper appeared in an AMS proceedings volume (Crossref record), which attests publication and not refereeing, so refereed is not listed. The reduction from the bound to this problem rests on Erdős's published 1965 attestation, the curator's commentary and the unaudited Lean development above, and no refereed publication of it is cited. The reduction has not been derived or reviewed here, and Kleitman's paper is not held; the problem page states the reopening condition, a copy of the paper.

Depends on. No page of this wiki.