Vela Mathematics Program: problems

Narrowed toproved ×number theory ×Clear all

Problem ledger

83 problems · 1/2Number SourcesGraph 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 · $100erdos:29

Erdős problem 29

number theoryadditive basisN/A

declared provederdos:35

Erdős problem 35

number theoryadditive basisN/A

declared proved · formalizederdos:48

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

number theoryN/A2 sources

declared provederdos:49

Erdős problem 49

number theoryprimesA365339 · A365474

declared provederdos:53

Erdős problem 53

number theoryadditive combinatoricspossible

declared proved · formalizederdos:69

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

number theoryirrationalityA2621532 sources

declared proved · $250erdos:144

Erdős problem 144

number theorydivisorsA005279

declared provederdos:175

Erdős problem 175

number theorybinomial coefficientsN/A

declared proved · formalizederdos:219

∅ ∉ Erdos219.primeArithmeticProgressions

number theoryadditive combinatoricsprimesA005115 · A113827 · A1235562 sources

declared proved · $500erdos:220

Erdős problem 220

number theoryA322144

declared provederdos:235

Erdős problem 235

number theoryN/A

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 provederdos:240

Erdős problem 240

number theoryprimesN/A

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 provederdos:284

Erdős problem 284

number theoryunit fractionspossible

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 provederdos:286

Erdős problem 286

number theoryunit fractionsN/A

declared provederdos:292

Erdős problem 292

number theoryunit fractionsA092671

declared provederdos:294

Erdős problem 294

number theoryunit fractionspossible

declared provederdos:305

Erdős problem 305

number theoryunit fractionspossible

declared provederdos:308

Erdős problem 308

number theoryunit fractionspossible

declared provederdos:310

Erdős problem 310

number theoryunit fractionsN/A

declared provederdos:339

Erdős problem 339

number theoryadditive basisN/A

declared provederdos:343

Erdős problem 343

number theorycomplete sequencesN/A

declared provederdos:344

Erdős problem 344

number theorycomplete sequencesN/A

declared provederdos:356

Erdős problem 356

number theorypossible

declared proved · formalizederdos:358

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

number theoryadditive basisprimespossible3 sources

declared provederdos:362

Erdős problem 362

number theorypossible

declared provederdos:372

Erdős problem 372

number theoryA071870

declared provederdos:378

Erdős problem 378

number theorybinomial coefficientsN/A

declared provederdos:380

Erdős problem 380

number theoryA070003 · A388654 · A387054 · A3891003 sources

declared provederdos:384

Erdős problem 384

number theorybinomial coefficientsN/A

declared provederdos:391

Erdős problem 391

number theoryfactorialsA034258 · A034259

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 provederdos:405

Erdős problem 405

number theoryfactorialsN/A

declared provederdos:407

Erdős problem 407

number theorypossible · A387688

declared provederdos:437

Erdős problem 437

number theorypossible

declared provederdos:439

Erdős problem 439

number theoryramsey theoryN/A

declared provederdos:444

Erdős problem 444

number theorydivisorsN/A

declared provederdos:465

Erdős problem 465

number theoryN/A

declared provederdos:466

Erdős problem 466

number theoryN/A

declared provederdos:471

Erdős problem 471

number theorypossible

declared provederdos:473

Erdős problem 473

number theoryA055265

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 provederdos:491

Erdős problem 491

number theoryN/A

Problems · Vela Mathematics Program

Problem ledger

Search problems.science