Problems · Vela Mathematics Program

declared provederdos:578

Erdős problem 578

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

declared proved · formalized · $250erdos:590

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

declared provederdos:605

Erdős problem 605

geometrydistancespossible

declared proved · $250erdos:607

Erdős problem 607

geometrypossible

declared provederdos:622

Erdős problem 622

graph theorypossible

declared provederdos:630

Erdős problem 630

declared provederdos:631

Erdős problem 631

declared provederdos:636

Erdős problem 636

declared provederdos:637

Erdős problem 637

number theoryadditive combinatoricsN/A

declared provederdos:652

Erdős problem 652

geometrydistancesN/A2 sources

declared provederdos:656

Erdős problem 656

declared provederdos:673

Erdős problem 673

number theorydivisorsN/A

declared provederdos:682

Erdős problem 682

number theoryprimesA386978

declared proved · formalizederdos:697

∀ (m : ℕ) (α : ℝ), ∃ δ, {n | ∃ d, d ≡ 1 [MOD m] ∧ ↑d ∈ Set.Ioo 1 (Real.exp (↑m ^ α)) ∧ d ∣ n}.HasDensity δ

number theorydivisorsN/A2 sources

declared provederdos:702

Erdős problem 702

combinatoricsN/A

declared proved · $250erdos:703

Erdős problem 703

combinatoricsA390645

declared provederdos:715

Erdős problem 715

declared provederdos:717

Erdős problem 717

declared provederdos:718

Erdős problem 718

declared proved · $100erdos:720

Erdős problem 720

graph theoryramsey theorypossible

declared provederdos:722

Erdős problem 722

combinatoricsN/A

declared provederdos:732

Erdős problem 732

combinatoricsN/A

declared provederdos:733

Erdős problem 733

combinatoricsgeometrypossible

declared provederdos:737

Erdős problem 737

declared provederdos:745

Erdős problem 745

declared provederdos:746

Erdős problem 746

True ↔ ∃ o, (o =o[Filter.atTop] fun x => 1) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos755.TUnit 6 n) ≤ (1 / 27 + o n) * ↑n ^ 3

declared provederdos:748

Erdős problem 748

number theoryA007865

declared provederdos:752

Erdős problem 752

graph theorycyclesN/A

declared provederdos:754

Erdős problem 754

geometrydistancespossible

declared proved · formalizederdos:755

geometrypossible2 sources

declared provederdos:767

Erdős problem 767

graph theoryturan numberpossible

declared provederdos:771

Erdős problem 771

number theorypossible

declared provederdos:772

Erdős problem 772

number theorysidon setsadditive combinatoricspossible

declared provederdos:780

Erdős problem 780

combinatoricshypergraphschromatic numberN/A

declared provederdos:795

Erdős problem 795

number theorypossible

declared provederdos:797

Erdős problem 797

graph theorychromatic numberpossible

declared provederdos:799

Erdős problem 799

declared provederdos:800

Erdős problem 800

declared provederdos:801

Erdős problem 801

declared provederdos:806

Erdős problem 806

additive combinatoricspossible

declared provederdos:814

Erdős problem 814

graph theorypossible

declared provederdos:816

Erdős problem 816