Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×formalized ×source:plby-lean-proofs ×Clear all

Problem ledger

6 problemsGraph view
declared open · formalizederdos:124
∀ {D : Finset ℕ}, (∀ d ∈ D, 3 ≤ d) → (∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ d ∈ D, Erdos124.sumsOfDistinctPowers d 0) → 1 ≤ ∑ d ∈ D, (↑d - 1)⁻¹
number theorybase representationsN/A4 sources
declared open · formalizederdos:264
¬Erdos264.IsIrrationalitySequence fun x => 2 ^ x
irrationalityN/A4 sources
declared open · formalizederdos:291
Erdos291.L 1 = 1 ∧ Erdos291.L 2 = 2 ∧ Erdos291.L 3 = 6 ∧ Erdos291.L 4 = 12
number theoryunit fractionsA1105663 sources
declared open · formalizederdos:424
Let a1=2a_1 = 2 and a2=3a_2 = 3 and continue the sequence by appending to a1,…,ana_1, \dots, a_n all possible values of aiaj−1a_ia_j - 1 with i≠ji \ne j. Is it true that the set of integers which eventually appear has positive density?
number theoryA0052444 sources
declared open · formalizederdos:1056
True ↔ ∀ k ≥ 2, ∃ p, ∃ (_ : Nat.Prime p), ∃ boundaries, ∃ (_ : StrictMono boundaries), Erdos1056.AllModProdEqualsOne p boundaries
number theoryA0604273 sources
declared open · formalizederdos:1095
Asymptotics.IsEquivalent Filter.atTop (fun k => Real.log ↑(Erdos1095.g k)) fun k => ↑k / Real.log ↑k
number theorybinomial coefficientsA0034584 sources

Search problems.science

Find a Problem, Result, source, or page