Предлагаю Вашему вниманию и обсуждению вот этот код для Coq. (it's self-contained, the standard library was only used.)
https://raw.githubusercontent.com/georg ... ter/Jech.vЭто сильно переделанный(как мне кажется, в лучшую сторону) и обильно дополненный вот этот репозиторий
https://github.com/coq-contribs/zfc .
Если у Воеводского были "Унивалентные основания математики" на Coq-e, то почему бы не воплощать в коде "Классические основания математики"? :)
Да, из теоретико-множественного есть Metamath (
http://us.metamath.org/ ), есть Mizar (
http://mizar.org/ ).
Первый - сложен в обращении, написан на С++, некоторые знакомые логики говорят, что система не очень хорошая(точную их аргументацию не воспроизведу). Второй - просто мне не знаком.
Прорешенный первые главы Йеха есть в интернете.
https://github.com/coq-contribs/zfc .
Деятельность, конечно, немного сектантская, но очень увлекательная и даже полезная. (многие, например, вообще не знают, чем отличаются, множества, классы, конгломераты,... и как с ними работать.)
p.s. есть слух, что где-то кто-то переводит Йеха на русский язык.
