Meckes is an expert on probability theory. His breakthrough came not here but on The n-Category Café, starting here:

https://golem.ph.utexas.edu/category/2023/01/a_curious_integral.html#c061933

and on until he says "Okay, here we go." He reduces the problem of showing

\[ \displaystyle{\frac{\pi}{8} - \int_0^\infty\cos(2x)\prod_{n=1}^\infty\cos\left(\frac{x}{n} \right) d x } \]

is small to the problem of showing it's improbable that the sum of certain random variables is bigger than 4. Then he uses Hoeffding's inequality!

(2/n)

I haven't carefully sorted out the details, but I believe Meckes has shown

\[ \displaystyle{\frac{\pi}{8} - \int_0^\infty\cos(2x)\prod_{n=1}^\infty\cos\left(\frac{x}{n} \right) d x < 0.00016 } \]

We'd need more sophisticated argument to do better, like show it's less than 10⁻⁴⁰. But this is pretty good! We now have human-comprehensible explanations of why this integral is less than π/8, but not much less.

I think this is a testament to the power of social media. But....

(3/n)

Mathstodon was not a big enough ecosystem to get the job done on its own. I had to summarize the state of the art in a blog article to attract the attention of the right expert.

I'm not saying this is a bad thing! It's just how it works. I often help solve problems that are too hard for me personally by running around and talking to different people until I bump into the right one. These people are not all sitting in one "place".

(4/n, n = 4)

@anton - One great thing about mathstodon.xyz is that it renders LaTeX, like

\[ \int e^{x^2} dx \]

Unfortunately I don't think any other instances of Mathstodon do that.

@johncarlosbaez @anton
For those viewing via the web-based view of another instance (like me): if you click the timestamp of John's post, you can view it directly on mathstodon.xyz - including nicely-rendered LateX 🙂

If you're using an app, find the "view in browser" option.