Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 534
claims/: The 1 claim page of Problem 534, one per claimant's result; the problem's standing derives from them.
Statement. What is the largest possible subset which contains such that for all ?
Status. Solved on the site: the curator credits Ahlswede and Khachatrian (1996) with proving Erdős's refined conjecture that the maximum is attained, for some , by the integers up to divisible by one of , where are the prime factors of , after the original guess of Erdős and Graham fell to easy counterexamples; see the claim page. The site notes that the 1973 source printed the condition as , a misprint for . The standing in the frontmatter derives from the claim pages.
Source. erdosproblems.com/534, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #534, https://www.erdosproblems.com/534.
References.
- [AhKh96] Ahlswede, Rudolf and Khachatrian, Levon H., Sets of integers with pairwise common divisor and a factor from a specified set of primes. Acta Arith. 75 (1996), 259-276.
- [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138.
Formalization. The formal-conjectures file
FormalConjectures/ErdosProblems/534.lean,
added on 2026-09-22 at the commit linked here, states the refined conjecture
as erdos_534 with sorry, tags it solved and names as its formal proof the
Lean development in Boris Alexeev's repository of formalized Erdős problems,
which the
claim page
links at a pinned commit. The pull request that added the file records an
outside check: it rebuilt Alexeev's development against the repository's
Mathlib, found the axioms propext, Classical.choice and Quot.sound only,
and compiled a bridge from his theorem to the new statement, whose definitions
coincide with his by rfl. This corpus has built and audited none of it.
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.