No transcript alas, but a fairly information-dense interview. Among the things I've learned is that the Coq/SSReflect and Lean communities have very different approaches to formalizing mathematics, with the former almost tailored to discrete maths and the latter to a more classical (Cantor-Hilbert-style) development of mathematics. I'm wondering whether it will ever be easy to port proofs from one system to the other...

And yes, both communities have their own downwards-incompatible version nightmares.