Skip to content

Problems · Vela Mathematics Program

Narrowed tosolved (Lean) ×number theory ×Clear all

Problem ledger

10 problemsGraph view
declared solved (Lean) · formalizederdos:42
True ↔ ∀ M ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Set ℕ), A.IsMaximalSidonSetIn N → ∃ B ⊆ Set.Icc 1 N, IsSidon B ∧ B.ncard = M ∧ (A - A) ∩ (B - B) = {0}
number theorysidon setsadditive combinatoricsN/A6 sources
declared solved (Lean) · formalizederdos:419
{x | MapClusterPt x Filter.atTop Erdos419.factorialDivisorRatio} = Erdos419.limitPointSet
number theoryfactorialsN/A5 sources
declared solved (Lean) · formalizederdos:459
∀ {u : ℕ}, 2 ≤ u → u + 2 ≤ Erdos459.f u ∧ Erdos459.f u ≤ u ^ 2
number theoryprimesA2892805 sources
declared solved (Lean) · formalizederdos:648
(fun n => ↑(Erdos648.g n)) =Θ[Filter.atTop] fun n => √(↑n / Real.log ↑n)
number theoryA3917505 sources
declared solved (Lean) · formalizederdos:650
∀ (m : ℕ), Erdos650.f m = min m ⌈2 * √↑m⌉₊
number theoryA0274346 sources
declared solved (Lean) · formalizederdos:694
∀ (fmax fmin : ℕ → ℕ), (∀ (n : ℕ), IsGreatest (Nat.totient ⁻¹' {n}) (fmax n)) → (∀ (n : ℕ), IsLeast (Nat.totient ⁻¹' {n}) (fmin n)) → ∃ o, Filter.Tendsto o Filter.atTop (nhds 0) ∧ ∀ (x : ℕ), sSup {x_1 | ∃ n, ∃ (_ : n ≤ x) (_ : ∃ m, m.totient = n), ↑(fmax n) / ↑(fmin n) = x_1} = (Real.exp Real.eulerMascheroniConstant + o x) * Real.log (Real.log ↑x)
number theorypossible6 sources
declared solved (Lean)erdos:696
Erdős problem 696
number theorydivisorspossible4 sources
declared solved (Lean) · formalizederdos:862
False ↔ (fun N => Real.logb 2 ↑(Erdos862.numMaximalSidonSets N)) =o[Filter.atTop] fun N => ↑N ^ (1 / 2)
number theorysidon setsA3823955 sources
declared solved (Lean) · formalizederdos:1102
∀ (A : ℕ → ℕ), StrictMono A → Erdos1102.HasPropertyP (Set.range A) → Filter.Tendsto (fun j => ↑(A j) / ↑j) Filter.atTop Filter.atTop
number theoryN/A5 sources
declared solved (Lean) · formalizederdos:1190
∀ (ε : ℝ), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, scaleL m ^ (-1 - ε) < Erdos1190.eps m ∧ Erdos1190.eps m < scaleL m ^ (-1 + ε)
number theorycovering systemspossible6 sources

Search problems.science

Find a Problem, Result, source, or page