---

Claim. Let $f_{\max}(n)$ and $f_{\min}(n)$ be the largest and smallest $m$ with $\phi(m)=n$. Theorem 2.1 of the note Totient fibre extremes: with the maximum over totient values $n\le x$,

$$\max_{n\le x,\ n\in\phi(\mathbb N)}\frac{f_{\max}(n)}{f_{\min}(n)} =(e^\gamma+o(1))\log\log x \qquad(x\to\infty).$$

This answers the "Investigate" question of Problem 694 with an asymptotic formula, which the site records as the problem's resolution. The upper bound is the classical extremal order $\max_{m\le T}m/\phi(m)=(e^\gamma+o(1))\log\log T$ applied to $M=f_{\max}(n)\le2n^2$; the lower bound builds, for each $y$, a collision $\phi(a_y)=\phi(b_y)$ with $b_y/a_y=(e^\gamma+o(1))\log y$ from a prime $\ell\equiv1\pmod{\prod_{p\le y}(p-1)}$ supplied by Linnik's theorem, and takes $y$ a constant times $\log x$. The construction is not explicit: without fixed Linnik constants no concrete pair is exhibited, a point a thread post of 2026-05-01 makes, so the result is asymptotic only.

Depends on. Nothing in this wiki. The note takes the prime number theorem in the form $\vartheta(y)\sim y$, Mertens' product theorem and Linnik's theorem at statement level.

The note's library card is the source card, with its Theorem 2.1 page; the card follows its proofs and nothing is independently reviewed by this project. The title page credits "GPT-5.5 PRO" and names no person; the hosting repository's README credits the proof to "Liam Price + GPT-5.5 Pro", and the site credits GPT-5.5 Pro, prompted by Price. Price posted the claim in the site's thread on 2026-05-01. This page is named for Price as the human submitter of an AI-assisted result, with GPT-5.5 Pro as the system; the attribution is recorded as the sources state it.

Acceptance. Reviewed, on the site's documented acceptance. The result was first posted in the site's thread on 2026-05-01 as a link to the Overleaf document linked above; the PDF linked above is the copy in the Shashi456/erdos-formalizations repository, whose creation stamp is 2 May 2026. On 2026-05-02 the site's curator, Thomas Bloom, called it a neat elementary proof and restated both bounds in their own words in the thread, the site's remarks record the asymptotic as proved, the page was edited that day, and the community database records the status solved (Lean) on 2026-05-06; Bloom is independent of the claimant. The same day Nat Sothanaphan posted in the thread that a standard check found no issues, while noting that the note cites nothing for the classical upper bound. No refereed publication or arXiv version exists.

Lean. Not formalized evidence: this corpus has not built or audited the developments, so they give no formalized evidence. The thread post of 2026-05-03 announced the first development, Erdos/P694/Proof.lean, which proves the asymptotic for its own supremum definition of the ratio with Mertens' product theorem and Linnik's theorem declared as axioms; Sothanaphan confirmed on 2026-05-03 that its statement matches the note and the axiomatized statements are correctly stated. A post of 2026-06-05 reports Mertens' theorem formalized, leaving Linnik's as the only axiom, and the file of 2026-08-25 in Boris Alexeev's lean-proofs repository (GitHub plby) claims an unconditional proof through a module the corpus has not examined. The developments present themselves as formalizations of the note (the lean-proofs file names GPT-5.5 Pro and Price as its informal authors and lists the thread's post 6202 and the Overleaf note among its URLs), so they are links on this page and not an independent proof. The formal-conjectures statement is a sorry body with no formal_proof attribute and differs in form from the developments' theorem; it is not a formalization link, and the problem page's "Formalization and the Lean label" section records the developments and this copy.