Vela

erdős #139 · Szemerédi's theorem

← #138 · #140 (packet.json; erdosproblems.com)

Let be the size of the largest subset of which does not contain a non-trivial -term arithmetic progression. Prove that .

Worked, still open.

additive combinatorics · solved · prize $1000 · formalized (Lean) · 0 attempts

machinery: additive-combinatorics,arithmetic-progressions,Szemeredi-theorem,density-regularity,prime-distribution

use this record

vela registry pull vfr_37aec80d874a0239
vela reproduce examples/erdos-problems

formal

AMS 5 11 · solved (literature)

theorem erdos_139 (k : ℕ) (hk : 1 < k) :
    Filter.Tendsto (fun N => (r k N / N : ℝ)) Filter.atTop (𝓝 0)
formal-conjectures/139.lean ↗

oeis

status

solved

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 b80f229871681584dd2cf8341b5c92e16d989753e7bfacae4916256b319a9ecc

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.