Combinatorics · Last catalog review 26 Jul 2026

Erdős Problem 535

Let

r \geq 3

, and let

f_r(N)

denote the size of the largest subset of

\{1,\ldots,N\}

such that no subset of size

r

has the same pairwise greatest common divisor between all elements. Erdős [Er64] proved that

f_3(N) > N^{c/\log\log N}

for some constant

c > 0

, and conjectured this should also be an upper bound; here we state the conjectural upper bound for all

r \geq 3

. See also [536].

References

Published 10 Jul 2026Never attempted

Formal statement

Lean type

∀ r ≥ 3, ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos535.f r N) ≤ ↑N ^ (c / Real.log (Real.log ↑N))

What you must prove

import FormalConjectures.ErdosProblems.«535»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos535.erdos_535" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/535.lean

Source type SHA-256: sha256:0681c713f97422d3f50a03ba25c825135ae3ca9a618dc041add3eeb402e64fb8
Task id: fc-e923379e-erdos535-erdos-535-3166c847c0-formalized-v1
Task commitment: sha256:8d74e93a299e9c623155508b8439204c7a9a9a0b595bf9f1efa06d1e9a045ac2

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.