Status
On this page
Status
Topics
Status
On this page
Status
Topics
Let and let be a non-decreasing function of which is always .
Is the lower density of
always ? Is the upper density always for some constant ?
Source: erdosproblems.com/1193
An accepted solution exists. The statement is false.
SOLVED (LEAN). The answer to both questions is no as the statement stands, since and make the set in question all of , of density , so neither conjectured bound holds. The derived standing therefore records a disproof rather than the plain answer the site's label carries: both questions ask whether a bound always holds, and the counterexample refutes each. The counterexample was posted on the site's thread on 2026-04-13 with a Lean file and adopted in the site's commentary, which presumes that Erdős intended restrictions on or not recorded in [Er80]; it is recorded on its claim page (Monticone, 2026) and accepted on the site's documented adoption, not on any review by this project. The label's Lean mark refers to that file and its copy in the lean-proofs repository, listed on the claim page and not built here.