Vela Mathematics Program: problems

Problem ledger

1,217 problems · 13/25Number SourcesGraph view

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 · $500erdos:604

Erdős problem 604

geometrydistancespossible

declared provederdos:605

Erdős problem 605

geometrydistancespossible

declared solvederdos:606

Erdős problem 606

geometryN/A

declared proved · $250erdos:607

Erdős problem 607

geometrypossible

declared disproved (Lean)erdos:608

Erdős problem 608

graph theoryN/A2 sources

declared openerdos:609

Erdős problem 609

graph theoryramsey theorypossible

declared proved (Lean)erdos:610

Erdős problem 610

graph theorypossible4 sources

declared openerdos:611

Erdős problem 611

graph theoryN/A

declared openerdos:612

Erdős problem 612

graph theoryN/A

declared disproved (Lean) · formalizederdos:613

False ↔ ∀ n ≥ 3, ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], G.edgeFinset.card = (2 * n + 1).choose 2 - n.choose 2 - 1 → ∃ B D, ∀ [DecidableRel B.Adj] [inst_3 : DecidableRel D.Adj], G = B ⊔ D ∧ B.IsBipartite ∧ ∀ (v : V), D.degree v < n

graph theoryN/A5 sources

declared openerdos:614

Erdős problem 614

graph theorypossible

declared disproved · formalizederdos:615

False ↔ ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (1 / 8 - c) * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ¬G.CliqueFree 4 ∨ ↑n / Real.log ↑n ≤ ↑G.indepNum

graph theoryramsey theorypossible2 sources

declared openerdos:616

Erdős problem 616

graph theoryN/A2 sources

declared falsifiable · formalizederdos:617

∀ r ≥ 3, ∀ {V : Type} [inst : Fintype V] [DecidableEq V], Fintype.card V = r ^ 2 + 1 → ∀ (coloring : Sym2 V → Fin r), ∃ S k, S.card = r + 1 ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

graph theoryN/A2 sources

declared proved (Lean) · formalizederdos:618

True ↔ ∀ (G : (n : ℕ) → SimpleGraph (Fin n)), (∀ (n : ℕ), (G n).CliqueFree 3) → ((fun n => ↑(G n).maxDegree) =o[Filter.atTop] fun n => ↑n ^ (1 / 2)) → (fun n => ↑(Erdos618.h2 (G n))) =o[Filter.atTop] fun n => ↑n ^ 2

graph theoryN/A5 sources

declared solved (Lean) · formalizederdos:619

False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), G.Connected → G.CliqueFree 3 → ↑(Erdos619.minNewEdges 4 G) < (1 - c) * ↑(Fintype.card V)

graph theoryN/A5 sources

declared openerdos:620

Erdős problem 620

graph theorypossible

declared proved (Lean) · formalizederdos:621

True ↔ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (a t : ℕ), IsGreatest {k | ∃ A ⊆ G.edgeFinset, A.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → ({s(x, y), s(y, z), s(x, z)} ∩ A).card ≤ 1} a → IsLeast {k | ∃ T ⊆ G.edgeFinset, T.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → (T ∩ {s(x, y), s(y, z), s(x, z)}).Nonempty} t → 4 * (a + t) ≤ n ^ 2

graph theoryN/A5 sources

declared provederdos:622

Erdős problem 622

graph theorypossible

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 open · formalizederdos:624

Filter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTop

combinatoricspossible2 sources

declared open · $1000erdos:625

Erdős problem 625

graph theorychromatic numberN/A

declared openerdos:626

Erdős problem 626

graph theorychromatic numbercyclespossible

declared openerdos:627

Erdős problem 627

graph theorychromatic numberpossible

declared falsifiable · formalizederdos:628

∀ (V : Type u_1) [Fintype V] (G : SimpleGraph V) (k : ℕ), G.chromaticNumber = ↑k → G.CliqueFree k → ∀ (a b : ℕ), a ≥ 2 → b ≥ 2 → a + b = k + 1 → ∃ s, (SimpleGraph.induce s G).chromaticNumber ≥ ↑a ∧ (SimpleGraph.induce sᶜ G).chromaticNumber ≥ ↑b

graph theorychromatic numberN/A2 sources

declared openerdos:629

Erdős problem 629

graph theorychromatic numberpossible2 sources

declared provederdos:630

Erdős problem 630

graph theorychromatic numberN/A

declared provederdos:631

Erdős problem 631

graph theorychromatic numberN/A

declared disprovederdos:632

Erdős problem 632

graph theorychromatic numberN/A

declared solved · formalized · $25erdos:633

∀ {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))}, Erdos633.IsCuttable n T → n ≠ 0

geometryN/A2 sources

declared open · $25erdos:634

Erdős problem 634

geometrypossible

declared openerdos:635

Erdős problem 635

number theoryN/A2 sources

declared provederdos:636

Erdős problem 636

graph theoryramsey theoryN/A

declared provederdos:637

Erdős problem 637

graph theoryramsey theoryN/A

declared openerdos:638

Erdős problem 638

graph theoryramsey theoryN/A

declared proved (Lean) · formalizederdos:639

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Sym2 (Fin n) → Fin 2), {e | ¬e.IsDiag ∧ ∀ (x y : Fin n), e = s(x, y) → ¬∃ z, z ≠ x ∧ z ≠ y ∧ C s(x, z) = C e ∧ C s(y, z) = C e}.ncard ≤ n ^ 2 / 4

graph theoryramsey theoryN/A5 sources

declared openerdos:640

Erdős problem 640

graph theorychromatic numberN/A

declared disprovederdos:641

Erdős problem 641

graph theoryN/A

declared openerdos:642

Erdős problem 642

graph theorycyclespossible

declared openerdos:643

Erdős problem 643

graph theoryhypergraphspossible

declared openerdos:644

Erdős problem 644

combinatoricspossible

declared proved (Lean) · formalizederdos:645

∀ (c : ℕ → Bool), ∃ x d, 0 < x ∧ x < d ∧ ∃ C, c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C

number theoryadditive combinatoricsramsey theoryN/A5 sources

declared proved (Lean) · formalizederdos:646

True ↔ ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → {n | ∀ p ∈ S, Even (padicValNat p n.factorial)}.Infinite

number theoryfactorialsN/A5 sources

declared verifiable · formalized · £25erdos:647

sorry ↔ ∃ n > 24, ⨆ m, ↑m + (ArithmeticFunction.sigma 0) ↑m ≤ n + 2

number theoryA062249 · A0872804 sources

declared solved (Lean) · formalizederdos:648

(fun n => ↑(Erdos648.g n)) =Θ[Filter.atTop] fun n => √(↑n / Real.log ↑n)

number theoryA3917505 sources

declared disproved (Lean) · formalizederdos:649

False ↔ ∀ (p q : ℕ), Nat.Prime p → Nat.Prime q → ∃ n, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q

number theorypossible5 sources

declared solved (Lean) · formalizederdos:650

∀ (m : ℕ), Erdos650.f m = min m ⌈2 * √↑m⌉₊

number theoryA0274346 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science