Vela Mathematics Program: problems

Problem ledger

110 problems · 1/3Number SourcesGraph view

declared open · formalized · $500erdos:89

(fun n => ↑n / √(Real.log ↑n)) =O[Filter.atTop] fun n => ↑(EuclideanGeometry.minimalDistinctDistances n)

geometrydistancesA186704 · A1316282 sources

declared disproved (Lean) · formalized · $500erdos:90

Conjectured upper bound on how many pairs among

n

points in the plane can be exactly one unit apart.

geometrydistancesA1867055 sources

declared open · formalizederdos:91

(∀ᶠ (n : ℕ) in Filter.atTop, ¬Erdos91.UniqueMinimizer n) ↔ True

geometrydistancesA186704 · possible3 sources

declared disproved · formalized · $500erdos:92

sorry ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos92.f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))

geometrydistancespossible2 sources

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 · $500erdos:95

Erdős problem 95

geometryconvexdistancespossible

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 open · formalizederdos:98

True ↔ Filter.Tendsto (fun n => ↑(Erdos98.h n) / ↑n) Filter.atTop Filter.atTop

geometrydistancespossible2 sources

declared open · formalized · $100erdos:99

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos99.HasMinDist1 A → IsMinOn (fun B => Metric.diam ↑B) {B | B.card = n ∧ Erdos99.HasMinDist1 B} A → ∃ p ∈ A, ∃ q ∈ A, ∃ r ∈ A, Erdos99.FormsEquilateralTriangle p q r

geometrydistancesN/A2 sources

declared open · formalizederdos:100

True ↔ ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A > C * ↑n

geometrydistancesN/A2 sources

declared open · formalized · $100erdos:101

(fun n => ↑(Erdos101.numLinesWithFourPointMax n)) =o[Filter.atTop] fun n => ↑n ^ 2

geometryA006065 · possible2 sources

declared openerdos:102

Erdős problem 102

geometryN/A

declared openerdos:103

Erdős problem 103

geometrydistancespossible

declared open · $100erdos:104

Erdős problem 104

geometryA003829

declared disproved (Lean) · formalized · $50erdos:105

False ↔ ∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))), Disjoint A B → A.card = B.card + 3 → ¬Collinear ℝ ↑A → ∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ affineSpan ℝ {p, q}

geometryN/A5 sources

declared falsifiableerdos:106

f(n)

is the maximum total side length of

n

interior-disjoint squares packed in the unit square, is

f(k^2 + 1) = k

? An exact rational configuration packs

17

squares with total side length greater than

4

, refuting the identity at

k = 4

geometryN/A3 sources

declared falsifiable · formalized · $500erdos:107

sorry ↔ ∀ n ≥ 3, Erdos107.f n = 2 ^ (n - 2) + 1

geometryconvexA0000512 sources

declared disproved · $250erdos:135

Erdős problem 135

distancesgeometrypossible

declared openerdos:173

Erdős problem 173

geometryramsey theoryN/A

declared openerdos:174

Erdős problem 174

geometryramsey theoryN/A

declared open · formalizederdos:188

IsLeast Erdos188.s sorry

geometryramsey theoryN/A2 sources

declared disproved (Lean) · formalizederdos:189

False ↔ Erdos189.Erdos189For (fun a b c d => (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧ (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧ (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction) fun a b c d => dist a b * dist b c

geometryramsey theoryN/A5 sources

declared open · formalizederdos:193

True ↔ ∀ (S : Set (Fin 3 → ℤ)), S.Finite → ∀ (a : ℕ → Fin 3 → ℤ), Erdos193.IsSWalk S a → (Set.range a).Infinite → Erdos193.HasCollinearTriple ℚ (Set.range fun n => Int.cast ∘ a n)

geometryA2312552 sources

declared disproved (Lean) · formalizederdos:209

False ↔ ∀ (d : ℕ), 4 ≤ d → ∀ (A : Finset (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)))), A.card = d → (∀ L ∈ A, Erdos209.IsLine L) → ((↑A).Pairwise fun L₁ L₂ => ¬L₁.Parallel L₂) → (∀ (p : EuclideanSpace ℝ (Fin 2)), Erdos209.pointMultiplicity A p ≤ 3) → Erdos209.HasGallaiTriangle A

geometryN/A4 sources

declared provederdos:210

Erdős problem 210

geometryA003034

declared proved · $100erdos:211

Erdős problem 211

geometryN/A

declared open · formalizederdos:212

True ↔ ∃ u, Dense u ∧ u.Pairwise fun c₁ c₂ => dist c₁ c₂ ∈ Set.range Rat.cast

geometrydistancesN/A2 sources

declared open · formalizederdos:213

True ↔ ∀ n ≥ 4, Erdos213.Erdos213For n

geometrydistancesN/A2 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 provederdos:215

Erdős problem 215

geometryN/A

declared disprovederdos:216

Erdős problem 216

geometryconvexA381776

declared openerdos:217

Erdős problem 217

geometrydistancespossible

declared solvederdos:223

Erdős problem 223

geometrydistancespossible

declared proved (Lean) · formalizederdos:224

∀ {d : ℕ} (A : Finset (EuclideanSpace ℝ (Fin d))), A.card = 2 ^ d + 1 → ∃ x y z, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ Erdos224.ObtuseAt x y z

geometryN/A5 sources

declared provederdos:232

Erdős problem 232

geometrydistancesN/A

declared open · formalizederdos:352

True ↔ ∃ c > 0, ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet A → ↑(MeasureTheory.volume A) ≥ ↑c → ∃ t, (∀ (p : Fin 3), t.points p ∈ A) ∧ EuclideanGeometry.triangle_area (t.points 0) (t.points 1) (t.points 2) = 1

geometryN/A3 sources

declared proved (Lean) · formalizederdos:353

True ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet A → MeasureTheory.volume A = ⊤ → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, ∃ d ∈ A, EuclideanGeometry.IsIsoscelesTrapezoid a b c d ∧ MeasureTheory.volume ((convexHull ℝ) {a, b, c, d}) = 1

geometryN/A4 sources

declared solved (Lean) · formalizederdos:502

∀ (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))), A.Finite → {d | ∃ x ∈ A, ∃ y ∈ A, x ≠ y ∧ dist x y = d}.ncard = 2 → A.ncard ≤ (n + 2).choose 2

geometrydistancesA0276275 sources

declared open · formalizederdos:503

∀ (n : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A.IsIsosceles), A.ncard = x} sorry

geometrydistancesA1757693 sources

declared solvederdos:504

Erdős problem 504

geometryN/A

declared disproved (Lean) · formalizederdos:505

∃ n S, Bornology.IsBounded S ∧ 0 < Metric.diam S ∧ ∀ (F : Fin (n + 1) → Set (EuclideanSpace ℝ (Fin n))), S ⊆ ⋃ i, F i → ∃ i, Metric.diam S ≤ Metric.diam (F i)

geometrypossible5 sources

declared decidableerdos:506

Erdős problem 506

geometrypossible

declared open · formalizederdos:507

Asymptotics.IsEquivalent Filter.atTop Erdos507.α sorry

geometryN/A3 sources

declared open · formalizederdos:508

4 ≤ (SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumber

geometryramsey theoryN/A2 sources

declared solvederdos:526

Erdős problem 526

probabilitygeometryN/A

declared openerdos:528

Erdős problem 528

geometryA387897 · A156816

declared openerdos:529

Erdős problem 529

geometryprobabilityN/A

declared open · $100erdos:588

Erdős problem 588

geometryA006065 · A008997

Problems · Vela Mathematics Program

Problem ledger

Search problems.science