ELBO in Lean 4
Formalizing the evidence lower bound in Lean.
A Lean 4 formalization of the evidence lower bound for finite, strictly positive distributions, including the ELBO decomposition and equality at the exact posterior.
The repository also includes learning resources that connect the formal proof to the underlying mathematics.