Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×divisors ×Clear all

Problem ledger

14 problemsGraph view
declared open · formalizederdos:18
∀ᶠ (n : ℕ) in Filter.atTop, Erdos18.practicalH n.factorial < n
number theorydivisorsfactorialsA0051532 sources
declared open · formalizederdos:450
How large must y(ε,n)y(\varepsilon, n) be so that every interval (x,x+y)(x, x+y) contains at most εy\varepsilon y integers having a divisor in (n,2n)(n, 2n)? The candidate proof gives the sharp fixed-ε\varepsilon order y=Θε(n)y = \Theta_\varepsilon(n), uniformly in the translate.
number theorydivisorsN/A4 sources
declared openerdos:468
Erdős problem 468
number theorydivisorsA167485 · A387502 · A387503
declared open · formalized · $10erdos:470
sorry ↔ ∃ n, n.Weird ∧ Odd n
number theorydivisorsA006037 · A0029752 sources
declared openerdos:693
Erdős problem 693
number theorydivisorsA391118 · possible
declared open · formalizederdos:859
∃ c₁ > 0, ∃ c₂ > 0, ∃ d, (∀ t > 0, (Erdos859.DivisorSumSet t).HasDensity (d t)) ∧ Asymptotics.IsEquivalent Filter.atTop (fun t => d t) fun t => c₁ / Real.log ↑t ^ c₂
number theorydivisorsN/A2 sources
declared open · formalizederdos:885
True ↔ ∀ k ≥ 1, ∃ Ns, (∀ n ∈ Ns, 1 ≤ n) ∧ Ns.card = k ∧ (⋂ n ∈ Ns, Erdos885.factorDifferenceSet n).ncard ≥ k
number theorydivisorsN/A2 sources
declared open · formalizederdos:886
sorry ↔ ∀ ε > 0, ∃ K, ∀ᶠ (n : ℕ) in Filter.atTop, (Erdos886.Erdos886Divisors n ε 1).card ≤ K
number theorydivisorsN/A2 sources
declared open · formalizederdos:887
∀ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card ≤ sorry
number theorydivisorsN/A2 sources
declared open · formalizederdos:893
True ↔ Filter.Tendsto (fun n => ↑(Erdos893.f (2 * n)) / ↑(Erdos893.f n)) Filter.atTop Filter.atTop
number theorydivisorsA046801 · possible3 sources
declared open · formalizederdos:945
True ↔ Erdos945.Erdos945Prop
number theorydivisorspossible · A0488922 sources
declared open · formalizederdos:975
True ↔ ∀ (f : Polynomial ℤ), f.natDegree ≠ 0 → Irreducible f → (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) → ∃ c > 0, Filter.Tendsto (fun x => Erdos975.Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)
number theorydivisorsA147807 · possible2 sources
declared open · formalizederdos:1054
sorry ↔ (fun n => ↑(Erdos1054.f n)) =o[Filter.atTop] fun n => ↑n
number theorydivisorsA1674853 sources
declared openerdos:1100
Erdős problem 1100
number theorydivisorsA325864 · possible2 sources

Search problems.science

Find a Problem, Result, source, or page