Vela Mathematics Program: problems

Narrowed toproved ×source:erdos-problems ×Clear all

Problem ledger

210 problems · 2/5Number SourcesGraph view

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

Erdős problem 255

discrepancyN/A

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

Erdős problem 395

analysisN/A

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:485

Erdős problem 485

analysispolynomialspossible2 sources

declared provederdos:491

Erdős problem 491

number theoryN/A

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

Erdős problem 496

number theorydiophantine approximationN/A

declared provederdos:515

Erdős problem 515

analysisN/A

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

Erdős problem 518

graph theoryramsey theoryN/A

declared provederdos:523

Erdős problem 523

analysisprobabilitypolynomialsN/A

declared provederdos:525

Erdős problem 525

analysisprobabilitypolynomialspossible

declared provederdos:527

Erdős problem 527

analysisprobabilityN/A

declared provederdos:546

Erdős problem 546

graph theoryramsey theorypossible

declared provederdos:553

Erdős problem 553

graph theoryramsey theoryA000791 · possible

declared provederdos:565

Erdős problem 565

graph theoryramsey theorypossible

declared provederdos:570

Erdős problem 570

graph theoryramsey theoryN/A

Problems · Vela Mathematics Program

Problem ledger

Search problems.science