Oh, how long we've been waiting for this! ❤️‍🔥🎉 Great paper, but why default coq was chosen? That’s totally okay (and coq is still kinda default for interactive formal proving), but there is others production-ready strong modern instruments existing on Earth today. Just interesting why so.