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

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-Lean-mathematical-library https://popl20.sigplan.org/details/CPP-2020-papers/14/The-Le... Might be fun reading for folks