DeepMind has formalized a theoretical result related to AI safety in Lean

Lean theorem prover seems to be the most convenient and practical (good enough for mathematicians to use it in real work, I am seeing plenty of such stories lately; there is a bit of controversy on whether to use Lean 3 or Lean 4).

The best quote according to "leanprover" twitter:

>Our favorite quote from the paper: "Monadic syntax is excellent for expressing stochastic algorithms, and working over finitely supported distributions avoids the need for integrability side conditions during proofs."

Links are in the comments.