Update:

On the first try of using chatgpt agent, it surfaced a reference from 2015 which contained a proof of the result in question.

The paper was on an unrelated topic. It was hidden in the appendix and was missing many relevant keywords.

https://twitter.com/damekdavis/status/1944837669218894123

The bound had also been stated but not proven in a 1994 paper. The 2015 paper gave a decently simple self-contained proof.

This question had been asked to a few prominent people in this field. They didn't know, so it wasn't well known. I'm sure they could have figured it out.

Update: I didn't solve the problem

Over the last 6 months, I've tried pretty hard to use LLMs to solve a (I think) not too difficult problem in a nearby field (learning theory).

The answers have gone from terrible to plausible, and I actually understand the problem better now.

https://twitter.com/damekdavis/status/1943359962794856718

I now have references that are highly relevant and several pathways that might work.

Unfortunately, every argument proposed has had (in retrospect) a fairly obvious hole in it.

Next formalization is the "gradient inequality" for smooth convex functions.

The proof (next tweet) is a few sentences of English.

My lean4 proof (below) is roughly 350 lines of code.

1/n The proof in English is short. It is a consequence of the simple convex analysis fact:

If f is a convex function such that f(0) = 0 and f(y)>= o(y), then f(y) \geq 0 globally.

I proved a super simple helper lemma.
In English the proof is 1 line.
In lean4, it took me around 50 lines of code.
1/n The proof took me around 5 hours (lol).
Any help shortening would be appreciated.

2/n

Cool technique. Reminds me of the the Cramer-Chernoff method, which applies a Markov type inequality and optimizes to find the "best" parameter....

https://twitter.com/sp_monte_carlo/status/1696506912680857945

Carrying out the optimization bounds the tail deviation as the exponential of the Fenchel conjugate of the log moment generating function of the r.v.