---

Claim. The answer to Problem 277 is yes: for every real $c$ there is a positive integer $n$ with $\sigma(n)>cn$ such that no covering system has as its moduli distinct divisors of $n$ greater than $1$. This is the theorem of J. A. Haight, Covering systems of congruences, a negative result, which the site's commentary credits with the affirmative answer; the theorem is stated here as the commentary states it, and the paper is not held in the library. In the language of the follow-up question Erdős asked in [Er80], with $f(x)$ the largest value of $\sigma(m)/m$ over $m<x$ whose divisors do not form a covering system, Haight's theorem says that $f(x)\to\infty$. A second proof, of a quantitative strengthening, is recorded on the claim page of Filaseta, Ford, Konyagin, Pomerance and Yu.

Erdős's follow-up question, as the site states it, asks whether $f(x)=o(\log\log x)$. Filaseta, Ford, Konyagin, Pomerance and Yu proved $f(x)\ge(1+o(1))\sqrt{\log\log x}$ in the paper held as FFKPY 2007. A comment on the site's thread (2025-09-13) observes that Hough's theorem, held as Hough 2015, that every covering system with distinct moduli has a modulus below an absolute constant $C$ answers the follow-up question negatively: let $n$ be the least common multiple of the integers up to $y$ all of whose prime factors exceed $C$; then every divisor of $n$ above $1$ exceeds $C$, so these divisors cannot be the moduli of a covering system, while $\sigma(n)/n\gg\log y\gg\log\log n$, so $f(x)\gg\log\log x$ and $f(x)$ is not $o(\log\log x)$. The site's commentary records the consequence as $f(x)=(1+o(1))\log\log x$, which is stronger than this argument supports: by Mertens's theorem the construction gives $\sigma(n)/n\sim e^{\gamma}\prod_{p\le C}(1-1/p)\log\log n$, a constant of order $1/\log C$, while Gronwall's theorem bounds $f(x)$ above by $(e^{\gamma}+o(1))\log\log x$; the constant $1$ is not established by it.

Depends on. Nothing in this wiki.

Acceptance. Refereed: Mathematika 26 (1979), no. 1, 53--61, doi:10.1112/s0025579300009608; the Crossref record dates the issue to June 1979, filled to the first of the month for this page's name. Reviewed: the site's curator, Thomas Bloom, credits Haight with the affirmative answer in the problem's commentary and labels the problem proved (page last edited 10 April 2026; as of 2026-10-07 its discussion thread carried one comment, the 2025 remark on Hough's theorem, and its proof-claim tab was empty).

Formalization. The site's label carries a Lean qualification. The formal-conjectures statement file for the problem carries the category research solved and a formal_proof attribute pointing to line 1294 of src/latest/ErdosProblems/Erdos277.lean in Boris Alexeev's lean-proofs repository at the commit of 2026-09-07 linked above. That file (first added 2026-08-15; 1,364 lines at the pin; Lean and Mathlib v4.33.0) declares itself a formalization of a solution to the problem, names Haight and Filaseta, Ford, Konyagin, Pomerance and Yu as informal authors and Codex and GPT-5.6 Sol as formal authors, and proves erdos_277: for every real $c$ there is $n$ with $\sigma(n)>cn$ such that every StrictCoveringSystem ℤ has a modulus ideal not containing $n$, that is, a modulus not dividing $n$. Its CoveringSystem structure is a finite family of residue classes covering the ring with every modulus ideal nonzero and proper, so the moduli exceed $1$, and the strict variant requires pairwise distinct modulus ideals, matching the statement's distinct divisors. The file's header says the proof uses the finite residual-density estimate of Filaseta, Ford, Konyagin, Pomerance and Yu, and it ends with #print axioms without the printed output. The formal-conjectures file states the same proposition under answer(True). The file is linked here because it names Haight's theorem as the statement it proves and Haight as an informal author; since its argument is that of Filaseta, Ford, Konyagin, Pomerance and Yu, it is linked on their claim page as well. This corpus has not built or audited the development, so formalized is not listed as evidence.