Problems · Vela Mathematics Program

of graphs, is there a single

declared open (Lean) · formalizederdos:180

For every finite family

\mathcal{F}

G \in \mathcal{F}

with

\mathrm{ex}(n;G) \ll_{\mathcal{F}} \mathrm{ex}(n;\mathcal{F})

? A counterexample refutes the Erdős-Simonovits compactness conjecture.

graph theoryturan numberN/A4 sources

declared openerdos:181

Erdős problem 181

-colouring of the edges of

declared provederdos:182

Erdős problem 182

graph theorypossible

declared open (Lean) · formalized · $250erdos:183

Let

R(3;k)

be the least

n

such that every

k

K_n

contains a monochromatic triangle. Determine

\lim_{k\to\infty} R(3;k)^{1/k}

(a $250 Erdős prize problem). A superexponential lower bound resolves the problem: the limit is infinite.

graph theoryramsey theoryA0033233 sources

declared open · formalizederdos:184

∃ f, (f =O[Filter.atTop] fun n => ↑n) ∧ ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V), ∃ D, (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) ∧ Erdos184.IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

graph theorycyclespossible2 sources

declared disproved (Lean) · formalized · $25erdos:426

False ↔ ∃ c, 0 < c ∧ ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, c * (2 ^ n.choose 2 / ↑n.factorial) ≤ ↑H.uniqueSubgraphCount

graph theorypossible5 sources

declared open · $500erdos:500

Erdős problem 500

graph theoryhypergraphsturan numberA140462

declared provederdos:518

Erdős problem 518

False ↔ ∀ (δ : ℝ), 0 < δ → ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 5 → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ∃ S, c * ↑n ≤ ↑S.card ∧ G.CliqueFreeOn (↑S) 3

declared disproved · formalizederdos:533

graph theoryN/A3 sources

declared openerdos:544

Erdős problem 544

graph theoryramsey theoryA000791

declared openerdos:545

Erdős problem 545

graph theoryramsey theoryA059442 · possible

declared provederdos:546

Erdős problem 546

declared decidableerdos:547

Erdős problem 547

declared falsifiableerdos:548

Erdős problem 548

declared disprovederdos:549

Erdős problem 549

be sufficiently large. If

declared openerdos:550

Let

m_1\leq\cdots\leq m_k

and

n

T

is a tree on

n

vertices and

G

is the complete multipartite graph with vertex class sizes

m_1,\ldots,m_k

, prove that

R(T,G)\leq (\chi(G)-1)(R(T,K_{m_1,m_2})-1)+m_1

graph theoryramsey theoryN/A4 sources

declared decidableerdos:551

Erdős problem 551

declared openerdos:552

Erdős problem 552

graph theoryramsey theoryA006672

declared provederdos:553

Erdős problem 553

graph theoryramsey theoryA000791 · possible

declared openerdos:554

Erdős problem 554

declared openerdos:555

Erdős problem 555

graph theoryramsey theoryA389313 · possible

declared decidableerdos:556

Erdős problem 556

graph theoryramsey theoryA389335

declared openerdos:557

Erdős problem 557

declared openerdos:558

Erdős problem 558

declared disprovederdos:559

Erdős problem 559

declared openerdos:560

Erdős problem 560

declared openerdos:561

Erdős problem 561

True ↔ ∀ r ≥ 3, (fun n => Real.log^[r - 1] ↑(Combinatorics.hypergraphRamsey r n)) =Θ[Filter.atTop] fun n => ↑n

declared open · formalizederdos:562

graph theoryramsey theoryhypergraphspossible2 sources

declared openerdos:563

Erdős problem 563

graph theoryramsey theoryhypergraphsN/A

declared open · formalized · $500erdos:564

True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ 2 ^ (c * n) ≤ ↑(Combinatorics.hypergraphRamsey 3 n)

graph theoryramsey theoryhypergraphspossible2 sources

declared provederdos:565

Erdős problem 565

True ↔ ∀ (p : ℕ) (G : SimpleGraph (Fin p)), (∀ (S : Finset (Fin p)), 2 ≤ S.card → (SimpleGraph.induce (↑S) G).edgeSet.ncard ≤ 2 * S.card - 3) → ∃ c > 0, ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [inst : DecidableRel H.Adj], (∀ (v : Fin n), 0 < H.degree v) → ↑(G.sizeRamsey H) ≤ c * ↑H.edgeSet.ncard

declared open · formalizederdos:566

graph theoryramsey theoryN/A2 sources

declared open · formalizederdos:567

True ↔ Erdos567.Q3.IsRamseySizeLinear

graph theoryramsey theoryN/A2 sources

declared openerdos:568

Erdős problem 568

declared openerdos:569

Erdős problem 569

declared provederdos:570

Erdős problem 570

declared openerdos:571

Erdős problem 571

graph theoryturan numberN/A

declared openerdos:572

Erdős problem 572

graph theoryturan numberpossible

declared openerdos:573

Erdős problem 573

graph theoryturan numberA006856

declared disprovederdos:574

Erdős problem 574

graph theoryturan numberpossible

declared openerdos:575

Erdős problem 575

graph theoryturan numberN/A

declared openerdos:576

Erdős problem 576

graph theoryturan numberpossible

declared provederdos:577

Erdős problem 577

declared provederdos:578

Erdős problem 578

True ↔ ∀ (δ : ℝ), 0 < δ → ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), Erdos579.octahedron.Free G → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → c * ↑n ≤ ↑G.indepNum

declared open · formalizederdos:579

graph theoryturan numberN/A2 sources

declared decidableerdos:580

Erdős problem 580