I want to prove the inequality $$\frac{\pi^2}{6}\le \int_0^{\infty} \sin(x^{\log x}) \ \mathrm dx $$
There are some obstacles I face: the indefinite integral cannot be expressed in terms of elementary functions,
Taylor series leads to a another function that cannot be expressed in terms of elementary functions. What else to try?
I don't think this can be done analytically but it can certainly be done by approximations. My general idea would be to approximate a few of the zeroes of the integrand which are bigger than 2 (I think 6 of them will suffice) noticing that the distance between consecutive zeroes is decreasing quickly. We can then estimate the value of the integral between each two consecutive zeros. The same is done for several of the zeroes less then 2 (this time 3 are enough). In this way we will arrive at an approximation between 1.69 and 1.64.
Notice that the value of the integral between each pair of consecutive zeroes is alternating between positive and negative but is strictly decreasing in absolute value (for $x>2$ and for $x<2$). If we've picked the approximated zeros correctly it will mean that the value of the integral in the (infinite) interval we have not examined will be positive, which concludes the proof.