Vela Mathematics Program: problems

Narrowed toopen ×arithmetic progressions ×Clear all

Problem ledger

15 problemsGraph view

declared open · formalized · $5000erdos:3

True ↔ ∀ (A : Set ℕ), (¬Summable fun a => 1 / ↑↑a) → ∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength ↑k

number theoryadditive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources

declared open · formalizederdos:141

sorry ↔ ∀ k ≥ 3, ∃ s, Erdos141.Set.IsAPAndPrimeProgressionOfLength s k

additive combinatoricsprimesarithmetic progressionsA0065602 sources

declared open · formalized · $10000erdos:142

∀ (k : ℕ), (fun N => ↑(Erdos142.r k N)) =Θ[Filter.atTop] sorry

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030053 sources

declared open · formalizederdos:160

have lower_bound := sorry; (lower_bound =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) ∧ ∀ c > 0, ((fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) → ∀ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_bound

additive combinatoricsarithmetic progressionspossible2 sources

declared openerdos:169

Erdős problem 169

additive combinatoricsarithmetic progressionsA005346

declared openerdos:176

Let

N(k, \ell)

be the least

N

such that every

f : [N] \to \{-1, 1\}

has a

k

-term arithmetic progression

P

with

|\sum_{n \in P} f(n)| \ge \ell

. In particular, is

N(k, 2) \le C^k

additive combinatoricsarithmetic progressionsdiscrepancypossible3 sources

declared openerdos:177

Erdős problem 177

discrepancyarithmetic progressionsN/A

declared open · formalizederdos:195

sorry = sSup {k | ∀ (f : ℤ ≃ ℤ), HasMonotoneAP (⇑f) k}

arithmetic progressionsN/A2 sources

declared open · formalizederdos:196

True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4

arithmetic progressionsN/A2 sources

declared open · formalizederdos:197

True ↔ ∃ A B, IsCompl A B ∧ (∃ f, ¬HasMonotoneAP (Subtype.val ∘ ⇑f) 3) ∧ ∃ g, ¬HasMonotoneAP (Subtype.val ∘ ⇑g) 3

arithmetic progressionsN/A2 sources

declared open · formalizederdos:200

sorry ↔ (fun n => ↑(Erdos200.longestPrimeArithmeticProgressions n)) =o[Filter.atTop] fun n => Real.log ↑n

primesarithmetic progressionsA0051152 sources

declared openerdos:201

Erdős problem 201

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A003005 · possible

declared openerdos:271

Erdős problem 271

additive combinatoricsarithmetic progressionsA005487

declared open · formalizederdos:272

Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos272.maxArithInterCard N)) sorry

additive combinatoricsarithmetic progressionspossible2 sources

declared openerdos:1186

What is the minimum asymptotic density

\delta_k

of monochromatic

k

-term arithmetic progressions in every two-colouring of

\{1, \dots, n\}

? The exact certificate gives

\delta_3 = 117/2192

, matching the known 548-bead colouring.

additive combinatoricsarithmetic progressionspossible2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science