Vela Mathematics Program: problems

Problem ledger

declared open · formalizederdos:70

True ↔ ∀ (β : Ordinal.{0}) (n : ℕ), β.card ≤ Cardinal.aleph0 → 2 ≤ n → Erdos70.OrdinalCardinalRamsey3 Cardinal.continuum.ord β ↑n

graph theoryramsey theoryset theoryN/A2 sources

declared openerdos:111

Erdős problem 111

graph theorychromatic numberset theoryN/A

declared disprovederdos:118

Erdős problem 118

set theoryramsey theoryN/A

declared not provable · $100erdos:474

Erdős problem 474

set theoryramsey theoryN/A

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 proved · formalized · $250erdos:590

OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0) (Ordinal.omega0 ^ Ordinal.omega0) 3

set theoryramsey theoryN/A2 sources

declared proved · formalized · $250erdos:591

True ↔ OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) 3

set theoryramsey theoryN/A3 sources

declared open · formalized · $1000erdos:592

∀ (β : Ordinal.{u}), β.card ≤ Cardinal.aleph0 → OrdinalCardinalRamsey (Ordinal.omega0 ^ β) (Ordinal.omega0 ^ β) 3 ↔ sorry β

set theoryramsey theoryN/A2 sources

declared open · formalized · $500erdos:593

Erdos Problem #593 asks which finite triple systems occur in every uncountably chromatic triple system. The answer is exactly the class generated from private-vertex expansions of finite bipartite graphs by finite disjoint unions and one-point amalgamations. Problem #1177 on exact spectra is settled alongside it.

set theorygraph theoryhypergraphsN/A4 sources

declared proved · formalizederdos:594

True ↔ ∀ (V : Type) (G : SimpleGraph V), IsEmpty (G.Coloring ℕ) → ∃ N, ∀ (k : ℕ), N ≤ k → ∃ v w, w.IsCycle ∧ w.length = 2 * k + 1

graph theoryset theoryN/A2 sources

declared open · formalized · $250erdos:595

True ↔ ∃ V, ∃ (_ : Infinite V), ∃ G, G.CliqueFree 4 ∧ ¬Erdos595.IsCountableUnionOfTriangleFree G

graph theoryset theoryN/A2 sources

declared open · formalizederdos:596

∀ {U₁ U₂ : Type} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂), G₁.IsErdosHajnalExceptional G₂ ↔ (fun {U₁ U₂} => sorry) G₁ G₂

graph theoryramsey theoryset theoryN/A2 sources

declared openerdos:597

Erdős problem 597

graph theoryramsey theoryset theoryN/A

declared open · formalizederdos:598

∀ (m : Type u_1) [Infinite m], True ↔ ∃ c, ∀ (X : Set m), Cardinal.mk ↑X = Erdos598.κ → c '' {s | ↑s ⊆ X} = Set.univ

set theoryramsey theoryN/A3 sources

declared proved · formalizederdos:599

True ↔ ∀ (V : Type) (G : SimpleGraph V) (A B : Set V), Disjoint A B → G.IsIndepSet A → G.IsIndepSet B → ∃ ι a b p S, (∀ (i : ι), a i ∈ A) ∧ (∀ (i : ι), b i ∈ B) ∧ (∀ (i : ι), (p i).IsPath) ∧ (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧ S ⊆ {v | ∃ i, v ∈ (p i).support} ∧ (∀ (i : ι), ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧ ∀ a' ∈ A, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

graph theoryset theoryN/A2 sources

declared open · $500erdos:601

Erdős problem 601

graph theoryset theoryN/A

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:623

Let

X

be a set of cardinality

\aleph_\omega

and

f

a function from the finite subsets of

X

X

such that

f(A)\not\in A

for all

A

. Must there exist an infinite independent

Y\subseteq X

, i.e. with

f(B)\not\in Y

for all finite

B\subset Y

? Claimed resolution: the positive assertion is equivalent to Koepke's free-subset property, hence independent of ZFC, with consistency strength exactly a measurable cardinal.

set theoryN/A4 sources

declared disproved (Lean) · formalizederdos:1067

False ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ H, H.coe.chromaticCardinal = Cardinal.aleph 1 ∧ H.coe.InfinitelyConnected

graph theoryset theoryN/A5 sources

declared open · formalizederdos:1068

True ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ s, s.Countable ∧ (SimpleGraph.induce s G).InfinitelyConnected

graph theoryset theorychromatic numberN/A2 sources

declared independent · formalizederdos:1119

True ↔ ∀ (m : Cardinal.{0}), Cardinal.aleph0 < m → m < Cardinal.continuum → ∀ (F : Set (ℂ → ℂ)), (∀ f ∈ F, Differentiable ℂ f) → (∀ (z₀ : ℂ), Cardinal.mk ↑{y | ∃ f ∈ F, f z₀ = y} ≤ m) → Cardinal.mk ↑F ≤ m

analysisset theoryN/A2 sources

declared independenterdos:1127

Erdős problem 1127

geometrydistancesset theoryN/A

declared disproved · formalized · $50erdos:1128

False ↔ ∀ (A B C : Type), Cardinal.mk A = Cardinal.aleph 1 → Cardinal.mk B = Cardinal.aleph 1 → Cardinal.mk C = Cardinal.aleph 1 → ∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, Cardinal.mk ↑A₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑B₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑C₁ = Cardinal.aleph 0 ∧ Erdos1128.IsMonochromaticBox f A₁ B₁ C₁

set theoryramsey theoryhypergraphsN/A2 sources

declared open · formalizederdos:1167

∀ (μ : Cardinal.{u}) (r : ℕ) (ν : Ordinal.ToType 1 → Cardinal.{u}), Combinatorics.cardinalPartitionRel μ r 1 ν ↔ μ ≥ ν Erdos1167.i0

set theoryprobabilityN/A2 sources

declared openerdos:1168

Erdős problem 1168

set theoryramsey theoryN/A

declared not disprovableerdos:1169

Erdős problem 1169

set theoryramsey theoryN/A

declared openerdos:1170

Erdős problem 1170

set theoryramsey theoryN/A

declared openerdos:1171

Erdős problem 1171

set theoryramsey theoryN/A

declared openerdos:1172

Erdős problem 1172

set theoryramsey theoryN/A

declared openerdos:1173

Erdős problem 1173

set theorycombinatoricsN/A

declared not disprovableerdos:1174

Erdős problem 1174

set theoryramsey theoryN/A

declared open · formalizederdos:1175

True ↔ ∀ (κ : Cardinal.{u_1}), Cardinal.aleph0 < κ → ∃ μ, ∀ (V : Type u_1) (G : SimpleGraph V), G.chromaticCardinal = μ → ∃ H, H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ

set theorychromatic numberN/A2 sources

declared not disprovable · formalizederdos:1176

True ↔ ∀ {V : Type u_1} (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ EColor, ∃ (_ : Cardinal.mk EColor = Cardinal.aleph 1), ∃ c_edge, ∀ (VColor : Type), Cardinal.mk VColor ≤ Cardinal.aleph 0 → ∀ (c_vert : V → VColor), ∃ vc, ∀ (ec : EColor), ∃ u v, ∃ (h : G.Adj u v), c_vert u = vc ∧ c_vert v = vc ∧ c_edge ⟨s(u, v), h⟩ = ec

set theorychromatic numberN/A2 sources

declared openerdos:1177

For a finite forbidden triple system

G

, what exact uncountable chromatic cardinalities occur among

G

-free triple systems, and how do those spectra interact? The revised manuscript answers the three exact-cardinal questions and claims a complete spectrum dichotomy.

set theorychromatic numberhypergraphsN/A3 sources

Problems · Vela Mathematics Program

Problem ledger