Vela Mathematics Program: problems

Problem ledger

1,217 problems · 23/25Number SourcesGraph view

declared open · formalizederdos:1101

Does there exist a good pairwise-coprime sequence

u_n

with

\sum 1/u_n < \infty

and polynomial growth? What if one only requires

u_n \le e^{o(n)}

number theoryN/A4 sources

declared solved (Lean) · formalizederdos:1102

∀ (A : ℕ → ℕ), StrictMono A → Erdos1102.HasPropertyP (Set.range A) → Filter.Tendsto (fun j => ↑(A j) / ↑j) Filter.atTop Filter.atTop

number theoryN/A5 sources

declared openerdos:1103

Erdős problem 1103

number theoryA392164

declared open · formalizederdos:1104

∃ c₁, 0 < c₁ ∧ c₁ ≤ 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, c₁ * √↑n / √(Real.log ↑n) ≤ ↑(Erdos1104.triangleFreeMaxChromatic n)

graph theorychromatic numberA2925282 sources

declared proved · formalizederdos:1105

True ↔ ∀ (k : ℕ), 3 ≤ k → (fun n => ↑((SimpleGraph.cycleGraph k).antiRamseyNum n) - ((↑k - 2) / 2 + 1 / (↑k - 1)) * ↑n) =O[Filter.atTop] fun x => 1

graph theoryramsey theorypossible3 sources

declared open · formalizederdos:1106

True ↔ Filter.Tendsto (fun n => (∏ i ∈ Finset.Icc 1 n, Erdos1106.p i).primeFactors.card) Filter.atTop Filter.atTop

number theoryA194259 · A1942602 sources

declared open · formalizederdos:1107

∀ r ≥ 2, ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1107.SumOfRPowerful r n

number theorypowerfulA056828 · A392342 · A392343 · possible2 sources

declared open · formalizederdos:1108

True ↔ ∀ k ≥ 2, {a | a ∈ Erdos1108.FactorialSums ∧ ∃ m, m ^ k = a}.Finite

number theoryfactorialsA051761 · A115645 · A0254942 sources

declared openerdos:1109

Erdős problem 1109

number theoryA392164 · A392165

declared open · formalizederdos:1110

True ↔ ∀ (p q : ℕ), q < p → 2 ≤ q → p.Coprime q → ¬(p = 3 ∧ q = 2) → {n | n.Coprime (p * q) ∧ ¬Erdos1110.Representable p q n}.Infinite

number theorypossible2 sources

declared openerdos:1111

Erdős problem 1111

graph theorypossible

declared open (Lean)erdos:1112

Erdős problem 1112

additive combinatoricsN/A

declared open · formalizederdos:1113

sorry ↔ ∃ k, k.IsSierpinskiNumber ∧ ¬Erdos1113.HasFinitePrimeCoveringSet k

number theorycovering systemsA0763362 sources

declared provederdos:1114

Erdős problem 1114

analysispolynomialsN/A

declared solvederdos:1115

Erdős problem 1115

analysisN/A

declared solvederdos:1116

Erdős problem 1116

analysisN/A

declared openerdos:1117

Erdős problem 1117

analysisN/A

declared solvederdos:1118

Erdős problem 1118

analysisN/A

declared independent · formalizederdos:1119

True ↔ ∀ (m : Cardinal.{0}), Cardinal.aleph0 < m → m < Cardinal.continuum → ∀ (F : Set (ℂ → ℂ)), (∀ f ∈ F, Differentiable ℂ f) → (∀ (z₀ : ℂ), Cardinal.mk ↑{y | ∃ f ∈ F, f z₀ = y} ≤ m) → Cardinal.mk ↑F ≤ m

analysisset theoryN/A2 sources

declared openerdos:1120

Erdős problem 1120

analysisN/A

declared proved (Lean) · formalizederdos:1121

∀ {n : ℕ} (c : Fin n → EuclideanSpace ℝ (Fin 2)) (r : Fin n → ℝ), (∀ (i : Fin n), 0 < r i) → (∀ (v : EuclideanSpace ℝ (Fin 2)) (t : ℝ), v ≠ 0 → (∀ (i : Fin n), ∀ p ∈ Metric.closedBall (c i) (r i), inner ℝ v p ≠ t) → (∀ (i : Fin n), inner ℝ v (c i) < t) ∨ ∀ (i : Fin n), t < inner ℝ v (c i)) → ∃ z, ⋃ i, Metric.closedBall (c i) (r i) ⊆ Metric.closedBall z (∑ i, r i)

geometryN/A5 sources

declared openerdos:1122

Erdős problem 1122

number theoryN/A

declared independent · $100erdos:1123

Erdős problem 1123

algebraN/A

declared provederdos:1124

Erdős problem 1124

geometryN/A

declared proved (Lean) · formalizederdos:1125

True ↔ ∀ (f : ℝ → ℝ), (∀ (x h : ℝ), h > 0 → 2 * f x ≤ f (x + h) + f (x + 2 * h)) → Monotone f

analysisN/A5 sources

declared proved (Lean) · formalizederdos:1126

True ↔ ∀ (f : ℝ → ℝ), (∀ᵐ (p : ℝ × ℝ) ∂MeasureTheory.volume.prod MeasureTheory.volume, f (p.1 + p.2) = f p.1 + f p.2) → ∃ h, (∀ (x y : ℝ), h (x + y) = h x + h y) ∧ ∀ᵐ (x : ℝ), f x = h x

analysisN/A5 sources

declared independenterdos:1127

Erdős problem 1127

geometrydistancesset theoryN/A

declared disproved · formalized · $50erdos:1128

False ↔ ∀ (A B C : Type), Cardinal.mk A = Cardinal.aleph 1 → Cardinal.mk B = Cardinal.aleph 1 → Cardinal.mk C = Cardinal.aleph 1 → ∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, Cardinal.mk ↑A₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑B₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑C₁ = Cardinal.aleph 0 ∧ Erdos1128.IsMonochromaticBox f A₁ B₁ C₁

set theoryramsey theoryhypergraphsN/A2 sources

declared provederdos:1129

Erdős problem 1129

analysispolynomialsN/A2 sources

declared provederdos:1130

Erdős problem 1130

analysispolynomialsN/A2 sources

declared openerdos:1131

Erdős problem 1131

analysispolynomialsN/A2 sources

declared openerdos:1132

Erdős problem 1132

analysispolynomialsN/A2 sources

declared open · formalizederdos:1133

Must every sufficiently large node set admit bounded labels that force any polynomial fitting almost all labels at degree below

(1+\varepsilon)n

to have arbitrarily large uniform norm? Claimed via Beurling density for Bernstein spaces.

analysispolynomialsN/A4 sources

declared disproved (Lean) · £10erdos:1134

Erdős problem 1134

number theoryA1856613 sources

declared open · formalized · $500erdos:1135

∀ n > 0, ∃ m, CollatzConjecture.collatzStep^[m] n = 1

number theoryA006370 · A0089082 sources

declared proved (Lean) · formalizederdos:1136

True ↔ ∃ A, 1 / 3 < A.lowerDensity ∧ Erdos1136.AvoidsPowersOfTwo A

number theoryN/A5 sources

declared open · formalizederdos:1137

True ↔ Filter.Tendsto (fun x => ↑((Finset.range x).sup fun n => primeGap n * primeGap (n - 1)) / ↑((Finset.range x).sup primeGap) ^ 2) Filter.atTop (nhds 0)

number theoryprimesA083550 · A0052502 sources

declared disproved (Lean) · formalizederdos:1138

False ↔ ∀ C > 1, Asymptotics.IsEquivalent Erdos1138.snd_gt_half_fst (Erdos1138.primeCount_Ioc_mul_const C) fun x => match x with | (x, y) => C * ↑(Erdos1138.sup_primeGap x) / Real.log y

number theoryprimespossible6 sources

declared open · formalizederdos:1139

True ↔ Filter.limsup (fun k => (↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) (k + 1)) - ↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) k)) / ↑(Real.log (↑k + 1))) Filter.atTop = ⊤

number theoryprimesA037143 · A1010413 sources

declared disprovederdos:1140

Erdős problem 1140

number theorypossible

declared disproved (Lean) · formalizederdos:1141

False ↔ Infinite ↑{n | Erdos1141.Erdos1141Prop n}

number theoryprimesA2145836 sources

declared open · formalizederdos:1142

sorry ↔ Infinite ↑{n | Erdos1142.Erdos1142Prop n}

number theoryprimesA0396692 sources

declared openerdos:1143

Erdős problem 1143

number theoryprimesN/A2 sources

declared openerdos:1144

Erdős problem 1144

number theoryprobabilityN/A

declared open · formalizederdos:1145

True ↔ Erdos1145.Erdos1145Prop

additive combinatoricsadditive basisN/A2 sources

declared open · formalizederdos:1146

True ↔ Erdos1146.IsEssentialComponent {k | ∃ m n, k = 2 ^ m * 3 ^ n}

number theorypossible2 sources

declared disprovederdos:1147

Erdős problem 1147

irrationaladditive basisN/A

declared proved (Lean) · formalizederdos:1148

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1148.Erdos1148Prop n

number theoryA390380 · A3931686 sources

declared provederdos:1149

Erdős problem 1149

number theoryN/A

declared open · formalizederdos:1150

True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (P : Polynomial ℂ), (∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1) → P.natDegree = n → ⨆ z, ‖Polynomial.eval (↑z) P‖ > (1 + c) * √↑n

analysispolynomialsN/A2 sources

Problems · Vela Mathematics Program

Problem ledger