Skip to content

Problems · Vela Mathematics Program

Narrowed todisproved (Lean) ×Clear all

Problem ledger

63 problems · 2/2NumberSourcesGraph view
declared disproved (Lean) · formalizederdos:967
False ↔ ∀ (a : ℕ → ℕ), StrictMono a → 1 < a 0 → (Summable fun k => 1 / ↑(a k)) → ∀ (t : ℝ), 1 + ∑' (k : ℕ), Erdos967.summand t (a k) ≠ 0
number theoryanalysisN/A5 sources
declared disproved (Lean) · formalizederdos:990
False ↔ ∃ C, ∀ (f : Polynomial ℂ), f.coeff 0 ≠ 0 → ∀ (α β : ℝ), 0 ≤ α → α ≤ β → β ≤ 2 * Real.pi → |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤ C * √(↑f.support.card * Real.log (Erdos990.M f))
analysisN/A6 sources
declared disproved (Lean) · formalizederdos:1034
False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), ↑n ^ 2 / 4 < ↑G.edgeSet.ncard → ∃ T, G.IsNClique 3 T ∧ ∃ Y, Erdos1034.JoinedToTwo G T Y ∧ (1 / 2 - ε) * ↑n < ↑Y.card
graph theorypossible5 sources
declared disproved (Lean) · formalizederdos:1037
False ↔ ∀ (ε : ℝ), 0 < ε → ∀ (C : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (∀ (d : ℕ), {v | (G.neighborSet v).ncard = d}.ncard ≤ 2) → (1 / 2 + ε) * ↑n < ↑(Set.range fun v => (G.neighborSet v).ncard).ncard → ∃ s, Erdos1037.IsTrivialSet G s ∧ C * Real.log ↑n < ↑s.ncard
graph theoryN/A5 sources
declared disproved (Lean) · formalizederdos:1043
False ↔ ∀ (f : Polynomial ℂ), f.Monic → f.degree ≥ 1 → ∃ u, ‖u‖ = 1 ∧ MeasureTheory.volume (⇑(ℝ ∙ u).orthogonalProjection '' Erdos1043.levelSet f) ≤ 2
analysisN/A5 sources
declared disproved (Lean) · formalizederdos:1047
False ↔ ∀ (f : Polynomial ℂ) (m : ℕ) (c : ℝ), f.Monic → (f.rootSet ℂ).ncard = m → 0 < c → (Erdos1047.componentsIn (Erdos1047.sublevelSet f c)).ncard = m → ∀ t ∈ Erdos1047.componentsIn (Erdos1047.sublevelSet f c), Convex ℝ t
analysisN/A5 sources
declared disproved (Lean) · formalizederdos:1048
False ↔ ∀ (r : ℝ) (f : Polynomial ℂ), r < 2 → f.Monic → f.degree ≥ 1 → (∀ z ∈ f.roots, ‖z‖ ≤ r) → ∃ z ∈ Erdos1048.openLevelSet f, ENNReal.ofReal (2 - r) < Metric.ediam (connectedComponentIn (Erdos1048.openLevelSet f) z)
analysisN/A5 sources
declared disproved (Lean) · formalizederdos:1067
False ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ H, H.coe.chromaticCardinal = Cardinal.aleph 1 ∧ H.coe.InfinitelyConnected
graph theoryset theoryN/A5 sources
declared disproved (Lean) · formalizederdos:1080
False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] [Nonempty V] (G : SimpleGraph V) (X Y : Set V), Erdos1080.IsBipartition G X Y → X.ncard = ⌊↑(Fintype.card V) ^ (2 / 3)⌋₊ → ↑G.edgeSet.ncard ≥ c * ↑(Fintype.card V) → ∃ v walk, walk.IsCycle ∧ walk.length = 6
graph theorypossible5 sources
declared disproved (Lean) · £10erdos:1134
Erdős problem 1134
number theoryA1856613 sources
declared disproved (Lean) · formalizederdos:1138
False ↔ ∀ C > 1, Asymptotics.IsEquivalent Erdos1138.snd_gt_half_fst (Erdos1138.primeCount_Ioc_mul_const C) fun x => match x with | (x, y) => C * ↑(Erdos1138.sup_primeGap x) / Real.log y
number theoryprimespossible6 sources
declared disproved (Lean) · formalizederdos:1141
False ↔ Infinite ↑{n | Erdos1141.Erdos1141Prop n}
number theoryprimesA2145836 sources
declared disproved (Lean)erdos:1197
Erdős problem 1197
analysisN/A5 sources

Search problems.science

Find a Problem, Result, source, or page