---

Claim. For complex numbers $z_1,\ldots,z_n$ with $\lvert z_i\rvert>1$ and any closed disc $D$ of radius $1$, at most $\binom n{\lfloor n/2\rfloor}$ of the $2^n$ sign choices $\epsilon\in\{-1,1\}^n$ have $\sum_i\epsilon_iz_i\in D$, sign choices counted with multiplicity even when their sums coincide. This is Theorem I of D. J. Kleitman, On a lemma of Littlewood and Offord on the distribution of certain sums, Math. Z. 90 (1965), no. 4, 251–259, proved through a two-color Sperner theorem and symmetric chain decompositions. Scaling the finitely many counted configurations by a small strict margin gives the same bound for $\lvert z_i\rvert\ge1$ and an open unit disc, the finite scaling consequence, which is the exact formulation of [[problems/analysis/E0498/_index|Problem 498]] with $D$ read as an open disc, the reading of Erdős's 1945 formulation, which the site's formal statement also uses. The bound is sharp, by equal real coefficients. The closed-disc assertion with moduli merely at least one is false already at $n=1$, as the consequence's page records; the claim is full for the open-disc formulation and for the closed disc under strict moduli, and no more.

Acceptance. The paper is a refereed journal publication, received 19 November 1964 and published in the August 1965 issue according to the publisher's record, the refereed evidence; the record gives no day, and this page is dated to the first day of that month. The site's curator, Thomas Bloom, labels the problem proved and credits the affirmative solution to this paper, the reviewed evidence. Kleitman's 1970 generalization to Hilbert spaces has its own claim page. The corpus's reconstruction of the complete plane proof on the source's result pages is author-recorded and awards no evidence here.

Formalization. The linked Lean file in the plby/lean-proofs repository, pinned at the commit in the link, declares itself a Lean formalization of a solution to Problem 498, names Kleitman as its informal author and names Gemini Flash, Gemini Pro, Claude Opus, Aristotle and the forum user JoshuaB as its formal authors. Its theorem erdos_498 (line 2006) states Theorem I's form, strict moduli $1<\lVert z_i\rVert$ and the closed ball Metric.closedBall c 1, counting integer sign vectors, under the toolchain leanprover/lean4:v4.33.0 with Mathlib v4.33.0; its 2,060 lines contain no sorry, axiom, native_decide or admit token. The statement file in google-deepmind/formal-conjectures, which states the open-disc form with moduli at least one, names this file as the formal proof and is itself a statement with sorry, so it is not a formalization link. The three live-editor sources posted in the site's discussion thread are recorded on the problem page under "Public formalization evidence". This corpus has not built or kernel-checked any of them, so no formalized evidence is listed.

Depends on. The cited paper and, for the open-disc formulation with moduli at least one, the finite scaling consequence.