报告人: 张丘平（oCaU）

时间：2021年4月3日（星期六）14：00

会议线上地址：腾讯会议496 394 976

摘要：本次报告将介绍张丘平（oCaU）基于Coq做的传统集合论教材的形式化。其内容讲包括：替代公理，选择公理，类型论自然数的嵌入，序数与基数的定义，阿列夫数的定义，以及Veblen不动点定理的证明。

报告人简介：张丘平2016年硕士毕业于日本筑波大学计算机专业。后就职于日本瑞可利公司从事IT开发继5年。基于个人兴趣自2020年始自学coq及公理化集合论。现业余时间致力于传统集合论教材的coq形式化。（知乎，GitHub）