Vela Mathematics Program: problems

Narrowed toproved ×source:erdos-problems ×Clear all

Problem ledger

210 problems · 1/5Number SourcesGraph view

declared proved · formalized · $10000erdos:4

True ↔ ∀ C > 0, Erdos4.Erdos4For C

number theoryprimesA0023862 sources

declared proved · formalized · $100erdos:6

{n | primeGap n < primeGap (n + 1) ∧ primeGap (n + 1) < primeGap (n + 2)}.Infinite

number theoryprimesA3352772 sources

declared proved · formalized · $100erdos:13

∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos13.IsForbiddenTripleFree A → ↑A.card ≤ ↑N / 3 + C

number theoryA0022642 sources

declared proved · $500erdos:21

Erdős problem 21

combinatoricsintersecting familyA3915992 sources

declared proved · formalizederdos:22

True ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ G, G.CliqueFree 4 ∧ ↑G.indepNum ≤ ε * ↑n ∧ ↑n ^ 2 / 8 ≤ ↑G.edgeFinset.card

graph theorypossible2 sources

declared proved · $100erdos:29

Erdős problem 29

number theoryadditive basisN/A

declared provederdos:35

Erdős problem 35

number theoryadditive basisN/A

declared proved · formalizederdos:48

True ↔ {(n, m) | n.totient = (ArithmeticFunction.sigma 1) m}.Infinite

number theoryN/A2 sources

declared provederdos:49

Erdős problem 49

number theoryprimesA365339 · A365474

declared provederdos:53

Erdős problem 53

number theoryadditive combinatoricspossible

declared provederdos:57

Erdős problem 57

graph theorychromatic numbercyclesN/A

declared provederdos:58

Erdős problem 58

graph theorychromatic numbercyclesN/A

declared provederdos:63

Erdős problem 63

graph theorychromatic numbercyclesN/A

declared proved · formalized · $500erdos:67

∀ (f : ℕ → ↥{-1, 1}) (C : ℝ), 0 < C → ∃ d ≥ 1, ∃ m ≥ 1, C < |∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))|

discrepancyA181740 · A2376952 sources

declared proved · formalizederdos:69

Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + 2)) / 2 ^ (n + 2))

number theoryirrationalityA2621532 sources

declared proved · $100erdos:72

Erdős problem 72

graph theorycyclesN/A

declared provederdos:73

Erdős problem 73

graph theoryN/A

declared provederdos:76

Erdős problem 76

graph theoryramsey theoryA060407

declared provederdos:79

Erdős problem 79

graph theoryramsey theoryN/A

declared proved · $500erdos:83

Erdős problem 83

combinatoricsA071799 · A387635

declared proved · $100erdos:88

Erdős problem 88

graph theoryramsey theoryN/A

declared proved · $500erdos:95

Erdős problem 95

geometryconvexdistancespossible

declared proved · formalizederdos:109

∀ (A : Set ℕ), A.upperDensity > 0 → ∃ B C, B.Infinite ∧ C.Infinite ∧ B + C ⊆ A

additive combinatoricsN/A2 sources

declared provederdos:116

Erdős problem 116

polynomialsanalysisN/A

declared provederdos:127

Erdős problem 127

graph theorypossible

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 proved · $250erdos:144

Erdős problem 144

number theorydivisorsA005279

declared proved · formalizederdos:152

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

sidon setsN/A4 sources

declared provederdos:157

Erdős problem 157

sidon setsN/A

declared provederdos:163

Erdős problem 163

graph theoryramsey theoryN/A

declared proved · $250erdos:166

Erdős problem 166

graph theoryramsey theoryA059442

declared provederdos:171

Erdős problem 171

additive combinatoricscombinatoricsA156989

declared provederdos:175

Erdős problem 175

number theorybinomial coefficientsN/A

declared provederdos:179

Erdős problem 179

additive combinatoricsarithmetic progressionspossible

declared provederdos:182

Erdős problem 182

graph theorypossible

declared provederdos:185

Erdős problem 185

additive combinatoricsA003142

declared provederdos:191

Erdős problem 191

combinatoricsramsey theoryN/A

declared provederdos:207

Erdős problem 207

combinatoricshypergraphsN/A

declared provederdos:210

Erdős problem 210

geometryA003034

declared proved · $100erdos:211

Erdős problem 211

geometryN/A

declared provederdos:215

Erdős problem 215

geometryN/A

declared proved · formalizederdos:219

∅ ∉ Erdos219.primeArithmeticProgressions

number theoryadditive combinatoricsprimesA005115 · A113827 · A1235562 sources

declared proved · $500erdos:220

Erdős problem 220

number theoryA322144

declared provederdos:225

Erdős problem 225

analysisN/A

declared proved · formalizederdos:228

True ↔ ∃ c₁ c₂, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p, p.degree = ↑n ∧ (∀ i ≤ n, p.coeff i = 1 ∨ p.coeff i = -1) ∧ ∀ (z : ℂ), ‖z‖ = 1 → √↑n < c₁ * ‖Polynomial.eval z p‖ ∧ ‖Polynomial.eval z p‖ < c₂ * √↑n

analysispolynomialsN/A2 sources

declared provederdos:232

Erdős problem 232

geometrydistancesN/A

declared provederdos:235

Erdős problem 235

number theoryN/A

declared proved · formalizederdos:239

True ↔ ∀ (f : ℕ → ℝ), (∀ n ≥ 1, f n = 1 ∨ f n = -1) ∧ (∀ (m n : ℕ), m.Coprime n → f (m * n) = f m * f n) ∧ f 1 = 1 → ∃ L, Filter.Tendsto (fun N => (∑ n ∈ Finset.Icc 1 N, f n) / ↑N) Filter.atTop (nhds L)

number theoryN/A2 sources

declared provederdos:240

Erdős problem 240

number theoryprimesN/A

Problems · Vela Mathematics Program

Problem ledger

Search problems.science