Skip to content

Erdős problem 694

Let f_\max(n) be the largest mm such that ϕ(m)=n\phi(m) = n, and f_\min(n) be the smallest such mm, where ϕ\phi is Euler's totient function. Investigate \max_{n\leq x}\frac{f_\max(n)}{f_\min(n)}.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/694.lean

Formal Conjectures

FormalConjectures/ErdosProblems/694.leanErdos694.erdos_6948 linesExact file
∀ (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)
SolvedStatement only, no proof

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:694
  • PLBY Lean proofsErdosProblems.Erdos694

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page