Comment by andriy_koval

> Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.

I am aware, also I am not sure why you wrote all of this. Your unknown to me "first course" claims to be some authority of formalization purity?