Vela Mathematics Program: problems

Narrowed toproved ×formalized ×source:erdos-problems ×Clear all

Problem ledger

40 problemsGraph view

declared proved · formalized · $10000erdos:4

True ↔ ∀ C > 0, Erdos4.Erdos4For C

number theoryprimesA0023862 sources

declared proved · formalized · $100erdos:6

{n | primeGap n < primeGap (n + 1) ∧ primeGap (n + 1) < primeGap (n + 2)}.Infinite

number theoryprimesA3352772 sources

declared proved · formalized · $100erdos:13

∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos13.IsForbiddenTripleFree A → ↑A.card ≤ ↑N / 3 + C

number theoryA0022642 sources

declared proved · formalizederdos:22

True ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ G, G.CliqueFree 4 ∧ ↑G.indepNum ≤ ε * ↑n ∧ ↑n ^ 2 / 8 ≤ ↑G.edgeFinset.card

graph theorypossible2 sources

declared proved · formalizederdos:48

True ↔ {(n, m) | n.totient = (ArithmeticFunction.sigma 1) m}.Infinite

number theoryN/A2 sources

declared proved · formalized · $500erdos:67

∀ (f : ℕ → ↥{-1, 1}) (C : ℝ), 0 < C → ∃ d ≥ 1, ∃ m ≥ 1, C < |∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))|

discrepancyA181740 · A2376952 sources

declared proved · formalizederdos:69

Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + 2)) / 2 ^ (n + 2))

number theoryirrationalityA2621532 sources

declared proved · formalizederdos:109

∀ (A : Set ℕ), A.upperDensity > 0 → ∃ B C, B.Infinite ∧ C.Infinite ∧ B + C ⊆ A

additive combinatoricsN/A2 sources

declared proved · formalized · $1000erdos:139

∀ (k : ℕ), 1 < k → Filter.Tendsto (fun N => ↑(Erdos139.r k N) / ↑N) Filter.atTop (nhds 0)

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources

declared proved · formalizederdos:152

True ↔ Filter.Tendsto Erdos152.f Filter.atTop Filter.atTop

sidon setsN/A4 sources

declared proved · formalizederdos:219

∅ ∉ Erdos219.primeArithmeticProgressions

number theoryadditive combinatoricsprimesA005115 · A113827 · A1235562 sources

declared proved · formalizederdos:228

True ↔ ∃ c₁ c₂, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p, p.degree = ↑n ∧ (∀ i ≤ n, p.coeff i = 1 ∨ p.coeff i = -1) ∧ ∀ (z : ℂ), ‖z‖ = 1 → √↑n < c₁ * ‖Polynomial.eval z p‖ ∧ ‖Polynomial.eval z p‖ < c₂ * √↑n

analysispolynomialsN/A2 sources

declared proved · formalizederdos:239

True ↔ ∀ (f : ℕ → ℝ), (∀ n ≥ 1, f n = 1 ∨ f n = -1) ∧ (∀ (m n : ℕ), m.Coprime n → f (m * n) = f m * f n) ∧ f 1 = 1 → ∃ L, Filter.Tendsto (fun N => (∑ n ∈ Finset.Icc 1 N, f n) / ↑N) Filter.atTop (nhds L)

number theoryN/A2 sources

declared proved · formalizederdos:245

True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard / N) Filter.atTop (nhds 0) → 3 ≤ Filter.limsup (fun N => ↑((A + A) ∩ Set.Icc 1 ⌊N⌋₊).ncard / ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard) Filter.atTop

additive combinatoricsN/A2 sources

declared proved · formalizederdos:248

∃ C > 0, {n | ∀ k ≥ 1, ↑(ArithmeticFunction.cardDistinctFactors (n + k)) ≤ C * ↑k}.Infinite

number theoryN/A2 sources

declared proved · formalizederdos:250

(∀ (x : ℝ), HasSum (fun n => ↑((ArithmeticFunction.sigma 1) n) / 2 ^ n) x → Irrational x) ↔ True

number theoryirrationalityA0667662 sources

declared proved · formalizederdos:277

True ↔ ∀ (c : ℝ), ∃ n, ↑((ArithmeticFunction.sigma 1) n) > c * ↑n ∧ ∀ (m : StrictCoveringSystem ℤ), ∃ i, ↑n ∉ m.moduli i

number theorycovering systemsN/A2 sources

declared proved · formalizederdos:285

True ↔ ∀ (f : ℕ → ℕ) (S : Set ℕ), S = {k | ∃ n, StrictMono n ∧ 0 ∉ Set.range n ∧ 1 = ∑ i, 1 / ↑(n i)} → (∀ k ∈ S, IsLeast {x | ∃ n, ∃ (_ : StrictMono n) (_ : 0 ∉ Set.range n) (_ : 1 = ∑ i, 1 / ↑(n i)), n (Fin.last k) = x} (f k)) → ∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ k ∈ S, ↑(f k) = (1 + o k) * Real.exp 1 / (Real.exp 1 - 1) * (↑k + 1)

number theoryunit fractionsA0306592 sources

declared proved · formalizederdos:358

True ↔ ∃ A, StrictMono A ∧ Filter.Tendsto (Erdos358.f A) Filter.atTop Filter.atTop

number theoryadditive basisprimespossible3 sources

declared proved · formalizederdos:402

∀ (A : Finset ℕ), 0 ∉ A → A.Nonempty → ∃ a ∈ A, ∃ b ∈ A, ↑(a.gcd b) ≤ ↑a / ↑A.card

number theoryN/A2 sources

declared proved · formalizederdos:480

True ↔ ∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ⨅ n, Filter.liminf (fun m => ↑↑n * |x (m + ↑n) - x m|) Filter.atTop ≤ 1 / √5

number theoryN/A3 sources

declared proved · formalizederdos:494

∀ (k card p : ℕ), Nat.Prime p → k ∈ Set.Ioo 0 p → p ∣ card → Erdos494.Erdos494Unique k card

analysisadditive combinatoricsN/A2 sources

declared proved · formalizederdos:516

∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (n : ℕ), a n ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → Erdos516.OfFiniteOrder f → Filter.limsup (fun r => Erdos516.ratio r f) Filter.atTop = 1

analysisN/A2 sources

declared proved · formalized · $250erdos:590

OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0) (Ordinal.omega0 ^ Ordinal.omega0) 3

set theoryramsey theoryN/A2 sources

declared proved · formalized · $250erdos:591

True ↔ OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) 3

set theoryramsey theoryN/A3 sources

declared proved · formalizederdos:594

True ↔ ∀ (V : Type) (G : SimpleGraph V), IsEmpty (G.Coloring ℕ) → ∃ N, ∀ (k : ℕ), N ≤ k → ∃ v w, w.IsCycle ∧ w.length = 2 * k + 1

graph theoryset theoryN/A2 sources

declared proved · formalizederdos:599

True ↔ ∀ (V : Type) (G : SimpleGraph V) (A B : Set V), Disjoint A B → G.IsIndepSet A → G.IsIndepSet B → ∃ ι a b p S, (∀ (i : ι), a i ∈ A) ∧ (∀ (i : ι), b i ∈ B) ∧ (∀ (i : ι), (p i).IsPath) ∧ (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧ S ⊆ {v | ∃ i, v ∈ (p i).support} ∧ (∀ (i : ι), ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧ ∀ a' ∈ A, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

graph theoryset theoryN/A2 sources

declared proved · formalizederdos:697

∀ (m : ℕ) (α : ℝ), ∃ δ, {n | ∃ d, d ≡ 1 [MOD m] ∧ ↑d ∈ Set.Ioo 1 (Real.exp (↑m ^ α)) ∧ d ∣ n}.HasDensity δ

number theorydivisorsN/A2 sources

declared proved · formalizederdos:755

True ↔ ∃ o, (o =o[Filter.atTop] fun x => 1) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos755.TUnit 6 n) ≤ (1 / 27 + o n) * ↑n ^ 3

geometrypossible2 sources

declared proved · formalizederdos:822

True ↔ (Set.range fun n => n + n.totient).HasPosDensity

number theoryA121048 · A1550852 sources

declared proved · formalized · $25erdos:825

True ↔ ∃ C, ∃ (_ : C > 0), ∀ (n : ℕ), ↑((ArithmeticFunction.sigma 1) n) > C * ↑n → ∃ s ⊆ n.properDivisors, n = s.sum id

number theoryA006037 · A3302442 sources

declared proved · formalizederdos:851

∀ ε ∈ Set.Ioo 0 1, ∃ r d, (Erdos851.TwoPowAddSet r).HasDensity d ∧ 1 - ε ≤ d

number theoryN/A4 sources

declared proved · formalizederdos:899

True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N) Filter.atTop (nhds 0) → Filter.limsup (fun N => ↑((A - A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop = ⊤

additive combinatoricsN/A2 sources

declared proved · formalizederdos:937

True ↔ {p | Erdos937.IsCoprimePowerfulAP4 p.1 p.2}.Infinite

number theorypossible2 sources

declared proved · formalizederdos:946

{n | (ArithmeticFunction.sigma 0) n = (ArithmeticFunction.sigma 0) (n + 1)}.Infinite

number theorydivisorsA005237 · A2847832 sources

declared proved · formalizederdos:987

True ↔ ∀ (x : ℕ → ℝ), (∀ (j : ℕ), x j ∈ Set.Ioo 0 1) → Filter.limsup (fun k => Erdos987.A x k) Filter.atTop = ⊤

analysisdiscrepancyN/A4 sources

declared proved · formalizederdos:1064

{n | n.totient > (n - n.totient).totient}.HasDensity 1

number theoryA051488 · A0514872 sources

declared proved · formalizederdos:1096

True ↔ ∃ ε > 0, ∀ (q : ℝ), 1 < q → q < 1 + ε → ∀ (x : ℕ → ℝ), StrictMono x → Set.range x = {x | ∃ S, ∑ i ∈ S, q ^ i = x} → Filter.Tendsto (fun k => x (k + 1) - x k) Filter.atTop (nhds 0)

number theoryN/A2 sources

declared proved · formalizederdos:1105

True ↔ ∀ (k : ℕ), 3 ≤ k → (fun n => ↑((SimpleGraph.cycleGraph k).antiRamseyNum n) - ((↑k - 2) / 2 + 1 / (↑k - 1)) * ↑n) =O[Filter.atTop] fun x => 1

graph theoryramsey theorypossible3 sources

declared proved · formalizederdos:1214

True ↔ ∀ (x y : ℕ), x ≥ 1 → y ≥ 1 → (∀ n ≥ 1, {p | Nat.Prime p ∧ p ∣ x ^ n - 1} = {p | Nat.Prime p ∧ p ∣ y ^ n - 1}) → x = y

number theoryN/A2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science