To echo the sibling comment, that answer is specifically referring to the type theory behind Lean (which I’ve heard is pretty weird in a lot of ways, albeit usu

To echo the sibling comment, that answer is specifically referring to the type theory behind Lean (which I’ve heard is pretty weird in a lot of ways, albeit usually in service of usability). Many type theories are weaker than ZFC, or even ZF, at least if I correctly skimmed https://proofassistants.stackexchange.com/a/1210/7 https://proofassistants.stackexchange.com/a/1210/7.