Problem 694

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

\max_{n\leq x}\frac{f_{\max}(n)}{f_{\min}(n)}

(where the maximum is restricted to those $n$ of the form $n=\phi(m)$ for some $m$ .)

Source: erdosproblems.com/694

Number theory

Wiki page

Status

SolvedAnswered

An accepted solution exists. Settled in another form, for example when its parts resolve differently or the question is open-ended.

Solved; the site's label is SOLVED (LEAN). The status-defining source is a five-page note whose title page credits "GPT-5.5 PRO", giving the asymptotic $(e^\gamma+o(1))\log\log x$ ; its claim page (Price, 2026) is accepted on the site's documented acceptance: the curator restated the proof in the site's thread on 2026-05-02 and the site records the result as the problem's resolution. Of the two external Lean developments, one proves that asymptotic, for its own definition of the ratio, from Mertens' product theorem and Linnik's theorem declared as axioms, and the other claims an unconditional proof through a module the corpus has not examined; this corpus has built neither, so they give no formalized evidence, and no refereed publication exists. See "Current assessment".

Problem 694

Status

Proof claims

Discussion