Vela Mathematics Program: problems

Problem ledger

1,217 problems · 5/25Number SourcesGraph view

declared openerdos:201

Erdős problem 201

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A003005 · possible

declared solved (Lean) · formalizederdos:202

∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos202.f N) = ↑N * scaleL N ^ (-1 + o N)

covering systemsA3899756 sources

declared open · formalizederdos:203

True ↔ ∃ m, m.Coprime 6 ∧ ∀ (k l : ℕ), ¬Nat.Prime (2 ^ k * 3 ^ l * m + 1)

primescovering systemsN/A2 sources

declared disproved (Lean) · formalizederdos:204

False ↔ ∃ n a, have D := {d | d ∣ n ∧ d > 1}; (∀ (x : ℤ), ∃ d ∈ D, x ≡ a d [ZMOD ↑d]) ∧ ∀ d ∈ D, ∀ d' ∈ D, d ≠ d' → (∃ x, x ≡ a d [ZMOD ↑d] ∧ x ≡ a d' [ZMOD ↑d']) → d.gcd d' = 1

covering systemsN/A5 sources

declared disproved (Lean) · formalizederdos:205

False ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos205.IsRepresentable (fun m => Real.log (Real.log ↑m)) n

number theorypossible6 sources

declared disproved (Lean) · formalizederdos:206

False ↔ ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), Erdos206.EventuallyGreedy x

number theoryunit fractionsN/A5 sources

declared provederdos:207

Erdős problem 207

combinatoricshypergraphsN/A

declared open · formalizederdos:208

True ↔ ∀ ε > 0, (fun n => ↑(Erdos208.erdos208.s (n + 1)) - ↑(Erdos208.erdos208.s n)) =O[Filter.atTop] fun n => ↑(Erdos208.erdos208.s n) ^ ε

number theoryA005117 · A0762592 sources

declared disproved (Lean) · formalizederdos:209

False ↔ ∀ (d : ℕ), 4 ≤ d → ∀ (A : Finset (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)))), A.card = d → (∀ L ∈ A, Erdos209.IsLine L) → ((↑A).Pairwise fun L₁ L₂ => ¬L₁.Parallel L₂) → (∀ (p : EuclideanSpace ℝ (Fin 2)), Erdos209.pointMultiplicity A p ≤ 3) → Erdos209.HasGallaiTriangle A

geometryN/A4 sources

declared provederdos:210

Erdős problem 210

geometryA003034

declared proved · $100erdos:211

Erdős problem 211

geometryN/A

declared open · formalizederdos:212

True ↔ ∃ u, Dense u ∧ u.Pairwise fun c₁ c₂ => dist c₁ c₂ ∈ Set.range Rat.cast

geometrydistancesN/A2 sources

declared open · formalizederdos:213

True ↔ ∀ n ≥ 4, Erdos213.Erdos213For n

geometrydistancesN/A2 sources

declared proved (Lean) · formalizederdos:214

True ↔ ∀ (S : Set (EuclideanSpace ℝ (Fin 2))), Erdos214.UnitDistanceAvoiding S → ∃ p, (∀ (i : Fin 4), p i ∈ Sᶜ) ∧ Congruent p Erdos214.unitSquare

geometrydistancesN/A5 sources

declared provederdos:215

Erdős problem 215

geometryN/A

declared disprovederdos:216

Erdős problem 216

geometryconvexA381776

declared openerdos:217

Erdős problem 217

geometrydistancespossible

declared open · formalizederdos:218

{n | primeGap (n + 1) ≤ primeGap n}.HasDensity (1 / 2)

number theoryprimesA333230 · A333231 · A0641133 sources

declared proved · formalizederdos:219

∅ ∉ Erdos219.primeArithmeticProgressions

number theoryadditive combinatoricsprimesA005115 · A113827 · A1235562 sources

declared proved · $500erdos:220

Erdős problem 220

number theoryA322144

declared proved (Lean) · formalizederdos:221

True ↔ ∃ A, ((fun N => ↑{a | a ∈ A ∧ a ≤ N}.ncard) =O[Filter.atTop] fun N => ↑N / Real.log ↑N) ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∃ k a, 0 ≤ k ∧ a ∈ A ∧ N = 2 ^ k + a

number theoryadditive basisN/A5 sources

declared openerdos:222

Erdős problem 222

number theorysquaresA001481 · A256435

declared solvederdos:223

Erdős problem 223

geometrydistancespossible

declared proved (Lean) · formalizederdos:224

∀ {d : ℕ} (A : Finset (EuclideanSpace ℝ (Fin d))), A.card = 2 ^ d + 1 → ∃ x y z, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ Erdos224.ObtuseAt x y z

geometryN/A5 sources

declared provederdos:225

Erdős problem 225

analysisN/A

declared proved (Lean) · formalizederdos:226

True ↔ ∃ F, Differentiable ℂ F ∧ (∀ (x : ℝ), (F ↑x).im = 0) ∧ (∀ (g : ℝ →ᵃ[ℝ] ℝ), (fun x => (F ↑x).re) ≠ ⇑g) ∧ Erdos226.PreservesRationality fun x => (F ↑x).re

analysisN/A5 sources

declared disprovederdos:227

Erdős problem 227

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

True ↔ ∀ (S : ℕ → Set ℂ), (∀ (n : ℕ), derivedSet (S n) = ∅) → ∃ f, Transcendental (Polynomial ℂ) f ∧ Differentiable ℂ f ∧ ∀ n ≥ 1, ∃ k, ∀ z ∈ S n, iteratedDeriv k f z = 0

analysisiterated functionsN/A5 sources

declared disprovederdos:230

Erdős problem 230

analysispolynomialsN/A

declared disproved (Lean)erdos:231

Erdős problem 231

combinatoricsN/A3 sources

declared provederdos:232

Erdős problem 232

geometrydistancesN/A

declared open · formalizederdos:233

(fun N => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) =O[Filter.atTop] fun N => ↑N * Real.log ↑N ^ 2

number theoryprimesA0747413 sources

declared open · formalizederdos:234

True ↔ ∃ f, Continuous f ∧ ∀ (c : NNReal), {n | ↑(primeGap n) / Real.log ↑n < ↑c}.HasDensity (f c)

number theoryprimesN/A2 sources

declared provederdos:235

Erdős problem 235

number theoryN/A

declared open · formalizederdos:236

(fun n => ↑(Erdos236.f n)) =o[Filter.atTop] fun n => Real.log ↑n

number theoryprimesA039669 · A1099252 sources

declared proved (Lean)erdos:237

Erdős problem 237

number theoryprimesN/A4 sources

declared open · formalizederdos:238

True ↔ ∀ c₁ > 0, ∀ c₂ > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∃ k, c₁ * Real.log x < ↑k ∧ ∃ f m, (∀ (i : Fin k), ↑(f i) ≤ x ∧ f i = Nat.nth Nat.Prime (m + ↑i)) ∧ ∀ (i : Fin (k - 1)), c₂ < primeGap (m + ↑i)

number theoryprimesN/A2 sources

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

declared open · formalized · $100erdos:241

True ↔ Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos241.f N 3)) fun N => ↑N ^ (1 / 3)

additive combinatoricssidon setsA3877042 sources

declared falsifiable · formalizederdos:242

∀ (n : ℕ), 2 < n → ∃ x y z, 1 ≤ x ∧ x < y ∧ y < z ∧ 4 / ↑n = 1 / ↑x + 1 / ↑y + 1 / ↑z

number theoryunit fractionsA073101 · A075245 · A075246 · A075247 · A075248 · A2871162 sources

declared open · formalizederdos:243

∀ (a : ℕ → ℕ), StrictMono a → Filter.Tendsto (fun n => ↑(a n) / ↑(a (n - 1)) ^ 2) Filter.atTop (nhds 1) → (Summable fun x => 1 / ↑(a x)) → ∀ᶠ (n : ℕ) in Filter.atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1

number theoryA0000582 sources

declared open · formalizederdos:244

True ↔ ∀ C > 1, 0 < {x | ∃ p k, ∃ (_ : Nat.Prime p), p + ⌊C ^ k⌋₊ = x}.lowerDensity

number theoryprimesN/A2 sources

declared proved · formalizederdos:245

True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard / N) Filter.atTop (nhds 0) → 3 ≤ Filter.limsup (fun N => ↑((A + A) ∩ Set.Icc 1 ⌊N⌋₊).ncard / ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard) Filter.atTop

additive combinatoricsN/A2 sources

declared proved (Lean) · formalizederdos:246

∀ (a b : ℕ), 2 ≤ a → 2 ≤ b → a.Coprime b → IsAddComplete (Erdos246.Gamma a b)

number theoryN/A5 sources

declared open · formalizederdos:247

True ↔ ∀ (n : ℕ → ℕ), StrictMono n → Filter.limsup (fun k => ↑(n k) / ↑k.succ) Filter.atTop = ⊤ → Transcendental ℚ (∑' (k : ℕ), 1 / 2 ^ n k)

number theoryirrationalityN/A2 sources

declared proved · formalizederdos:248

∃ C > 0, {n | ∀ k ≥ 1, ↑(ArithmeticFunction.cardDistinctFactors (n + k)) ≤ C * ↑k}.Infinite

number theoryN/A2 sources

declared open · formalizederdos:249

True ↔ Irrational (∑' (n : ℕ), ↑n.totient / 2 ^ n)

number theoryirrationalityA2569362 sources

declared proved · formalizederdos:250

(∀ (x : ℝ), HasSum (fun n => ↑((ArithmeticFunction.sigma 1) n) / 2 ^ n) x → Irrational x) ↔ True

number theoryirrationalityA0667662 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science