Skip to content

Problems · Vela Mathematics Program

Narrowed toproved (Lean) ×distances ×Clear all

Problem ledger

5 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 proved (Lean) · formalizederdos:214
True ↔ ∀ (S : Set (EuclideanSpace ℝ (Fin 2))), Erdos214.UnitDistanceAvoiding S → ∃ p, (∀ (i : Fin 4), p i ∈ Sᶜ) ∧ Congruent p Erdos214.unitSquare
geometrydistancesN/A5 sources
declared proved (Lean) · formalizederdos:659
True ↔ ∃ A, (∀ (n : ℕ), (A n).card = n ∧ ∀ S ⊆ A n, S.card = 4 → 3 ≤ EuclideanGeometry.distinctDistances S) ∧ (fun n => ↑(EuclideanGeometry.distinctDistances (A n))) =O[Filter.atTop] fun n => ↑n / √(Real.log ↑n)
geometrydistancespossible6 sources
declared proved (Lean) · formalizederdos:756
True ↔ (fun n => ↑n) =O[Filter.atTop] fun n => ↑(Erdos756.maxRichDistances n)
geometrydistancespossible5 sources

Search problems.science

Find a Problem, Result, source, or page