Skip to content

Problems · Vela Mathematics Program

Narrowed toproved (Lean) ×source:erdos-ai-contributions-wiki ×Clear all

Problem ledger

111 problems · 3/3NumberSourcesGraph view
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 ∑1/(alog⁡a)\sum 1/(a \log a) taken over primitive sets of integers (sets where no element divides another).
number theoryprimitive setspossible6 sources

Search problems.science

Find a Problem, Result, source, or page