Vela Mathematics Program: problems

Narrowed toformalized ×combinatorics ×Clear all

Problem ledger

15 problemsGraph view

declared open · formalized · $1000erdos:20

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

combinatoricsA3320772 sources

declared open · formalized · $100erdos:120

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

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

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

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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science