Skip to content

Problems · Vela Mathematics Program

Narrowed todisproved (Lean) ×source:plby-lean-proofs ×Clear all

Problem ledger

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