Vela Mathematics Program: problems

Narrowed toopen ×source:erdos-problems ×Clear all

Problem ledger

604 problems · 2/13Number SourcesGraph view

declared openerdos:102

Erdős problem 102

geometryN/A

declared openerdos:103

Erdős problem 103

geometrydistancespossible

declared open · $100erdos:104

Erdős problem 104

geometryA003829

declared open · formalizederdos:108

True ↔ ∀ r ≥ 4, ∀ k ≥ 2, ∃ f, ∀ (V : Type u) (G : SimpleGraph V), Nonempty V → ↑f ≤ G.chromaticNumber → ∃ H, H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k

graph theorychromatic numbercyclespossible2 sources

declared openerdos:111

Erdős problem 111

graph theorychromatic numberset theoryN/A

declared openerdos:112

Erdős problem 112

graph theoryramsey theorypossible

declared openerdos:117

Erdős problem 117

group theorypossible

declared open · formalized · $100erdos:120

True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A

combinatoricsN/A3 sources

declared openerdos:122

Erdős problem 122

number theoryN/A

declared open · formalizederdos:124

∀ {D : Finset ℕ}, (∀ d ∈ D, 3 ≤ d) → (∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ d ∈ D, Erdos124.sumsOfDistinctPowers d 0) → 1 ≤ ∑ d ∈ D, (↑d - 1)⁻¹

number theorybase representationsN/A4 sources

declared open · formalized · $250erdos:126

True ↔ ∀ (f : ℕ → ℕ), Erdos126.IsMaximalAddFactorsCard f → Filter.Tendsto (fun n => ↑(f n) / Real.log ↑n) Filter.atTop Filter.atTop

number theorypossible2 sources

declared openerdos:129

Erdős problem 129

graph theoryramsey theorypossible

declared open · formalizederdos:130

For an infinite planar set in strong general position, how large can the chromatic and clique numbers of its positive-integer-distance graph be - in particular, can the chromatic number be infinite? Yes: there is such a set, no three collinear and no four concyclic, with infinite chromatic number.

graph theorychromatic numberN/A4 sources

declared openerdos:131

Let

F(N)

be the maximal size of

A\subseteq\{1,\ldots,N\}

such that no

a\in A

divides the sum of any nonempty subset of

A\setminus\{a\}

. Estimate

F(N)

. The lower bound

F(N)\gg N^{1/5}

is classical, from constructions of Erdős and Csaba, and every non-dividing set is non-averaging, which gave

F(N)\leq N^{1/4+o(1)}

. The claimed new result is the matching upper bound

F(N)\leq N^{1/5+o(1)}

, obtained by running the Pham-Zakharov density-increment argument one dimension lower through a projective normalization, hence

F(N)=N^{1/5+o(1)}

number theoryA0680632 sources

declared open · $100erdos:132

Erdős problem 132

distancesN/A

declared open · formalizederdos:137

sorry ↔ ∀ k ≥ 3, ∀ (n : ℕ), ¬(∏ x ∈ Finset.Ioc n (n + k), x).Powerful

number theoryN/A2 sources

declared open · formalized · $500erdos:138

W(k)

is the least

N

such that every two-colouring of

\{1, \dots, N\}

contains a monochromatic

k

-term arithmetic progression, must

W(k+1) - W(k) \to \infty

additive combinatoricsA0053464 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 · formalized · $500erdos:143

True ↔ ∀ (A : Set ℝ), Erdos143.WellSeparatedSet A → Filter.liminf (fun x => ↑(A ∩ Set.Icc 1 x).ncard / x) Filter.atTop = 0

primitive setsN/A2 sources

declared open · formalizederdos:145

True ↔ ∀ α ≥ 0, ∃ β, Filter.Tendsto (fun x => 1 / x * ∑ n ∈ Erdos145.A x, (↑(Erdos145.s (n + 1)) - ↑(Erdos145.s n)) ^ α) Filter.atTop (nhds β)

number theoryA0051172 sources

declared openerdos:148

Erdős problem 148

number theoryunit fractionsA076393 · A006585

declared openerdos:149

Erdős problem 149

graph theoryN/A

declared openerdos:151

Erdős problem 151

graph theorypossible

declared open · formalizederdos:153

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

sidon setsN/A2 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 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 open · $250erdos:165

Erdős problem 165

graph theoryramsey theoryA0007912 sources

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 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 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 openerdos:181

Erdős problem 181

graph theoryramsey theorypossible

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 openerdos:187

Erdős problem 187

additive combinatoricsramsey theoryN/A

declared open · formalizederdos:188

IsLeast Erdos188.s sorry

geometryramsey theoryN/A2 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 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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science