Skip to content

Problems · Vela Mathematics Program

Narrowed toproved ×set theory ×Clear all

Problem ledger

4 problemsGraph view
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 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 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

Search problems.science

Find a Problem, Result, source, or page