Vela Mathematics Program: problems

Problem ledger

1,217 problems · 20/25Number SourcesGraph view

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

Erdős problem 957

geometrydistancesN/A

declared disproved (Lean) · formalizederdos:958

False ↔ ∀ (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → (EuclideanGeometry.distanceSet A).card = n - 1 ∧ Finset.image (EuclideanGeometry.distanceMultiplicity A) (EuclideanGeometry.distanceSet A) = Finset.Icc 1 (n - 1) → Erdos958.IsEquidistantOnLine A ∨ Erdos958.IsEquidistantOnCircle A

distancesgeometryN/A5 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 disprovederdos:960

Erdős problem 960

geometrypossible3 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 disproved · formalizederdos:965

False ↔ ∀ (f : ℝ → Fin 2), ∃ A, ¬A.Countable ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a ≠ b → c ≠ d → f (a + b) = f (c + d)

ramsey theoryN/A2 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: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 proved (Lean) · formalizederdos:974

∀ {n : ℕ} [inst : NeZero n] (z : Fin n → ℂ), z 0 = 1 → {k | ∀ j < n - 1, ∑ i, z i ^ (k + j) = 0}.Infinite → Erdos974.IsTuranConfiguration z

analysisN/A5 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 falsifiable · formalizederdos:982

∀ (n : ℕ), 3 ≤ n → ∀ (p : Fin n → EuclideanSpace ℝ (Fin 2)), Function.Injective p → EuclideanGeometry.IsConvexPolygon p → ∃ i, {d | ∃ j, j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2

geometryconvexdistancesA0045262 sources

declared openerdos:983

Erdős problem 983

number theorypossible2 sources

declared provederdos:984

Erdős problem 984

arithmetic progressionsadditive combinatoricsN/A

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

Erdős problem 986

graph theoryramsey theoryA000791 · A0594423 sources

declared proved · formalizederdos:987

True ↔ ∀ (x : ℕ → ℝ), (∀ (j : ℕ), x j ∈ Set.Ioo 0 1) → Filter.limsup (fun k => Erdos987.A x k) Filter.atTop = ⊤

analysisdiscrepancyN/A4 sources

declared solvederdos:988

Erdős problem 988

discrepancypossible

declared solvederdos:989

Erdős problem 989

discrepancypossible

declared disproved (Lean) · formalizederdos:990

False ↔ ∃ C, ∀ (f : Polynomial ℂ), f.coeff 0 ≠ 0 → ∀ (α β : ℝ), 0 ≤ α → α ≤ β → β ≤ 2 * Real.pi → |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤ C * √(↑f.support.card * Real.log (Erdos990.M f))

analysisN/A6 sources

declared provederdos:991

Erdős problem 991

discrepancyN/A

declared disprovederdos:992

Erdős problem 992

discrepancyN/A

declared falsifiableerdos:993

Erdős problem 993

graph theoryA000055 · possible

declared disprovederdos:994

Erdős problem 994

analysisdiscrepancyN/A

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

True ↔ ∀ (α : ℝ), ¬Erdos997.IsWellDistributed fun n => Int.fract (α * ↑(Nat.nth Nat.Prime n))

analysisdiscrepancyprimesN/A6 sources

declared provederdos:998

Erdős problem 998

analysisdiophantine approximationN/A

declared provederdos:999

Erdős problem 999

number theorydiophantine approximationN/A

declared proved (Lean) · formalizederdos:1000

True ↔ ∃ n, StrictMono n ∧ 0 < n 0 ∧ Filter.Tendsto (Erdos1000.phiAvg n) Filter.atTop (nhds 0)

number theorydiophantine approximationN/A5 sources

Problems · Vela Mathematics Program

Problem ledger