---

Claim. Both clauses of the corrected Statement of Problem 49 hold. Let $M(x)$ be the largest size of a set $\{a_1<\cdots<a_t\}$ of positive integers up to $x$ with $\phi(a_1)\le\cdots\le\phi(a_t)$. Theorem 1.1 of T. Tao, Monotone Nondecreasing Sequences of the Euler Totient Function, states: "We have $M(x) \leq \left(1 + O\left(\frac{\log_2^5 x}{\log x}\right)\right) \frac{x}{\log x}$ for all $x \geq 10$", and, by the prime number theorem, in the form (1.2),

$$\pi(x)\le M(x)\le\left(1+O\left(\frac{(\log\log x)^5}{\log x}\right)\right)\pi(x),$$

the lower bound coming from the primes, on which $\phi(p)=p-1$ increases. A set on which $\phi$ is strictly increasing is in particular one on which it is nondecreasing, so every strict example $A\subseteq\{1,\ldots,N\}$ has $\lvert A\rvert\le M(N)=(1+o(1))\pi(N)$, and since $\pi(N)=o(N)$, also $\lvert A\rvert=o(N)$ (the strict transfer). This answers both clauses of the corrected Statement; it does not decide Erdős's exact conjecture, recorded on the problem page, that the primes are a largest strict example.

Covers. Both clauses of the corrected Statement: every strict example $A\subseteq\{1,\ldots,N\}$ has $\lvert A\rvert<(1+o(1))\pi(N)$, and so $\lvert A\rvert=o(N)$. Erdős's exact conjecture, that the primes are a largest strict example, is not part of the corrected Statement and is not covered.

Depends on. The strict transfer, the passage from Tao's nondecreasing maximum to strict examples.

Acceptance. Reviewed: the site's curator, Thomas F. Bloom, independent of the author, labels the problem PROVED (LEAN) and credits the bound to this paper [Ta24d]; the source digest compiles the complete proof chain. Refereed publication: La Matematica 3(2) (2024), 793–820, doi:10.1007/s44007-024-00115-z, received 10 September 2023, accepted 30 April 2024, published online 23 May 2024. The page is dated by the first arXiv posting, arXiv:2309.02325 v1 of 5 September 2023.

Formalization. The file src/latest/ErdosProblems/Erdos49.lean of Boris Alexeev's lean-proofs repository, linked above at its main-branch commit of 4 September 2026, declares itself a Lean formalization of a solution to Erdős Problem 49 with Terence Tao as informal author and Codex and GPT-5.6 Sol as formal authors. It states erdos_49, the strict $o(N)$ clause, and erdos_49_quantitative, Tao's nondecreasing bound with its rate; neither asserts that the primes are a largest strict example. This corpus has not built or audited the development, so the page lists no formalized evidence.