Vela Mathematics Program: problems

Narrowed toopen ×source:erdos-problems ×Clear all

Problem ledger

604 problems · 10/13Number SourcesGraph view

declared openerdos:929

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

Erdős problem 934

graph theorypossible

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

True ↔ ∀ k ≥ 4, ∀ r ≥ 1, ∃ V G, Erdos944.SimpleGraph.IsErdos944 G k r

graph theorychromatic numberN/A2 sources

declared open · formalizederdos:945

True ↔ Erdos945.Erdos945Prop

number theorydivisorspossible · A0488922 sources

declared open · formalizederdos:949

True ↔ ∀ (S : Set ℝ), (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, Cardinal.mk ↑A = Cardinal.continuum ∧ A + A ⊆ Sᶜ

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

What is the largest possible measure of a subset of a radius-

R

disk in

\mathbb{R}^2

containing no pair of points at a positive integer distance? A Poisson-Bessel kernel argument gives

M(R) \ll R^{1/2}

; with Sárközy's lower construction,

M(R) = R^{1/2 + o(1)}

geometrydistancesN/A3 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 openerdos:956

Erdős problem 956

geometrydistancesconvexpossible2 sources

declared open · formalizederdos:959

How large can the difference between the largest and second-largest distance multiplicities be among

n

planar points?

geometrydistancesN/A4 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 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:973

True ↔ ∃ C > 1, ∀ n ≥ 2, ∃ z, z 1 = 1 ∧ (∀ i ∈ Finset.Icc 1 n, 1 ≤ ‖z i‖) ∧ ∀ k ∈ Finset.Icc 2 (n + 1), ‖∑ i ∈ Finset.Icc 1 n, z i ^ k‖ < C ^ (-↑n)

analysisN/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 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 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 openerdos:995

Erdős problem 995

analysisdiscrepancyN/A2 sources

declared open · formalizederdos:996

Let

n_1<n_2<\cdots

be a lacunary sequence of integers and

f\in L^2([0,1])

with

n

th Fourier partial sum

f_n

. Is there an absolute constant

C>0

such that if

\| f-f_n\|_2 \ll (\log\log\log n)^{-C}

then

\frac{1}{N}\sum_{k\leq N}f(\{\alpha n_k\})\to\int_0^1 f

for almost every

\alpha

? A preprint answers this negatively via a dyadic spike-block counterexample.

analysisN/A4 sources

declared open · formalizederdos:1002

sorry ↔ ∃ g, Monotone g ∧ Filter.Tendsto g Filter.atBot (nhds 0) ∧ Filter.Tendsto g Filter.atTop (nhds 1) ∧ ∀ (c : ℝ), Filter.Tendsto (fun n => (MeasureTheory.volume {α | α ∈ Set.Ioo 0 1 ∧ (fun α n => 1 / Real.log ↑n * ∑ k ∈ Finset.Icc 1 n, (1 / 2 - Int.fract (α * ↑k))) α n ≤ c}).toReal) Filter.atTop (nhds (g c))

analysisdiophantine approximationN/A2 sources

declared open · formalizederdos:1003

True ↔ {n | n.totient = (n + 1).totient}.Infinite

number theoryA0012742 sources

declared open · formalizederdos:1004

True ↔ ∀ c > 0, ∀ᶠ (x : ℕ) in Filter.atTop, ∃ n ≤ x, Erdos1004.IsDistinctTotientRun n ⌊Real.log ↑x ^ c⌋₊

number theorypossible3 sources

declared openerdos:1005

Erdős problem 1005

number theoryA386893

declared openerdos:1011

Erdős problem 1011

graph theorypossible

declared openerdos:1013

Erdős problem 1013

graph theoryA292528

declared openerdos:1016

Erdős problem 1016

graph theorycyclesA105206

declared openerdos:1017

Erdős problem 1017

graph theorypossible

declared open · $100erdos:1029

Erdős problem 1029

graph theoryramsey theoryA059442

Problems · Vela Mathematics Program

Problem ledger

Search problems.science