Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 988
claims/: The 1 claim page of Problem 988, one per claimant's result; the problem's standing derives from them.
Statement. If is a subset of the unit sphere then define the discrepancy
where the maximum is taken over all spherical caps , and is the appropriately normalised measure of .
Is it true that
as ?
Status. SOLVED, the site's label: Schmidt's 1969 theorem, refereed in Inventiones Mathematicae, answers the question yes in every dimension. The derived standing, solved and proved, is more specific than the site's label, which names no polarity: the accepted claim on the claim page proves the statement.
Source. erdosproblems.com/988, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #988, https://www.erdosproblems.com/988.
References.
- [Ro54] Roth, K. F., On irregularities of distribution. Mathematika (1954), 73-79.
- [Sc69b] Schmidt, Wolfgang M., Irregularities of distribution. IV. Invent. Math. (1969), 55-82.
Formalization. No formal-conjectures statement: the site's indicator
reports no formalized statement and the community database records none. The
file src/latest/ErdosProblems/Erdos988.lean of the GitHub repository
plby/lean-proofs declares itself a Lean formalization of a solution to the
problem, with Schmidt as its informal author and Codex and GPT-5.6 Sol as its
formal authors; it proves for every finite
and from it the divergence of the minimum discrepancy, by a
Stolarsky positive-kernel argument rather than Schmidt's. It is linked,
pinned, from
Schmidt's claim page,
and is not built or audited here, so no claim carries formalized
evidence.
Progress
Not yet compiled.
Known Results
Not yet compiled.