Erdős Problem a Daythe open tracker

Erdős Problem #49

PROVED LEANdatabase updated 2026-08-24

The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

The largest size of a set \(A\subseteq\{1,\ldots,N\}\) on which Euler's totient function is strictly increasing.

The largest size of a set \(A\subseteq\{1,\ldots,N\}\) on which Euler's totient function is non-decreasing.

Let \(A=\{a_1<\cdots<a_t\}\subseteq \{1,\ldots,N\}\) be such that \(\phi(a_1)<\cdots<\phi(a_t)\). The primes are such an example. Are they the largest possible? Can one show that \(\lvert A\rvert<(1+o(1))\pi(N)\) or even \(\lvert A\rvert=o(N)\)? Erdős remarks that the last conjecture is probably easy, and that similar questions can be asked about \(\sigma(n)\). Solved by Tao [Ta24d], who proved that \[ \lvert A\rvert \leq \left(1+O\left(\frac{(\log\log x)^5}{\log x}\right)\right)\pi(x).\] In [Er95c] Erdős further asks about the situation when \(\phi(a_1)\leq \cdots \leq \phi(a_t)\). See also [415](https://www.erdosproblems.com/415).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/49.
Prizenone
Topicsnumber theory, primes
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA365339, A365474
Original pageerdosproblems.com/49
NOBODY HAS SENT US AN ATTEMPT YET

If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.