Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Problem 277

../

claims/: The 2 claim pages of Problem 277, one per claimant's result; the problem's standing derives from them.


Statement. Is it true that, for every cc, there exists an nn such that σ(n)>cn\sigma(n)>cn but there is no covering system whose moduli all distinct divisors of nn (which are >1>1)?

Status. PROVED (LEAN), the site's label. The status-defining source is Haight's theorem (Mathematika 26 (1979), 53--61, refereed): for every cc some nn has σ(n)>cn\sigma(n)>cn while its divisors above 11 cannot be the moduli of a covering system, so the answer is yes; the claim page is Haight (accepted on the refereed publication and the site's credit). A second, quantitative proof by Filaseta, Ford, Konyagin, Pomerance and Yu (J. Amer. Math. Soc. 2007, refereed) is recorded on their claim page. The site's Lean qualification refers to the Lean proof recorded under Formalization.

Source. erdosproblems.com/277, accessed 2026-09-04; as of 2026-10-07 the page was last edited 10 April 2026, its discussion thread carried one comment (the 2025 remark on Hough's theorem) and its proof-claim tab was empty. Cite as: T. F. Bloom, Erdős Problem #277, https://www.erdosproblems.com/277.

References.

  • [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
  • [FFKPY07] Filaseta, Michael and Ford, Kevin and Konyagin, Sergei and Pomerance, Carl and Yu, Gang, Sieving by large integers and covering systems of congruences. J. Amer. Math. Soc. (2007), 495-517.
  • [Ha79] Haight, J. A., Covering systems of congruences, a negative result. Mathematika 26 (1979), no. 1, 53-61, doi:10.1112/s0025579300009608 (Crossref record, 2026-10-07); not held in the library.
  • [Ho15] Hough, Bob, Solution of the minimum modulus problem for covering systems. Ann. of Math. (2) (2015), 361-382.

Formalization. Statement in formal-conjectures (pinned to the commit of 2026-09-18), whose entry carries the category research solved and a formal_proof attribute pointing to src/latest/ErdosProblems/Erdos277.lean of Boris Alexeev's lean-proofs repository at a pinned commit. That file declares itself a formalization of a solution to the problem, naming Haight and Filaseta, Ford, Konyagin, Pomerance and Yu as informal authors, and is pinned on Haight's and on their claim page; this corpus has not built or audited it, so it gives no formalized evidence.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.