Skip to content

Problems · Vela Mathematics Program

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

Problem ledger

10 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 openerdos:367
Erdős problem 367
number theoryA0575213 sources
declared openerdos:368
Erdős problem 368
number theoryA0743993 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 openerdos:866
Estimate the least excess gk(N)g_k(N) forcing kk integers whose pairwise sums all lie in a dense subset of {1,…,2N}\{1, \dots, 2N\}; in particular, determine the positive variant h4(n)h_4(n).
number theoryadditive combinatoricspossible5 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
declared openerdos:1100
Erdős problem 1100
number theorydivisorsA325864 · possible2 sources

Search problems.science

Find a Problem, Result, source, or page