This article says that Ramanujan claimed that $$ \pi^2(x) < {ex \over \log x} \pi(x/e), $$ and that it is indeed true for $x$ sufficiently large. They really glaze over the proof though, and I'm having trouble filling in the gaps. I know how to prove (1.2) below, but not the next equation:
More specifically, when I apply the expansion with $n=4$ to $\pi(x/e)$, there appear terms of the form $(\log x - 1)^k$, which I cannot see how to reconcile with the $\log^k x$ terms from applying the expansion to $\pi(x)$.
I'm just asking for a nudge in the right direction, not a complete exposition.
Actually, now that I've looked at this more, can someone explain why (1.2) has an equality rather than $\pi(x) \sim \operatorname{li}(x) = \dotsb$ ?
The first citation of the paper linked is Bruce Berndt's book Ramanujan's Notebooks Part IV, which I think is the original source of this proof, alhough Ramanujan might have known it himself.
The direct application of (1.2) with $n=4$ to the left-hand side of the desired inequality is $$ \pi^2(x) = {x^2 \over \log^2 x} + {2x^2 \over \log^3 x} + {5x^2 \over \log^4 x} + {16 x^2 \over \log^5 x} + {64 x^2 \over \log^6 x} + O\left({x^2 \over \log^7 x}\right). $$ For the right-hand side it is: $$ {ex \over \log x} \pi(x/e) = {x^2 \over (\log x)(\log x - 1)} + {x^2 \over (\log x)(\log x - 1)^2} + {2x^2 \over (\log x)(\log x - 1)^3} + {6x^2 \over (\log x)(\log x - 1)^4} + {24x^2 \over (\log x)(\log x - 1)^5} + O \left({x^2 \over (\log x)(\log x - 1)^6}\right), $$ since $\log (x/e) = \log x - \log e = \log x - 1$. To deal with the powers of $(\log x - 1)$, they need to be expanded into a series in powers of $\log x$. For the first one, it is a geometric series: $$ {1 \over \log x - 1} = {1 \over \log x} \cdot {1 \over 1 - 1/(\log x)} = {1 \over \log x} \sum_{n=0}^\infty {1 \over \log^n x}. $$ Since only a finite number of terms are needed, the others can be found by raising this series to higher powers. Other methods to get the same series are the binomial series and differentiating the geometric series. Doing this amazingly gives $$ {ex \over \log x} \pi(x/e) = {x^2 \over \log^2 x} + {2x^2 \over \log^3 x} + {5x^2 \over \log^4 x} + {16 x^2 \over \log^5 x} + {\mathbf{65} x^2 \over \log^6 x} + O\left({x^2 \over \log^7 x}\right), $$ which is all that's needed.