[carterschonwald]

Here’s a nice paper and talk by the mathlib folks at a January 2020 proofs and certified programs conf https://popl20.sigplan.org/details/CPP-2020-papers/14/The-Le...

Might be fun reading for folks