Vela Mathematics Program: problems

Narrowed tosource:plby-lean-proofs ×Clear all

Problem ledger

196 problems · 4/4Number SourcesGraph view

declared proved (Lean) · formalizederdos:923

True ↔ ∀ (V : Type u_1) (n : ℕ), ∃ k, ∀ (G : SimpleGraph V), ↑k ≤ G.chromaticNumber → ∃ H ≤ G, ↑n ≤ H.chromaticNumber ∧ H.CliqueFree 3

graph theorychromatic numberN/A5 sources

declared proved (Lean)erdos:947

Erdős problem 947

number theorycovering systemsN/A4 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)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 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 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 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 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 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:1056

True ↔ ∀ k ≥ 2, ∃ p, ∃ (_ : Nat.Prime p), ∃ boundaries, ∃ (_ : StrictMono boundaries), Erdos1056.AllModProdEqualsOne p boundaries

number theoryA0604273 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 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 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 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 openerdos:1100

Erdős problem 1100

number theorydivisorsA325864 · possible2 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 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

declared disproved (Lean) · formalizederdos:1141

False ↔ Infinite ↑{n | Erdos1141.Erdos1141Prop n}

number theoryprimesA2145836 sources

declared proved (Lean) · formalizederdos:1148

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1148.Erdos1148Prop n

number theoryA390380 · A3931686 sources

declared solvederdos:1187

Erdős problem 1187

number theoryprimesadditive combinatoricsN/A3 sources

declared solved (Lean) · formalizederdos:1190

∀ (ε : ℝ), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, scaleL m ^ (-1 - ε) < Erdos1190.eps m ∧ Erdos1190.eps m < scaleL m ^ (-1 + ε)

number theorycovering systemspossible6 sources

declared solved (Lean) · formalizederdos:1193

False ↔ ∀ (A : Set ℕ) (g : ℕ → ℕ), Monotone g → (∀ (n : ℕ), 0 < g n) → {n | AdditiveCombinatorics.sumRep A n = g n}.lowerDensity = 0

additive combinatoricsN/A5 sources

declared proved (Lean) · formalizederdos:1196

Bounds the weighted sum

\sum 1/(a \log a)

taken over primitive sets of integers (sets where no element divides another).

number theoryprimitive setspossible6 sources

declared disproved (Lean)erdos:1197

Erdős problem 1197

analysisN/A5 sources

Problems · Vela Mathematics Program

Problem ledger