Vela Mathematics Program: problems

Narrowed toopen ×geometry ×Clear all

Problem ledger

55 problems · 1/2Number 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 open · formalizederdos:91

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

geometrydistancesA186704 · possible3 sources

declared open · formalizederdos:96

∀ (n : ℕ), BddAbove (Erdos96.convexUnitDistanceCounts n)

geometrydistancesconvexpossible2 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 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 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 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 openerdos:217

Erdős problem 217

geometrydistancespossible

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

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

geometrydistancesA1757693 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 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

declared openerdos:589

Erdős problem 589

geometrypossible

declared open · $500erdos:604

Erdős problem 604

geometrydistancespossible

declared open · $25erdos:634

Erdős problem 634

geometrypossible

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 openerdos:654

n

planar points have no four concyclic, must some point determine

(1 - o(1))n

distinct distances? Failing that, can one always force more than

(1/3 + c)n

geometrydistancespossible3 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 openerdos:657

Erdős problem 657

geometrydistancespossible

declared openerdos:660

Erdős problem 660

geometrydistancesconvexpossible

declared open · $50erdos:661

Erdős problem 661

geometrydistancespossible

declared openerdos:662

Among sufficiently large one-separated planar point sets, does the triangular lattice maximize the number of distances below each threshold? Explicit rational oblique lattices beat the triangular lattice under several closed- and strict-shell readings.

geometrydistancesN/A3 sources

declared openerdos:668

Erdős problem 668

geometrydistancesA385657

declared openerdos:669

Erdős problem 669

geometryA003035 · A006065 · A008997 · possible

declared openerdos:670

Erdős asked whether every

n

-point set in Euclidean space whose pairwise distances are mutually at least 1 apart must have diameter at least

(1+o(1))n^2

. Disproved: an explicit high-dimensional construction beats the conjectured constant.

geometrydistancesN/A2 sources

declared openerdos:704

Erdős problem 704

graph theorygeometrychromatic numberN/A

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 openerdos:827

Erdős problem 827

geometrypossible

declared openerdos:831

Erdős problem 831

geometrypossible

declared openerdos:838

Erdős problem 838

geometryconvexpossible

declared openerdos:953

What is the largest possible measure of a subset of a radius-

R

disk in

\mathbb{R}^2

containing no pair of points at a positive integer distance? A Poisson-Bessel kernel argument gives

M(R) \ll R^{1/2}

; with Sárközy's lower construction,

M(R) = R^{1/2 + o(1)}

geometrydistancesN/A3 sources

declared openerdos:956

Erdős problem 956

geometrydistancesconvexpossible2 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 openerdos:1070

Erdős problem 1070

geometrypossible2 sources

declared openerdos:1083

Erdős problem 1083

geometrydistancesA186704 · possible

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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science