Vela Mathematics Program: problems

Narrowed tonumber theory ×Clear all

Problem ledger

576 problems · 10/12Number SourcesGraph view

declared provederdos:894

Erdős problem 894

number theoryramsey theoryN/A

declared solvederdos:896

Erdős problem 896

number theorypossible3 sources

declared disproved (Lean) · formalizederdos:897

False ↔ ∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun x => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) | Nat.Prime p}) = ⊤ → Filter.limsup (fun n => (↑(f (n + 1)) - ↑(f n)) / ↑(Real.log ↑n)) Filter.atTop = ⊤

number theoryN/A6 sources

declared open · formalizederdos:912

∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => c * (↑n / Real.log ↑n) ^ (1 / 2)

number theoryfactorialsA0716262 sources

declared open · formalizederdos:913

True ↔ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite

number theoryA3597472 sources

declared openerdos:928

Erdős problem 928

number theoryA006530

declared openerdos:929

Erdős problem 929

number theorypossible

declared open · formalizederdos:930

True ↔ ∀ r > 0, ∃ k, ∀ (I₁ I₂ : Fin r → ℕ), (∀ (i : Fin r), 0 < I₁ i ∧ I₁ i + k ≤ I₂ i + 1) → (∀ (i j : Fin r), i < j → I₂ i < I₁ j) → ¬Erdos930.IsPower (∏ i, ∏ m ∈ Finset.Icc (I₁ i) (I₂ i), m)

number theoryN/A2 sources

declared open · formalizederdos:931

sorry ↔ ∀ (k₁ k₂ : ℕ), k₂ ≥ 3 → k₂ ≤ k₁ → {(n₁, n₂) | n₁ + k₁ ≤ n₂ ∧ (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors = (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Finite

number theoryN/A3 sources

declared open · formalizederdos:932

{r | 2 ≤ {m ∈ Finset.Ioo (Nat.nth Nat.Prime r) (Nat.nth Nat.Prime r.succ) | m.maxPrimeFac < Nat.nth Nat.Prime r.succ - Nat.nth Nat.Prime r}.card}.Infinite

number theoryA3878642 sources

declared open · formalizederdos:933

True ↔ Filter.limsup (fun n => ↑↑(2 ^ Erdos933.k n * 3 ^ Erdos933.l n) / (↑↑n * ↑(Real.log ↑n))) Filter.atTop = ⊤

number theorypossible2 sources

declared openerdos:935

Erdős problem 935

number theoryA057521 · A389244 · possible2 sources

declared open · formalizederdos:936

True ↔ Erdos936.EventuallyNotPowerful fun x => x.factorial + 1

number theoryA146968 · possible2 sources

declared proved · formalizederdos:937

True ↔ {p | Erdos937.IsCoprimePowerfulAP4 p.1 p.2}.Infinite

number theorypossible2 sources

declared open · formalizederdos:938

True ↔ {P | (↑P).IsAPOfLength 3 ∧ ∃ k, P = {Nat.nth Nat.Powerful k, Nat.nth Nat.Powerful (k + 1), Nat.nth Nat.Powerful (k + 2)}}.Finite

number theoryA001694 · A076446 · possible2 sources

declared open · formalizederdos:939

True ↔ ∀ r ≥ 4, (Erdos939.Erdos939Sums r).Nonempty

number theorypossible2 sources

declared open · formalizederdos:940

True ↔ ∀ r ≥ 3, {n | ∃ S, S.card ≤ r ∧ (∀ s ∈ S, r.Full s) ∧ n = S.sum}.HasDensity 0

number theorypossible2 sources

declared provederdos:941

Erdős problem 941

number theoryA056828

declared open · formalizederdos:942

Let

h(n)

count powerful integers in

[n^2, (n+1)^2)

. What is the extremal order of

h(n)

number theorypossible4 sources

declared open · formalizederdos:943

True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(AdditiveCombinatorics.sumRep Nat.Powerful n) ≤ ↑n ^ o n

number theorypossible4 sources

declared open · formalizederdos:945

True ↔ Erdos945.Erdos945Prop

number theorydivisorspossible · A0488922 sources

declared proved · formalizederdos:946

{n | (ArithmeticFunction.sigma 0) n = (ArithmeticFunction.sigma 0) (n + 1)}.Infinite

number theorydivisorsA005237 · A2847832 sources

declared proved (Lean)erdos:947

Erdős problem 947

number theorycovering systemsN/A4 sources

declared solvederdos:948

Erdős problem 948

number theoryramsey theoryN/A3 sources

declared open · formalizederdos:950

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

number theoryprimesN/A2 sources

declared open · formalizederdos:951

sorry ↔ ∀ (a : ℕ → ℝ), 1 < a 0 → StrictMono a → Erdos951.Erdos951Prop a → ∀ᶠ (x : ℝ) in Filter.atTop, {i | a i ≤ x}.ncard ≤ ⌊x⌋₊.primeCounting

number theoryN/A3 sources

declared open · formalizederdos:952

∃ x C, Function.Injective x ∧ ∀ (n : ℕ), Prime (x n) ∧ Zsqrtd.norm (x (n + 1) - x n) < C

number theoryN/A2 sources

declared openerdos:954

Erdős problem 954

number theoryA3906422 sources

declared open · formalizederdos:955

True ↔ ∀ (A : Set ℕ), A.HasDensity 0 → {x | Erdos955.s x ∈ A}.HasDensity 0

number theorypossible2 sources

declared open · formalizederdos:961

True ↔ ∃ C, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Erdos961.f k) < Real.log ↑k ^ C

number theoryA2132532 sources

declared open · formalizederdos:962

True ↔ ∃ ε, (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑(Erdos962.k n) ≤ (Real.log ↑n).rpow (1 / 2 + ε n)

number theoryA3279092 sources

declared openerdos:963

Erdős problem 963

number theorypossible2 sources

declared proved (Lean)erdos:964

Erdős problem 964

number theorydivisorsN/A4 sources

declared proved (Lean) · formalizederdos:966

Let

k,r\geq 2

. Does there exist a set

A\subseteq \mathbb{N}

that contains no non-trivial arithmetic progression of length

k+1

, yet in any

r

-colouring of

A

there must exist a monochromatic non-trivial arithmetic progression of length

k

? Answered in the affirmative.

number theoryadditive combinatoricsramsey theoryN/A6 sources

declared disproved (Lean) · formalizederdos:967

False ↔ ∀ (a : ℕ → ℕ), StrictMono a → 1 < a 0 → (Summable fun k => 1 / ↑(a k)) → ∀ (t : ℝ), 1 + ∑' (k : ℕ), Erdos967.summand t (a k) ≠ 0

number theoryanalysisN/A5 sources

declared open · formalizederdos:968

sorry ↔ 0 < {n | Erdos968.u n < Erdos968.u (n + 1)}.lowerDensity

number theoryA3875912 sources

declared openerdos:969

Erdős problem 969

number theoryA0139282 sources

declared openerdos:970

Erdős problem 970

number theoryA048669

declared open · formalizederdos:971

True ↔ ∃ c > 0, ∃ C > 0, ∀ᶠ (d : ℕ) in Filter.atTop, C * ↑d.totient ≤ ↑{a ∈ Finset.Iio d | a.Coprime d ∧ ↑(Erdos971.leastCongruentPrime a d) > (1 + c) * ↑d.totient * Real.log ↑d}.card

number theoryA2265212 sources

declared open · formalizederdos:972

True ↔ ∀ α > 1, Irrational α → (Erdos972.primeSet α).Infinite

number theoryN/A2 sources

declared open · formalizederdos:975

True ↔ ∀ (f : Polynomial ℤ), f.natDegree ≠ 0 → Irreducible f → (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) → ∃ c > 0, Filter.Tendsto (fun x => Erdos975.Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)

number theorydivisorsA147807 · possible2 sources

declared openerdos:976

Erdős problem 976

number theoryN/A2 sources

declared provederdos:977

Erdős problem 977

number theoryA005420 · A002583

declared open · formalizederdos:978

∀ {f : Polynomial ℤ}, Irreducible f → 2 < f.natDegree → (∀ (x : ℕ), f.natDegree ≠ 2 ^ x) → 0 < f.leadingCoeff → (∀ (p : ℕ), Nat.Prime p → ∃ n, ¬↑p ^ (f.natDegree - 1) ∣ Polynomial.eval (↑n) f) → {n | Powerfree (f.natDegree - 1) (Polynomial.eval (↑n) f)}.HasPosDensity

number theorypossible2 sources

declared open · formalizederdos:979

True ↔ ∀ k ≥ 2, Filter.limsup (fun n => (Erdos979.solutionSet n k).encard) Filter.atTop = ⊤

number theoryA385316 · possible2 sources

declared provederdos:980

Erdős problem 980

number theoryA053760 · A098990 · possible

declared provederdos:981

Erdős problem 981

number theoryN/A

declared openerdos:983

Erdős problem 983

number theorypossible2 sources

declared open · formalizederdos:985

sorry ↔ ∀ (p : ℕ), Nat.Prime p → p ≠ 2 → ∃ q, Nat.Prime q ∧ q < p ∧ orderOf ↑q = p - 1

number theoryA002233 · A219429 · A103309 · possible2 sources

declared provederdos:999

Erdős problem 999

number theorydiophantine approximationN/A

Problems · Vela Mathematics Program

Problem ledger

Search problems.science