Combinatorics

Erdős 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

erdosproblems.com/535

Er64 P. Erdős, On a problem in elementary number theory and a combinatorial problem. Math. Comp. (1964), 644–646.
AbHa70 H. L. Abbott and D. Hanson, An extremal problem in number theory. Bull. London Math. Soc. (1970), 324–326.
Er73 P. Erdős, Problems and results on combinatorial number theory, in *A Survey of Combinatorial Theory*, North-Holland, 1973.

No one has attempted this yet.

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-379fc029-erdos535-erdos-535-c15ef11f1d-formalized-v1
Task commitment: sha256:49057fc2fd7a11602d9d6872683f71cb4c0348d9a40fcaeb46d2422f01b0b934

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.