Skip to content

Problems · Vela Mathematics Program

Narrowed togeometry ×Clear all

Problem ledger

110 problems · 3/3NumberSourcesGraph view
declared openerdos:1088
Erdős problem 1088
geometrypossible
declared solvederdos:1089
Erdős problem 1089
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 solvederdos:1091
Erdős problem 1091
geometrychromatic numberN/A3 sources
declared disproved · formalizederdos:1092
False ↔ (fun n => ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f 2 n)
geometrychromatic numberN/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 provederdos:1124
Erdős problem 1124
geometryN/A
declared independenterdos:1127
Erdős problem 1127
geometrydistancesset theoryN/A
declared openerdos:1207
Erdős problem 1207
geometrydistancespossible
declared openerdos:1208
Erdős problem 1208
geometrydistancesA193838 · A271490 · possible2 sources