Vela Mathematics Program: problems

Narrowed toformalized ×geometry ×Clear all

Problem ledger

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 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 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 falsifiable · formalized · $500erdos:107

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

geometryconvexA0000512 sources

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 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 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 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 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 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 solved · formalized · $25erdos:633

∀ {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))}, Erdos633.IsCuttable n T → n ≠ 0

geometryN/A2 sources

declared open · formalizederdos:653

True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (1 - o n) * ↑n ≤ ↑(EuclideanGeometry.maximalDistinctDistancesFrom n)

geometrydistancespossible2 sources

declared open · formalizederdos:655

False ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))), X.card = n → Erdos655.IsValid X → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)

geometrydistancespossible3 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 · formalizederdos:755

True ↔ ∃ o, (o =o[Filter.atTop] fun x => 1) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos755.TUnit 6 n) ≤ (1 / 27 + o n) * ↑n ^ 3

geometrypossible2 sources

declared proved (Lean) · formalizederdos:756

True ↔ (fun n => ↑n) =O[Filter.atTop] fun n => ↑(Erdos756.maxRichDistances n)

geometrydistancespossible5 sources

declared open · formalizederdos:757

∀ {A : Set ℝ}, sorry = sSup {c | Erdos757.IsAdmissible c}

geometrydistancessidon setspossible2 sources

declared open · formalizederdos:769

For the least cutoff

c(n)

after which every

k

occurs as the number of homothetic cubes in a decomposition of the unit

n

-cube, is

c(n) \gg n^n

? The Lean proof shows

c(n) = o(n^n)

along odd dimensions.

number theorygeometryA014544 · possible4 sources

declared proved (Lean) · formalizederdos:798

True ↔ (fun n => ↑(Erdos798.t n)) =o[Filter.atTop] fun n => ↑n

geometryA1164465 sources

declared disproved (Lean) · formalizederdos:846

False ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), ∀ ε > 0, A.Infinite → Erdos846.NonTrilinearFor A ε → Erdos846.WeaklyNonTrilinear A

geometryN/A6 sources

declared proved (Lean) · formalizederdos:898

∀ (A B C P L M N : EuclideanSpace ℝ (Fin 2)), AffineIndependent ℝ ![A, B, C] → P ∈ interior ((convexHull ℝ) {A, B, C}) → N ∈ affineSpan ℝ {A, B} → (affineSpan ℝ {P, N}).direction ⟂ (affineSpan ℝ {A, B}).direction → M ∈ affineSpan ℝ {B, C} → (affineSpan ℝ {P, M}).direction ⟂ (affineSpan ℝ {B, C}).direction → L ∈ affineSpan ℝ {C, A} → (affineSpan ℝ {P, L}).direction ⟂ (affineSpan ℝ {C, A}).direction → dist P A + dist P B + dist P C ≥ 2 * (dist P M + dist P N + dist P L)

geometryN/A5 sources

declared disproved (Lean) · formalizederdos:958

False ↔ ∀ (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → (EuclideanGeometry.distanceSet A).card = n - 1 ∧ Finset.image (EuclideanGeometry.distanceMultiplicity A) (EuclideanGeometry.distanceSet A) = Finset.Icc 1 (n - 1) → Erdos958.IsEquidistantOnLine A ∨ Erdos958.IsEquidistantOnCircle A

distancesgeometryN/A5 sources

declared open · formalizederdos:959

How large can the difference between the largest and second-largest distance multiplicities be among

n

planar points?

geometrydistancesN/A4 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

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 falsifiable · formalizederdos:1082

True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.NonTrilinear ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A

geometrydistancespossible3 sources

declared open · formalizederdos:1084

∀ {n : ℕ}, n ≠ 0 → Erdos1084.f 2 n < 3 * n

geometrydistancesA045945 · possible3 sources

declared open · formalizederdos:1085

∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (1 + c / Real.log (Real.log ↑n)) < ↑(Erdos1085.f 2 n)

geometrydistancesA186705 · possible2 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 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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science