Proof for strict inequality $\pi(ab) > \pi(a)\pi(b)$? I asked about the very similar $\pi(ab)\geq \pi(a)\pi(b)$ a while ago, and this is indeed a proven result for $a,b\geq \sqrt{53}$.
Empirically, the stricter $\pi(ab)>\pi(a)\pi(b)$ looks true so long as either $a$ or $b$ is $\geq 23$.
It also seems to pretty immediately fall out of the PNT, a la
$$\pi(ab)\sim\frac{ab}{\log(ab)}>\frac{ab}{\log(a)\log(b)}\sim \pi(a)\pi(b)$$
given sufficiently large $a,b$.

If someone can point me to a paper, give pointers/work out on how this proof could be done, or if applicable, explain why this is probably not provable, I'll consider this answered.
If you can verify my proof below or give some solid feedback, that would work too.

Okay, I have a first attempt. For $x\geq 17$, Wikipedia gives the bounds
$$\frac x {\log x} < \pi(x) \tag{1}$$
$$\pi(x) < 1.25506 \frac x {\log x}. \tag{2}$$
From applying $(2)$ twice, we have
$$\pi(a)\pi(b) < 1.25506^2 \cdot  \frac{ab}{\log(a)\log(b)}.\tag{3}$$
From $(1)$, we get $$\frac{ab}{\log(ab)} < \pi(ab).\tag{4}$$
It only remains to connect them:
$$1.25506^2 \cdot  \frac{ab}{\log(a)\log(b)} < \frac{ab}{\log(ab)}.\tag{5}$$
From trial and error, letting $a,b \geq 24$ seems sufficient to satisfy $(5)$. We put the pieces together and get the final inequality chain
$$\pi(a)\pi(b) < 1.25506^2 \cdot  \frac{ab}{\log(a)\log(b)} <\frac{ab}{\log(ab)} < \pi(ab). \tag{6}$$
This gives $\pi(a)\pi(b)<\pi(ab)$ for $a,b\geq 24$. Have I gone awry somewhere or does this work?

To finish the proof , we only have to show $(5)$ for $a,b\ge 24$
WLOG we can assume $24\le a\le b$ and therefore $\ln(a)\le \ln(b)$.
Then we have $$\frac{\ln(a)\cdot \ln(b)}{\ln(ab)}=\frac{\ln(a)\cdot \ln(b)}{\ln(a)+\ln(b)}\ge \frac{\ln(24)\cdot \ln(b)}{2\ln(b)}=\frac{\ln(24)}{2}>1.25506^2$$ hence $$\frac{\ln(a)\cdot \ln(b)}{\ln(ab)}>1.25506^2$$
which is equivalent to $(5)$ finishing the proof.
