Vela Mathematics Program: problems

Narrowed toopen ×primes ×Clear all

Problem ledger

43 problemsGraph view

declared openerdos:5

Erdős problem 5

number theoryprimesA001223

declared open · formalizederdos:9

1 ∈ Erdos9.Erdos9A

number theoryadditive basisprimesA0062862 sources

declared open · formalizederdos:10

True ↔ ∃ k, Erdos10.sumPrimeAndTwoPows k = Set.univ \ {0, 1}

number theoryadditive basisprimesA3870532 sources

declared open · formalizederdos:15

True ↔ Summable fun k => (-1) ^ (k + 1) * (↑k + 1) / ↑(Nat.nth Nat.Prime k)

number theoryprimesN/A2 sources

declared open · formalizederdos:17

sorry ↔ {p | Erdos17.IsClusterPrime p}.Infinite

number theoryprimesA0381332 sources

declared open · formalizederdos:141

sorry ↔ ∀ k ≥ 3, ∃ s, Erdos141.Set.IsAPAndPrimeProgressionOfLength s k

additive combinatoricsprimesarithmetic progressionsA0065602 sources

declared open · formalizederdos:200

sorry ↔ (fun n => ↑(Erdos200.longestPrimeArithmeticProgressions n)) =o[Filter.atTop] fun n => Real.log ↑n

primesarithmetic progressionsA0051152 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 open · formalizederdos:218

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

number theoryprimesA333230 · A333231 · A0641133 sources

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 open · formalizederdos:236

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

number theoryprimesA039669 · A1099252 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 open · formalizederdos:244

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

number theoryprimesN/A2 sources

declared open · formalizederdos:279

True ↔ ∀ k ≥ 3, ∃ a N, (∀ (p : ℕ), Nat.Prime p → a p < p) ∧ ∀ n ≥ N, ∃ p, ∃ t ≥ k, Nat.Prime p ∧ n = a p + t * p

number theorycovering systemsprimesN/A2 sources

declared open · formalizederdos:428

True ↔ ∃ A, (∃ᶠ (n : ℕ) in Filter.atTop, ∀ a ∈ A, 0 < a → a < n → Nat.Prime (n - a)) ∧ Filter.liminf (fun n => Erdos428.primeDensityRatio A n) Filter.atTop > 0

number theoryprimesN/A2 sources

declared openerdos:431

Erdős problem 431

number theoryprimesN/A

declared open · formalizederdos:454

True ↔ Filter.limsup (fun n => ↑(Erdos454.f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤

number theoryprimesA389676 · A3896772 sources

declared openerdos:461

Erdős problem 461

number theoryprimespossible

declared openerdos:462

Erdős problem 462

number theoryprimesA032742 · possible

declared open · formalizederdos:463

True ↔ ∃ f, ∃ (_ : Filter.Tendsto f Filter.atTop Filter.atTop), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m, m.Composite ∧ n + f n < m ∧ m < n + m.minFac

number theoryprimespossible2 sources

declared open · formalizederdos:680

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k, k ≠ 0 ∧ (n + k).minFac > k ^ 2 + 1

number theoryprimesN/A2 sources

declared open · formalizederdos:681

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k > 0, (n + k).Composite ∧ ∀ (p : ℕ), Erdos681.IsLPF p (n + k) → p > k ^ 2

number theoryprimesA3896802 sources

declared open · formalizederdos:683

True ↔ ∃ c > 0, ∀ (n k : ℕ), 0 < k ∧ k < n → ↑(Erdos683.P n k) > min (↑n - ↑k + 1) (↑k ^ (1 + c))

number theoryprimesbinomial coefficientsA006530 · A074399 · A121359 · possible2 sources

declared openerdos:684

For the least

k

at which the small-prime part of

\binom{n}{k}

exceeds

n^2

, how large can

f(n)

be?

number theoryprimesbinomial coefficientsA392019 · possible3 sources

declared openerdos:685

Erdős problem 685

number theoryprimesbinomial coefficientsN/A

declared open · formalizederdos:850

True ↔ ∃ x y, x ≠ y ∧ x.primeFactors = y.primeFactors ∧ (x + 1).primeFactors = (y + 1).primeFactors ∧ (x + 2).primeFactors = (y + 2).primeFactors

number theoryprimesA3431013 sources

declared openerdos:852

Erdős problem 852

number theoryprimesA001223 · A053597 · A0785152 sources

declared open · formalizederdos:853

Filter.Tendsto Erdos853.r Filter.atTop Filter.atTop

number theoryprimesA001223 · A3907692 sources

declared open · formalizederdos:855

True ↔ ∀ᶠ (x : ℕ) (y : ℕ) in Filter.atTop, (x + y).primeCounting ≤ x.primeCounting + y.primeCounting

number theoryprimesA0231932 sources

declared openerdos:860

Erdős problem 860

number theoryprimesA048670 · A058989

declared open · formalizederdos:890

sorry ↔ ∀ k ≥ 1, Filter.liminf (fun n => ∑ i ∈ Finset.range k, ↑(Erdos890.omegaGt k (n + i))) Filter.atTop ≤ ↑k

number theoryprimesN/A2 sources

declared open · formalizederdos:950

True ↔ Filter.liminf (fun n => ↑(Erdos950.f n)) Filter.atTop = 1

number theoryprimesN/A2 sources

declared open · formalizederdos:1055

∀ (r : ℕ+), {p | Nat.Prime p ∧ Erdos1055.IsOfClass r p}.Infinite

number theoryprimesA0051132 sources

declared open · formalizederdos:1059

Erdos1059.AllFactorialSubtractionsComposite 101

number theoryprimesA0641522 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 openerdos:1143

Erdős problem 1143

number theoryprimesN/A2 sources

declared openerdos:1184

Erdős problem 1184

number theoryprimespossible

declared openerdos:1200

Erdős problem 1200

number theoryprimespossible

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