Vela Mathematics Program: problems

Narrowed tofalsifiable ×source:erdos-problems ×Clear all

Problem ledger

declared falsifiable · formalizederdos:23

∀ (n : ℕ), 0 < n → ∀ H ≤ Erdos23.blowupC5 n, H.IsBipartite → n ^ 2 ≤ ((Erdos23.blowupC5 n).edgeFinset \ H.edgeFinset).card

graph theoryA3896462 sources

declared falsifiable · formalized · $1000erdos:64

True ↔ ∀ (V : Type u_1) (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.minDegree ≥ 3 → ∃ k v c, k ≥ 2 ∧ c.IsCycle ∧ c.length = 2 ^ k

graph theorycyclesN/A2 sources

declared falsifiable · formalized · $100erdos:97

True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.ConvexIndep ↑A → ¬Erdos97.HasNEquidistantProperty 4 A

geometrydistancesconvexN/A2 sources

declared falsifiableerdos:106

f(n)

is the maximum total side length of

n

interior-disjoint squares packed in the unit square, is

f(k^2 + 1) = k

? An exact rational configuration packs

17

squares with total side length greater than

4

, refuting the identity at

k = 4

geometryN/A3 sources

declared falsifiable · formalized · $500erdos:107

sorry ↔ ∀ n ≥ 3, Erdos107.f n = 2 ^ (n - 2) + 1

geometryconvexA0000512 sources

declared falsifiable · $250erdos:114

Erdős problem 114

polynomialsanalysisN/A

declared falsifiable · formalized · $250erdos:128

True ↔ ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), (∀ (V' : Set V), 2 * V'.ncard + 1 ≥ Fintype.card V → 50 * (SimpleGraph.induce V' G).edgeSet.ncard > Fintype.card V ^ 2) → ¬G.CliqueFree 3

graph theoryN/A2 sources

declared falsifiableerdos:167

Erdős problem 167

graph theoryN/A

declared falsifiable · formalizederdos:242

∀ (n : ℕ), 2 < n → ∃ x y z, 1 ≤ x ∧ x < y ∧ y < z ∧ 4 / ↑n = 1 / ↑x + 1 / ↑y + 1 / ↑z

number theoryunit fractionsA073101 · A075245 · A075246 · A075247 · A075248 · A2871162 sources

declared falsifiable · formalizederdos:287

True ↔ ∀ (k : ℕ) (hk : 2 ≤ k) (s : Fin k → ℕ), StrictMono s → 1 < s ⟨0, ⋯⟩ → ∑ i, 1 / ↑(s i) = 1 → 3 ≤ Erdos287.max_gap k s

number theoryunit fractionsN/A2 sources

declared falsifiable · formalizederdos:375

True ↔ Erdos375.Erdos375Prop

number theoryN/A2 sources

declared falsifiable · formalizederdos:398

sorry ↔ {n | ∃ m, n.factorial + 1 = m ^ 2} = {4, 5, 7}

number theoryfactorialsA146968 · A1413992 sources

declared falsifiable · formalizederdos:458

True ↔ ∀ (k : ℕ), Erdos458.lcm_upto (Nat.nth Prime (k + 1) - 1) < Nat.nth Prime k * Erdos458.lcm_upto (Nat.nth Prime k)

number theoryprimesA0566042 sources

declared falsifiable · formalizederdos:488

True ↔ ∀ (A : Finset ℕ), A.Nonempty → 0 ∉ A → 1 ∉ A → ∀ (n m : ℕ), m > n → A.max ≤ ↑n → ↑{x ∈ Finset.Icc 1 m | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑m < 2 * ↑{x ∈ Finset.Icc 1 n | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑n

number theoryN/A3 sources

declared falsifiableerdos:548

Erdős problem 548

graph theoryN/A

declared falsifiableerdos:583

Erdős problem 583

graph theoryN/A

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 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 falsifiable · formalizederdos:699

True ↔ ∀ (n i j : ℕ), 1 ≤ i → i < j → j ≤ n / 2 → ∃ p, Nat.Prime p ∧ i ≤ p ∧ p ∣ (n.choose i).gcd (n.choose j)

number theorybinomial coefficientsN/A2 sources

declared falsifiable · formalizederdos:723

True ↔ ∀ {P L : Type} (x : Membership P L) (x_1 : Fintype P) (x_2 : Fintype L) (pp : Configuration.ProjectivePlane P L), IsPrimePow (Configuration.ProjectivePlane.order P L)

combinatoricsN/A2 sources

declared falsifiableerdos:743

Erdős problem 743

graph theoryN/A2 sources

declared falsifiable · formalizederdos:779

∀ n ≥ 1, have P := ∏ i ∈ Finset.range (n + 1), Nat.nth Nat.Prime i; ∃ p, Nat.Prime p ∧ Nat.Prime (P + p) ∧ Nat.nth Nat.Prime n < p ∧ p < P

number theoryprimesA0052352 sources

declared falsifiable · formalizederdos:982

∀ (n : ℕ), 3 ≤ n → ∀ (p : Fin n → EuclideanSpace ℝ (Fin 2)), Function.Injective p → EuclideanGeometry.IsConvexPolygon p → ∃ i, {d | ∃ j, j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2

geometryconvexdistancesA0045262 sources

declared falsifiableerdos:993

Erdős problem 993

graph theoryA000055 · possible

declared falsifiableerdos:1020

Erdős problem 1020

graph theoryhypergraphsN/A

declared falsifiable · formalizederdos:1041

∀ (n : ℕ) (f : Polynomial ℂ), n ≥ 2 → f.natDegree = n → f.Monic → f.rootSet ℂ ⊆ Metric.ball 0 1 → ∃ z₁ z₂, ∃ (_ : {z₁, z₂} ≤ f.roots), ∃ γ, Set.range ⇑γ ⊆ {z | ‖Polynomial.eval z f‖ < 1} ∧ Erdos1041.length (Set.range ⇑γ) < 2

analysisN/A3 sources

declared falsifiable · formalizederdos:1082

True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.NonTrilinear ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A

geometrydistancespossible3 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science