Wiki
Wiki

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 A⊆{1,…,N}A\subseteq\{1,\ldots,N\} which contains NN such that gcd(a,b)>1\mathrm{gcd}(a,b)>1 for all a≠b∈Aa\neq b\in A?

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 jj, by the integers up to NN divisible by one of 2q1,…,2qj,q1⋯qj2q_1,\ldots,2q_j,q_1\cdots q_j, where q1<⋯<qrq_1<\cdots<q_r are the prime factors of NN, 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,b)=1(a,b)=1, a misprint for (a,b)>1(a,b)>1. 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.