Skip to content

Problems Β· Vela Mathematics Program

Problem ledger

1,217 problems Β· 12/25NumberSourcesGraph view
declared decidableerdos:551
ErdΕ‘s problem 551
graph theoryramsey theoryN/A
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
graph theoryramsey theorypossible
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
graph theoryramsey theoryN/A
declared openerdos:558
ErdΕ‘s problem 558
graph theoryramsey theorypossible
declared disprovederdos:559
ErdΕ‘s problem 559
graph theoryramsey theorypossible
declared openerdos:560
ErdΕ‘s problem 560
graph theoryramsey theorypossible
declared openerdos:561
ErdΕ‘s problem 561
graph theoryramsey theoryN/A
declared open Β· formalizederdos:562
True ↔ βˆ€ r β‰₯ 3, (fun n => Real.log^[r - 1] ↑(Combinatorics.hypergraphRamsey r n)) =Θ[Filter.atTop] fun n => ↑n
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
graph theoryramsey theorypossible
declared open Β· formalizederdos:566
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
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
graph theoryramsey theoryN/A
declared openerdos:569
ErdΕ‘s problem 569
graph theoryramsey theoryN/A
declared provederdos:570
ErdΕ‘s problem 570
graph theoryramsey theoryN/A
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
graph theoryN/A
declared provederdos:578
ErdΕ‘s problem 578
graph theoryN/A
declared open Β· formalizederdos:579
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
graph theoryturan numberN/A2 sources
declared decidableerdos:580
ErdΕ‘s problem 580
graph theoryN/A
declared solvederdos:581
ErdΕ‘s problem 581
graph theorypossible
declared proved (Lean) Β· formalized Β· $100erdos:582
True ↔ βˆƒ V x G, G.CliqueFree 4 ∧ Erdos582.EdgeRamseyTriangle G
graph theoryramsey theoryN/A5 sources
declared falsifiableerdos:583
ErdΕ‘s problem 583
graph theoryN/A
declared openerdos:584
Must every graph with nn vertices and Ξ΄n2\delta n^2 edges contain large subgraphs in which every two edges lie on specified short cycles? A dense high-girth construction refutes the statement when Ξ΄\delta may shrink with nn.
graph theorycyclesN/A2 sources
declared openerdos:585
ErdΕ‘s problem 585
graph theorycyclespossible
declared disprovederdos:586
ErdΕ‘s problem 586
number theorycovering systemsN/A
declared solved Β· formalizederdos:587
βˆƒ O > 0, βˆƒ O' > 0, βˆ€αΆ  (N : β„•) in Filter.atTop, ↑(Erdos587.MaxNotSqSum N) ≀ O' * Real.nthRoot 3 ↑N * Real.log ↑N ^ O
number theoryA3720402 sources
declared open Β· $100erdos:588
ErdΕ‘s problem 588
geometryA006065 Β· A008997
declared openerdos:589
ErdΕ‘s problem 589
geometrypossible
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 Β· formalizederdos:600
True ↔ βˆ€ (r : β„•), 2 ≀ r β†’ Filter.Tendsto (fun n => ↑(Erdos600.eFunction n (r + 1)) - ↑(Erdos600.eFunction n r)) Filter.atTop Filter.atTop
graph theorypossible2 sources

Search problems.science

Find a Problem, Result, source, or page