Vela Mathematics Program: problems

Narrowed tocombinatorics ×Clear all

Problem ledger

47 problemsGraph view

declared open · formalized · $1000erdos:20

sorry ↔ ∃ c, ∀ (n k : ℕ), n > 0 → Erdos20.f n k < c k ^ n

combinatoricsA3320772 sources

declared proved · $500erdos:21

Erdős problem 21

combinatoricsintersecting familyA3915992 sources

declared proved · $500erdos:83

Erdős problem 83

combinatoricsA071799 · A387635

declared open · formalized · $100erdos:120

True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A

combinatoricsN/A3 sources

declared open · $500erdos:161

Erdős problem 161

combinatoricsramsey theorydiscrepancyN/A2 sources

declared openerdos:162

Erdős problem 162

combinatoricsramsey theorydiscrepancyN/A

declared provederdos:171

Erdős problem 171

additive combinatoricscombinatoricsA156989

declared provederdos:191

Erdős problem 191

combinatoricsramsey theoryN/A

declared solved (Lean)erdos:192

Erdős problem 192

arithmetic progressionscombinatoricsN/A3 sources

declared provederdos:207

Erdős problem 207

combinatoricshypergraphsN/A

declared disproved (Lean)erdos:231

Erdős problem 231

combinatoricsN/A3 sources

declared proved (Lean) · formalizederdos:447

True ↔ (fun n => ↑(Erdos447.maxUnionFree n)) =o[Filter.atTop] fun n => 2 ^ n

combinatoricspossible5 sources

declared solved (Lean) · formalizederdos:497

∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ (n : ℕ), ↑(DedekindNumber.M' n) = 2 ^ ((1 + o n) * ↑(n.choose (n / 2)))

combinatoricsA0003725 sources

declared proved (Lean) · formalizederdos:498

True ↔ ∀ (n : ℕ) (z : Fin n → ℂ), (∀ (i : Fin n), 1 ≤ ‖z i‖) → ∀ (c : ℂ), {ε | (∀ (i : Fin n), ε i = -1 ∨ ε i = 1) ∧ ∑ i, ↑(ε i) * z i ∈ Metric.ball c 1}.ncard ≤ n.choose (n / 2)

combinatoricsanalysisN/A5 sources

declared proved (Lean) · formalizederdos:499

True ↔ ∀ (n : ℕ), ∀ M ∈ doublyStochastic ℝ (Fin n), ∃ σ, ↑n ^ (-↑n) ≤ ∏ i, M i (σ i)

combinatoricsN/A5 sources

declared open · formalizederdos:501

For every

x \in \mathbb{R}

let

A_x \subset \mathbb{R}

be a bounded set of Lebesgue outer measure

< 1

. Must there be an infinite independent set, that is an infinite

X \subseteq \mathbb{R}

with

x \notin A_y

for all distinct

x, y \in X

? Erdős and Hajnal proved that arbitrarily large finite independent sets exist. Hechler showed in 1972 that the answer is no under the continuum hypothesis, so any positive answer had to come from a model where CH fails, and Sungchul Lee later derived one from a real-valued measurable cardinal. The answer is that neither side is provable. Dropping Lee's large cardinal by transferring his argument to the extension of a model of CH by random reals gives a model where the answer is yes; Hechler's construction gives one where it is no. The question is independent of ZFC.

combinatoricsset theoryN/A4 sources

declared open · formalizederdos:602

¬Erdos602.disjoint_without_infinite_claim

combinatoricsset theoryN/A3 sources

declared solvederdos:603

Erdős problem 603

combinatoricsset theoryN/A3 sources

declared open · formalizederdos:624

Filter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTop

combinatoricspossible2 sources

declared openerdos:644

Erdős problem 644

combinatoricspossible

declared disprovederdos:664

Erdős problem 664

combinatoricsN/A

declared openerdos:665

Erdős problem 665

combinatoricsN/A2 sources

declared open · formalizederdos:701

True ↔ ∀ {X : Type} [Nonempty X] [Fintype X] (F : Set (Set X)), IsLowerSet F → ∃ x, ∀ F' ⊆ F, F'.Intersecting → Cardinal.mk ↑F' ≤ Cardinal.mk ↑{A | A ∈ F ∧ x ∈ A}

combinatoricsintersecting familyN/A2 sources

declared provederdos:702

Erdős problem 702

combinatoricsN/A

declared proved · $250erdos:703

Erdős problem 703

combinatoricsA390645

declared provederdos:722

Erdős problem 722

combinatoricsN/A

declared falsifiable · formalizederdos:723

True ↔ ∀ {P L : Type} (x : Membership P L) (x_1 : Fintype P) (x_2 : Fintype L) (pp : Configuration.ProjectivePlane P L), IsPrimePow (Configuration.ProjectivePlane.order P L)

combinatoricsN/A2 sources

declared openerdos:724

Erdős problem 724

combinatoricsA001438

declared openerdos:725

Erdős problem 725

combinatoricsA001009

declared provederdos:732

Erdős problem 732

combinatoricsN/A

declared provederdos:733

Erdős problem 733

combinatoricsgeometrypossible

declared openerdos:734

Erdős problem 734

combinatoricspossible2 sources

declared solvederdos:747

Erdős problem 747

combinatoricshypergraphsN/A

declared openerdos:776

Erdős problem 776

combinatoricspossible2 sources

declared solvederdos:777

Erdős problem 777

graph theorycombinatoricsN/A

declared provederdos:780

Erdős problem 780

combinatoricshypergraphschromatic numberN/A

declared open · formalizederdos:857

have f := sorry; ∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun n => ↑(Erdos857.m n k) / f k n) Filter.atTop (nhds 1)

combinatoricspossible2 sources

declared openerdos:901

Erdős problem 901

combinatoricshypergraphspossible

declared provederdos:903

Erdős problem 903

combinatoricsN/A

declared proved (Lean) · formalizederdos:1022

False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)

combinatoricshypergraphspossible6 sources

declared solved (Lean) · formalizederdos:1023

True ↔ ∃ c, 0 < c ∧ Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos1023.F n)) fun n => c * 2 ^ n / ↑n ^ (1 / 2)

combinatoricsA347025 · possible5 sources

declared solvederdos:1025

Erdős problem 1025

combinatoricspossible

declared solved (Lean) · formalizederdos:1026

For a sequence of

n

distinct reals, determine the largest constant

c

such that some monotonic subsequence always has sum exceeding

(c-o(1))\cdot(1/\sqrt{n})

times the total sum. Resolved as

c = 1

combinatoricsA391431 · A3914906 sources

declared provederdos:1027

Erdős problem 1027

combinatoricsN/A

declared openerdos:1159

Erdős problem 1159

combinatoricsN/A

declared openerdos:1173

Erdős problem 1173

set theorycombinatoricsN/A

declared openerdos:1183

Erdős problem 1183

combinatoricsramsey theorypossible2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science