Vela Mathematics Program: problems

Narrowed toproved (Lean) ×source:jayyhk-erdos-lean ×Clear all

Problem ledger

120 problems · 3/3Number SourcesGraph view

declared proved (Lean)erdos:947

Erdős problem 947

number theorycovering systemsN/A4 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 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 (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 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 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 proved (Lean) · formalizederdos:1051

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

irrationalityN/A6 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 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 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 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 proved (Lean) · formalizederdos:1148

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

number theoryA390380 · A3931686 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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science