Vela Mathematics Program: problems

Narrowed toarithmetic progressions ×Clear all

Problem ledger

27 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 proved · formalized · $1000erdos:139

∀ (k : ℕ), 1 < k → Filter.Tendsto (fun N => ↑(Erdos139.r k N) / ↑N) Filter.atTop (nhds 0)

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources

declared proved · $500erdos:140

Erdős problem 140

additive combinatoricsarithmetic progressionsA003002

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 provederdos:179

Erdős problem 179

additive combinatoricsarithmetic progressionspossible

declared solvederdos:190

Erdős problem 190

additive combinatoricsarithmetic progressionspossible

declared solved (Lean)erdos:192

Erdős problem 192

arithmetic progressionscombinatoricsN/A3 sources

declared disproved (Lean) · formalizederdos:194

False ↔ ∀ k ≥ 3, ∀ (r : ℝ → ℝ → Prop), IsStrictTotalOrder ℝ r → ∃ s, s.IsAPOfLength k ∧ (List.Pairwise r s ∨ List.Pairwise (flip r) s)

arithmetic progressionsN/A5 sources

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 disproved (Lean) · formalizederdos:198

∀ (V : Type u_1) [inst : AddCommGroup V] [Module ℚ V], ∃ X, (∀ (Y : Set V), Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧ ∀ (Y : Set V), Y.IsAPOfLength 3 → (X ∩ Y).ncard ≤ 2

additive combinatoricssidon setsarithmetic progressionsN/A5 sources

declared disproved (Lean) · formalizederdos:199

False ↔ ∀ (A : Set ℝ), ThreeAPFree A → ∃ S, S.IsAPOfLength ⊤ ∧ S ⊆ Aᶜ

arithmetic progressionsN/A5 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 proved · formalizederdos:219

∅ ∉ Erdos219.primeArithmeticProgressions

number theoryadditive combinatoricsprimesA005115 · A113827 · A1235562 sources

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 provederdos:984

Erdős problem 984

arithmetic progressionsadditive combinatoricsN/A

declared solvederdos:1185

Erdős problem 1185

additive combinatoricsarithmetic progressionsN/A

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

declared solvederdos:1187

Erdős problem 1187

number theoryprimesadditive combinatoricsN/A3 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science