Vela Mathematics Program: problems

Narrowed toformalized ×source:erdos-ai-contributions-wiki ×Clear all

Problem ledger

258 problems · 5/6Number SourcesGraph view

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

declared open · formalizederdos:1004

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

number theorypossible3 sources

declared solved (Lean) · formalizederdos:1007

IsLeast {m | ∃ n G, G.HasDimension 4 ∧ G.edgeSet.ncard = m} sorry

graph theoryN/A5 sources

declared proved (Lean) · formalizederdos:1008

True ↔ ∃ c > 0, ∀ (V : Type) [Fintype V] (G : SimpleGraph V), ∃ H ≤ G, (SimpleGraph.cycleGraph 4).Free H ∧ c * ↑G.edgeSet.ncard ^ (2 / 3) ≤ ↑H.edgeSet.ncard

graph theoryN/A5 sources

declared proved (Lean) · formalizederdos:1014

∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun l => ↑R(k, l + 1) / ↑R(k, l)) Filter.atTop (nhds 1)

graph theorypossible7 sources

declared proved (Lean) · formalizederdos:1022

False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)

combinatoricshypergraphspossible6 sources

declared solved (Lean) · formalizederdos:1023

True ↔ ∃ c, 0 < c ∧ Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos1023.F n)) fun n => c * 2 ^ n / ↑n ^ (1 / 2)

combinatoricsA347025 · possible5 sources

declared solved (Lean) · formalizederdos:1026

For a sequence of

n

distinct reals, determine the largest constant

c

such that some monotonic subsequence always has sum exceeding

(c-o(1))\cdot(1/\sqrt{n})

times the total sum. Resolved as

c = 1

combinatoricsA391431 · A3914906 sources

declared solved (Lean) · formalizederdos:1028

(fun n => ↑(Erdos1028.H n)) =Θ[Filter.atTop] fun n => ↑n ^ (3 / 2)

graph theorydiscrepancypossible5 sources

declared disproved (Lean) · formalizederdos:1034

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), ↑n ^ 2 / 4 < ↑G.edgeSet.ncard → ∃ T, G.IsNClique 3 T ∧ ∃ Y, Erdos1034.JoinedToTwo G T Y ∧ (1 / 2 - ε) * ↑n < ↑Y.card

graph theorypossible5 sources

declared proved (Lean) · formalizederdos:1036

True ↔ ∀ (c : ℝ), 0 < c → ∃ δ, 0 < δ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), ↑G.cliqueNum ≤ c * Real.log ↑n → ↑G.indepNum ≤ c * Real.log ↑n → Erdos1036.HasManyNonIsomorphicInducedSubgraphs G (2 ^ (δ * ↑n))

graph theorypossible5 sources

declared disproved (Lean) · formalizederdos:1037

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ (C : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (∀ (d : ℕ), {v | (G.neighborSet v).ncard = d}.ncard ≤ 2) → (1 / 2 + ε) * ↑n < ↑(Set.range fun v => (G.neighborSet v).ncard).ncard → ∃ s, Erdos1037.IsTrivialSet G s ∧ C * Real.log ↑n < ↑s.ncard

graph theoryN/A5 sources

declared open · formalizederdos:1038

Among all nonconstant monic polynomials

f

whose roots lie in

[-1, 1]

, determine

\inf_f |\{x \in \mathbb{R} : |f(x)| < 1\}|

analysisN/A4 sources

declared falsifiable · formalizederdos:1041

∀ (n : ℕ) (f : Polynomial ℂ), n ≥ 2 → f.natDegree = n → f.Monic → f.rootSet ℂ ⊆ Metric.ball 0 1 → ∃ z₁ z₂, ∃ (_ : {z₁, z₂} ≤ f.roots), ∃ γ, Set.range ⇑γ ⊆ {z | ‖Polynomial.eval z f‖ < 1} ∧ Erdos1041.length (Set.range ⇑γ) < 2

analysisN/A3 sources

declared disproved (Lean) · formalizederdos:1043

False ↔ ∀ (f : Polynomial ℂ), f.Monic → f.degree ≥ 1 → ∃ u, ‖u‖ = 1 ∧ MeasureTheory.volume (⇑(ℝ ∙ u).orthogonalProjection '' Erdos1043.levelSet f) ≤ 2

analysisN/A5 sources

declared solved (Lean) · formalizederdos:1044

IsGLB {L | ∃ f, Erdos1044.IsAdmissible f ∧ Erdos1044.maxBoundaryLength f = L} 2

analysisN/A5 sources

declared disproved (Lean) · formalizederdos:1047

False ↔ ∀ (f : Polynomial ℂ) (m : ℕ) (c : ℝ), f.Monic → (f.rootSet ℂ).ncard = m → 0 < c → (Erdos1047.componentsIn (Erdos1047.sublevelSet f c)).ncard = m → ∀ t ∈ Erdos1047.componentsIn (Erdos1047.sublevelSet f c), Convex ℝ t

analysisN/A5 sources

declared disproved (Lean) · formalizederdos:1048

False ↔ ∀ (r : ℝ) (f : Polynomial ℂ), r < 2 → f.Monic → f.degree ≥ 1 → (∀ z ∈ f.roots, ‖z‖ ≤ r) → ∃ z ∈ Erdos1048.openLevelSet f, ENNReal.ofReal (2 - r) < Metric.ediam (connectedComponentIn (Erdos1048.openLevelSet f) z)

analysisN/A5 sources

declared proved (Lean) · formalizederdos:1051

True ↔ ∀ (a : ℕ → ℤ), StrictMono a → Erdos1051.GrowthCondition a → Irrational (Erdos1051.ErdosSeries a)

irrationalityN/A6 sources

declared open · formalizederdos:1054

sorry ↔ (fun n => ↑(Erdos1054.f n)) =o[Filter.atTop] fun n => ↑n

number theorydivisorsA1674853 sources

declared open · formalizederdos:1061

For

S(x) = \#\{(a,b) : a + b \le x,\ \sigma(a) + \sigma(b) = \sigma(a+b)\}

, is

S(x) \sim cx

? The preprint claims

S(x)

grows faster than

x (\log x)^R

for every fixed

R

, ruling out the linear asymptotic.

number theoryA110177 · possible4 sources

declared open · formalizederdos:1062

(∃ l, Filter.Tendsto (fun n => ↑(Erdos1062.f n) / ↑n) Filter.atTop (nhds l) ∧ Irrational l) ↔ True

number theoryA0383723 sources

declared disproved (Lean) · formalizederdos:1067

False ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ H, H.coe.chromaticCardinal = Cardinal.aleph 1 ∧ H.coe.InfinitelyConnected

graph theoryset theoryN/A5 sources

declared proved (Lean) · formalizederdos:1071

True ↔ ∃ S, Maximal (fun T => (∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧ seg.1.ofLp 0 ∈ Set.Icc 0 1 ∧ seg.1.ofLp 1 ∈ Set.Icc 0 1 ∧ seg.2.ofLp 0 ∈ Set.Icc 0 1 ∧ seg.2.ofLp 1 ∈ Set.Icc 0 1) ∧ (↑T).Pairwise Erdos1071.SegmentsDisjoint) S

geometryN/A5 sources

declared disproved (Lean) · formalizederdos:1080

False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] [Nonempty V] (G : SimpleGraph V) (X Y : Set V), Erdos1080.IsBipartition G X Y → X.ncard = ⌊↑(Fintype.card V) ^ (2 / 3)⌋₊ → ↑G.edgeSet.ncard ≥ c * ↑(Fintype.card V) → ∃ v walk, walk.IsCycle ∧ walk.length = 6

graph theorypossible5 sources

declared falsifiable · formalizederdos:1082

True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.NonTrilinear ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A

geometrydistancespossible3 sources

declared proved (Lean) · formalizederdos:1090

True ↔ ∀ (k : ℕ), 3 ≤ k → ∃ A, ∀ (C : ↥A → Fin 2), ∃ S, ∃ (hSA : S ⊆ A), Collinear ℝ ↑S ∧ S.card ≥ k ∧ (∀ y ∈ A, y ∈ affineSpan ℝ ↑S → y ∈ S) ∧ ∃ c, ∀ (x : Fin 2 → ℝ) (hx : x ∈ S), C ⟨x, ⋯⟩ = c

geometryramsey theoryN/A5 sources

declared disproved · formalizederdos:1092

False ↔ (fun n => ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f 2 n)

geometrychromatic numberN/A5 sources

declared open · formalizederdos:1095

Asymptotics.IsEquivalent Filter.atTop (fun k => Real.log ↑(Erdos1095.g k)) fun k => ↑k / Real.log ↑k

number theorybinomial coefficientsA0034584 sources

declared open · formalizederdos:1097

False ↔ ∃ C > 0, ∀ (A : Finset ℤ), ↑(Erdos1097.CommonDifferencesThreeTermAP A).ncard ≤ C * ↑A.card ^ (3 / 2)

number theoryadditive combinatoricsN/A3 sources

declared proved (Lean) · formalizederdos:1098

True ↔ ∀ (G : Type u_1) [inst : Group G], (∀ (s : Set G), (Erdos1098.nonCommutingGraph G).IsClique s → s.Finite) → ∃ n, ∀ (s : Finset G), (Erdos1098.nonCommutingGraph G).IsClique ↑s → s.card ≤ n

group theoryN/A5 sources

declared open · formalizederdos:1101

Does there exist a good pairwise-coprime sequence

u_n

with

\sum 1/u_n < \infty

and polynomial growth? What if one only requires

u_n \le e^{o(n)}

number theoryN/A4 sources

declared solved (Lean) · formalizederdos:1102

∀ (A : ℕ → ℕ), StrictMono A → Erdos1102.HasPropertyP (Set.range A) → Filter.Tendsto (fun j => ↑(A j) / ↑j) Filter.atTop Filter.atTop

number theoryN/A5 sources

declared proved (Lean) · formalizederdos:1121

∀ {n : ℕ} (c : Fin n → EuclideanSpace ℝ (Fin 2)) (r : Fin n → ℝ), (∀ (i : Fin n), 0 < r i) → (∀ (v : EuclideanSpace ℝ (Fin 2)) (t : ℝ), v ≠ 0 → (∀ (i : Fin n), ∀ p ∈ Metric.closedBall (c i) (r i), inner ℝ v p ≠ t) → (∀ (i : Fin n), inner ℝ v (c i) < t) ∨ ∀ (i : Fin n), t < inner ℝ v (c i)) → ∃ z, ⋃ i, Metric.closedBall (c i) (r i) ⊆ Metric.closedBall z (∑ i, r i)

geometryN/A5 sources

declared proved (Lean) · formalizederdos:1125

True ↔ ∀ (f : ℝ → ℝ), (∀ (x h : ℝ), h > 0 → 2 * f x ≤ f (x + h) + f (x + 2 * h)) → Monotone f

analysisN/A5 sources

declared proved (Lean) · formalizederdos:1126

True ↔ ∀ (f : ℝ → ℝ), (∀ᵐ (p : ℝ × ℝ) ∂MeasureTheory.volume.prod MeasureTheory.volume, f (p.1 + p.2) = f p.1 + f p.2) → ∃ h, (∀ (x y : ℝ), h (x + y) = h x + h y) ∧ ∀ᵐ (x : ℝ), f x = h x

analysisN/A5 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 proved (Lean) · formalizederdos:1136

True ↔ ∃ A, 1 / 3 < A.lowerDensity ∧ Erdos1136.AvoidsPowersOfTwo A

number theoryN/A5 sources

declared disproved (Lean) · formalizederdos:1138

False ↔ ∀ C > 1, Asymptotics.IsEquivalent Erdos1138.snd_gt_half_fst (Erdos1138.primeCount_Ioc_mul_const C) fun x => match x with | (x, y) => C * ↑(Erdos1138.sup_primeGap x) / Real.log y

number theoryprimespossible6 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science