Michael Schroeder · Preprint · Version 1 · 22 September 2026 · ORCID 0009-0004-3249-0195

Erdős Problem 278: Formulas and Complexity of Maximum Covered Density

Abstract

Given distinct moduli, how much of the integers can one cover by choosing one residue class for each? When classes with noncoprime moduli can be made disjoint, a signed independence-polynomial formula gives the maximum. An optimal residue vector is explicit if every prime p divides at most p moduli. Nevertheless, evaluating this formula is #P-hard for polynomially bounded squarefree three-prime moduli with a cubic noncoprime graph. Complete-covering decision is NP-hard for distinct moduli; threshold decision is deterministically NP-complete even on prime–modulus incidence trees. In contrast, exact optimization and optimizer recovery are fixed-parameter tractable in noncoprime-graph treewidth, without supplied factorizations. We also disprove an unrestricted extension of a coprime inclusion–exclusion bound. Saturated local trees and convex compression provide exact representations. A scoped Lean companion verifies structural results for supplied coprime coordinates; the complexity classifications and specified arithmetic extensions remain written proofs.

Read the Paper

Companion and Verification Materials

The archive includes the PDF and self-contained LaTeX manuscript, 187 selected Lean source files, nine Python reference and audit modules, five regression suites, an illustration checker, dependency pins, reproduction instructions and verification records.

Start with README.md in the archive, then lean/PUBLICATION_SCOPE.md for the paper-to-theorem mapping. The source-only package excludes build caches, compiled proofs, downloaded dependencies and private working notes.

Citation and file integrity

Schroeder, Michael. Erdős Problem 278: Formulas and Complexity of Maximum Covered Density. Version 1, Zenodo, 2026. DOI: 10.5281/zenodo.22874487. Download the BibTeX citation.

The PDF and ZIP on this site are byte-identical to the published Zenodo files. Download the SHA-256 checksums for both files. The archive also contains a manifest covering its 346 payload files and a verification script.

The manuscript is dated 21 September 2026; its first public release was 22 September 2026. Preparation-time references to a reserved DOI inside the unchanged archive describe the pre-publication checkpoint. The Zenodo record is now public.

What Is Formalized

Lean checks selected structural results for supplied coprime coordinates: the density/Chinese-remainder bridge, Shearer and coprime-disjoint results, saturation, the structural optimization formula and arithmetic realization. Identified arithmetic components of the four-prime counting construction are also included.

The complete paper is not formally verified. The complexity classifications, factorization-free algorithm and runtime bounds, three-prime counting refinement, covering reduction, and deterministic and randomized star reductions remain written proofs. The Python suites supply exact finite checks, not additional Lean theorems.

The companion pins official Lean 4.32.2 and a specific mathlib revision. Its evidence records a same-host source rebuild using pinned external dependency caches, a 3,393-declaration axiom audit, stock-kernel replay and the exact Python checks. This is not an independent-machine test or an external referee report.

The Problem

Erdős Problem 278 asks about the densities left uncovered by residue classes with prescribed distinct moduli. This paper studies the maximum covered density, or equivalently the minimum missed density. It separates choosing the residue classes from evaluating their exact density: even when an optimal choice is explicit, exact evaluation can remain counting-hard.

The results give formulas for structured families, algorithms for bounded noncoprime-graph treewidth, and hardness classifications for restricted inputs. They do not claim that the problem website has accepted Erdős Problem 278 as solved.

Licence and Assistance

The original manuscript, documentation and audit outputs are licensed under CC BY 4.0. Original code, including the Lean and Python sources and build helpers, is licensed under Apache 2.0. Third-party licences and notices are preserved. See RIGHTS.md in the archive for the material-specific allocation.

This work benefited from research assistance by AI systems developed by OpenAI and Anthropic, including support for proof exploration, proof development, and exact computational checks among others.