Conjectures.io

Number theory

Erdős 142 - lower

Show that rk(N)=ok(N/log⁡N)r_k(N) = o_k(N / \log N), where rk(N)r_k(N) the largest possible size of a subset of {1,…,N}\{1, \dots, N\} that does not contain any non-trivial kk-term arithmetic progression.

References

No one has attempted this yet.

Formal statement

Lean type

∀ (k : ℕ), 1 < k → (fun N => ↑(Erdos142.r k N)) =o[Filter.atTop] fun N => ↑N / Real.log ↑N

What you must prove

import FormalConjectures.ErdosProblems.«142»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos142.erdos_142.variants.lower" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/142.lean

Source type SHA-256
sha256:a3f73a02f0e943bd284c080928f5a62067c273a79ce4fb3b55dd05a781c9f52c
Task id
fc-379fc029-variants-lower-6ff2287ea4-formalized-v1
Task commitment
sha256:cf95a04071dd7c65efd5b1aae958c0d2325e29a427d660761cbb7118397da9a9

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.