Vela Mathematics Program: problems

Problem ledger

319 problems · 7/7Number SourcesGraph view

declared open · formalizederdos:1113

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

number theorycovering systemsA0763362 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 open · formalized · $500erdos:1135

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

number theoryA006370 · A0089082 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 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 open · formalizederdos:1142

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

number theoryprimesA0396692 sources

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 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

declared open · formalizederdos:1167

∀ (μ : Cardinal.{u}) (r : ℕ) (ν : Ordinal.ToType 1 → Cardinal.{u}), Combinatorics.cardinalPartitionRel μ r 1 ν ↔ μ ≥ ν Erdos1167.i0

set theoryprobabilityN/A2 sources

declared open · formalizederdos:1175

True ↔ ∀ (κ : Cardinal.{u_1}), Cardinal.aleph0 < κ → ∃ μ, ∀ (V : Type u_1) (G : SimpleGraph V), G.chromaticCardinal = μ → ∃ H, H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ

set theorychromatic numberN/A2 sources

declared open · formalizederdos:1188

Estimate the number

F(x)

of minimal distinct covering systems whose moduli all lie in

[1, x]

. The candidate proof gives

\log\log F(x)/\log x \to 1

, i.e.

F(x) = \exp(x^{1+o(1)})

number theorycovering systemspossible4 sources

declared open · formalizederdos:1192

True ↔ ∀ r ≥ 2, ∃ A, (∀ᶠ (n : ℕ) in Filter.atTop, Erdos1192.f_r A r n > 0) ∧ (fun x => ∑ n ∈ Finset.range (x + 1), ↑(Erdos1192.f_r A r n) ^ 2) =O[Filter.atTop] fun x => ↑x

additive combinatoricsadditive basispossible2 sources

declared open · formalizederdos:1199

True ↔ ∀ (color : ℕ → Fin 2), ∃ A, A.Infinite ∧ ∀ n ∈ A + A, ∀ m ∈ A + A, color n = color m

additive combinatoricsramsey theorypossible2 sources

declared open · formalizederdos:1201

Is it true that for every

\epsilon,\eta>0

there exists a

k

such that the density of

n

for which

P(n(n+1)\cdots(n+k))>n^{1-\epsilon}

is at least

1-\eta

, where

P(m)

is the greatest prime divisor of

m

? A short argument via the Matomäki-Radziwiłł theorem establishes the lower-density version.

number theoryprimespossible4 sources

declared open · formalizederdos:1203

True ↔ Filter.Tendsto Erdos1203.F Filter.atTop Filter.atTop

number theorypossible2 sources

declared open · formalizederdos:1209

False ↔ ∃ f, ∀ (a : ℕ → ℕ), StrictMono a → (∀ (k : ℕ), f k ≤ a k) → (∃ n, ∀ (k : ℕ), Nat.Prime (n + a k)) → {n | ∀ (k : ℕ), Nat.Prime (n + a k)}.Infinite

number theorypossible3 sources

declared open · formalizederdos:1210

True ↔ ∃ C, ∀ (n : ℕ) (A : Finset ℕ), (∀ a ∈ A, 1 ≤ a ∧ a < n) → (∀ a ∈ A, ∀ b ∈ A, a ≠ b → a.Coprime b) → ∑ a ∈ A, 1 / (↑n - ↑a) ≤ ∑ p ∈ Finset.range n with Prime p, 1 / ↑p + C

number theorypossible2 sources

declared open · formalizederdos:1212

∀ {a s : ℕ}, a < s → (∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p) → a.gcd s = 1

number theoryprimespossible2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science