Skip to content

Problems · Vela Mathematics Program

Narrowed todisproved (Lean) ×source:erdos-ai-contributions-wiki ×Clear all

Problem ledger

59 problems · 2/2NumberSourcesGraph view
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