Skip to content

Problems · Vela Mathematics Program

Narrowed tofalsifiable ×formalized ×source:formal-conjectures ×Clear all

Problem ledger

19 problemsGraph view
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 falsifiable · formalized · $500erdos:107
sorry ↔ ∀ n ≥ 3, Erdos107.f n = 2 ^ (n - 2) + 1
geometryconvexA0000512 sources
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 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 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 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 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

Search problems.science

Find a Problem, Result, source, or page