Released heavy-tailed-noise-lean, a Lean 4 formalization of lower bounds for strict-K=1 stochastic optimization under heavy-tailed noise.