Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Problem 178 asks, for an infinite collection of infinite sets of integers with , whether one function can satisfy
for every . Beck answers yes in Balancing families of integer sequences (1981): for every such family there is a single whose partial sums along each of the first sequences stay below a constant depending only on . The argument has two parts. A finite balancing theorem treats sequences at once: a pigeonhole lemma finds, among enough integer vectors of bounded norm, a nonempty signed subfamily summing to zero, and a hierarchical grouping of the columns of the incidence matrix into signed blocks zeroes out more rows at each level, with the bound for the -th row a product of the first block-size parameters and so independent of the sequences and of the number of rows. A compactness step then extracts one for the whole infinite family from the signings produced for each finite . In the 2017 chapter A discrepancy problem: balancing infinite dimensional vectors Beck made the bound quantitative: the constant can be taken as for every . The chapter reproves the 1981 theorem in this quantitative form and is listed above as a later posting of it; the quantitative bound itself is a refinement and is not the claim this page records.
Scope. Full. The theorem is the site's question as stated, with the sets read as strictly increasing sequences of natural numbers, the reading the formal-conjectures statement also takes.
Depends on. Nothing in this wiki; the result rests on the cited paper alone.
Acceptance. Refereed: the paper appeared in Combinatorica 1 (1981),
no. 3, 209–216. Reviewed: the site's curator, T. F. Bloom, labels the problem
proved and credits the paper in the commentary, noting the 2017 quantitative
bound. A Lean 4 proof of the theorem erdos_178, credited to Matteo Del
Vecchio and the Aristotle system and following Beck's argument, was posted to
the site's thread on 21 April 2026 and is kept in Boris Alexeev's
lean-proofs collection at the pinned commit. formal-conjectures added the
same statement, in its answer form, on 26 June 2026 and tags that copy as its
formal proof. The file's axiom report lists only propext, Classical.choice
and Quot.sound. This corpus has neither built that proof nor audited its
statement, so the formalization is recorded as a posting and not listed as
acceptance evidence. The paper's print date is known only to the month, so
this page is dated to the first day of September 1981; the paper is not held
in the library, and the statement above follows the site's remark, the
citation and the Lean proof's own account of the argument.