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.