Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×convex ×Clear all

Problem ledger

6 problemsGraph view
declared proved (Lean) · formalizederdos:93
∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.ConvexIndep ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A
geometryconvexdistancesN/A5 sources
declared proved (Lean) · formalized · £25erdos:94
∃ C > 0, ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.ConvexIndep ↑P → ∑ u ∈ EuclideanGeometry.distanceSet P, ↑(EuclideanGeometry.distanceMultiplicity P u) ^ 2 ≤ C * ↑P.card ^ 3
geometryconvexdistancesA3878585 sources
declared open · formalizederdos:96
∀ (n : ℕ), BddAbove (Erdos96.convexUnitDistanceCounts n)
geometrydistancesconvexpossible2 sources
declared falsifiable · formalized · $100erdos:97
True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.ConvexIndep ↑A → ¬Erdos97.HasNEquidistantProperty 4 A
geometrydistancesconvexN/A2 sources
declared falsifiable · formalized · $500erdos:107
sorry ↔ ∀ n ≥ 3, Erdos107.f n = 2 ^ (n - 2) + 1
geometryconvexA0000512 sources
declared falsifiable · formalizederdos:982
∀ (n : ℕ), 3 ≤ n → ∀ (p : Fin n → EuclideanSpace ℝ (Fin 2)), Function.Injective p → EuclideanGeometry.IsConvexPolygon p → ∃ i, {d | ∃ j, j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2
geometryconvexdistancesA0045262 sources
Vela Mathematics Program: problems · problems.science