Gotta double check.
You must log in or register to comment.
They're using Lean for the proofing for those interested. It's a pretty neat system from the little I've seen. Uses a graph to represent the proof path and pre-requisites, and it's kinda integrated with TeX.
I found a YouTube link in your comment. Here are links to the same video on alternative frontends that protect your privacy: