Vela Mathematics Program: problems

Problem ledger

1,217 problems · 4/25Number SourcesGraph view

declared openerdos:151

Erdős problem 151

graph theorypossible

declared proved · formalizederdos:152

True ↔ Filter.Tendsto Erdos152.f Filter.atTop Filter.atTop

sidon setsN/A4 sources

declared open · formalizederdos:153

True ↔ Filter.Tendsto Erdos153.f Filter.atTop Filter.atTop

sidon setsN/A2 sources

declared proved (Lean) · formalizederdos:154

True ↔ ∀ (m : ℕ), 2 ≤ m → ∀ (N : ℕ → ℕ) (A : ℕ → Finset ℕ), Filter.Tendsto (fun k => ↑(N k)) Filter.atTop Filter.atTop → (∀ (k x : ℕ), x ∈ A k → x ≤ N k) → (∀ (k : ℕ), IsSidon ↑(A k)) → Filter.Tendsto (fun k => ↑(A k).card / √↑(N k)) Filter.atTop (nhds 1) → ∀ i < m, Filter.Tendsto (fun k => ↑{s ∈ A k + A k | s % m = i}.card / ↑(A k + A k).card) Filter.atTop (nhds (1 / ↑m))

sidon setsN/A6 sources

declared open · formalizederdos:155

True ↔ ∀ k ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, Erdos155.F (N + k) ≤ Erdos155.F N + 1

additive combinatoricssidon setsA143824 · A227590 · A0030222 sources

declared open · formalizederdos:156

True ↔ (fun N => ↑(Erdos156.minMaximalSidonSet N)) =O[Filter.atTop] fun N => ↑N ^ (1 / 3)

sidon setsA3823972 sources

declared provederdos:157

Erdős problem 157

sidon setsN/A

declared open · formalizederdos:158

∀ {A : Set ℕ}, Erdos158.B2 1 A ↔ IsSidon A

sidon setsN/A2 sources

declared openerdos:159

Erdős problem 159

graph theoryramsey theorypossible

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 open · $500erdos:161

Erdős problem 161

combinatoricsramsey theorydiscrepancyN/A2 sources

declared openerdos:162

Erdős problem 162

combinatoricsramsey theorydiscrepancyN/A

declared provederdos:163

Erdős problem 163

graph theoryramsey theoryN/A

declared proved (Lean) · formalizederdos:164

True ↔ ∀ (A : Set ℕ), (∀ a ∈ A, 2 ≤ a) → Erdos1196.IsPrimitive A → ∑' (a : ↑A), 1 / (↑↑a * Real.log ↑↑a) ≤ ∑' (p : ↑{p | Nat.Prime p}), 1 / (↑↑p * Real.log ↑↑p)

number theoryprimitive setsA1372455 sources

declared open · $250erdos:165

Erdős problem 165

graph theoryramsey theoryA0007912 sources

declared proved · $250erdos:166

Erdős problem 166

graph theoryramsey theoryA059442

declared falsifiableerdos:167

Erdős problem 167

graph theoryN/A

declared open · formalizederdos:168

Erdos168.F 0 = 0

additive combinatoricsA004059 · A057561 · A094708 · A3864392 sources

declared openerdos:169

Erdős problem 169

additive combinatoricsarithmetic progressionsA005346

declared open · formalizederdos:170

Filter.Tendsto (fun N => ↑(Erdos170.F N) / √↑N) Filter.atTop (nhds sorry)

additive combinatoricsA0466932 sources

declared provederdos:171

Erdős problem 171

additive combinatoricscombinatoricsA156989

declared open · formalizederdos:172

True ↔ ∀ (n : ℕ) (color : ℕ → Fin n) (m : ℕ), ∃ A, A.card ≥ m ∧ ∃ c, ∀ (S : Finset ↥A), S.Nonempty → color (∑ x ∈ S, ↑x) = c ∧ color (∏ x ∈ S, ↑x) = c

additive combinatoricsramsey theoryN/A2 sources

declared openerdos:173

Erdős problem 173

geometryramsey theoryN/A

declared openerdos:174

Erdős problem 174

geometryramsey theoryN/A

declared provederdos:175

Erdős problem 175

number theorybinomial coefficientsN/A

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 proved (Lean) · formalizederdos:178

True ↔ ∀ (a : ℕ → ℕ → ℕ), (∀ (i : ℕ), StrictMono (a i)) → ∃ f, (∀ (n : ℕ), f n = 1 ∨ f n = -1) ∧ ∀ (d : ℕ), ∃ C, ∀ (m i : ℕ), i < d → |∑ j ∈ Finset.range m, f (a i j)| ≤ ↑C

discrepancyN/A5 sources

declared provederdos:179

Erdős problem 179

additive combinatoricsarithmetic progressionspossible

declared open (Lean) · formalizederdos:180

For every finite family

\mathcal{F}

of graphs, is there a single

G \in \mathcal{F}

with

\mathrm{ex}(n;G) \ll_{\mathcal{F}} \mathrm{ex}(n;\mathcal{F})

? A counterexample refutes the Erdős-Simonovits compactness conjecture.

graph theoryturan numberN/A4 sources

declared openerdos:181

Erdős problem 181

graph theoryramsey theorypossible

declared provederdos:182

Erdős problem 182

graph theorypossible

declared open (Lean) · formalized · $250erdos:183

Let

R(3;k)

be the least

n

such that every

k

-colouring of the edges of

K_n

contains a monochromatic triangle. Determine

\lim_{k\to\infty} R(3;k)^{1/k}

(a $250 Erdős prize problem). A superexponential lower bound resolves the problem: the limit is infinite.

graph theoryramsey theoryA0033233 sources

declared open · formalizederdos:184

∃ f, (f =O[Filter.atTop] fun n => ↑n) ∧ ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V), ∃ D, (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) ∧ Erdos184.IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

graph theorycyclespossible2 sources

declared provederdos:185

Erdős problem 185

additive combinatoricsA003142

declared solvederdos:186

Erdős problem 186

additive combinatoricsA389784

declared openerdos:187

Erdős problem 187

additive combinatoricsramsey theoryN/A

declared open · formalizederdos:188

IsLeast Erdos188.s sorry

geometryramsey theoryN/A2 sources

declared disproved (Lean) · formalizederdos:189

False ↔ Erdos189.Erdos189For (fun a b c d => (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧ (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧ (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction) fun a b c d => dist a b * dist b c

geometryramsey theoryN/A5 sources

declared solvederdos:190

Erdős problem 190

additive combinatoricsarithmetic progressionspossible

declared provederdos:191

Erdős problem 191

combinatoricsramsey theoryN/A

declared solved (Lean)erdos:192

Erdős problem 192

arithmetic progressionscombinatoricsN/A3 sources

declared open · formalizederdos:193

True ↔ ∀ (S : Set (Fin 3 → ℤ)), S.Finite → ∀ (a : ℕ → Fin 3 → ℤ), Erdos193.IsSWalk S a → (Set.range a).Infinite → Erdos193.HasCollinearTriple ℚ (Set.range fun n => Int.cast ∘ a n)

geometryA2312552 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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science