@joshchen @amy Yes! Mario was/is essentially alone on Lean4Lean, and until now he was spending his Lean4Lean energy on the specification of the theory, the checker, and some meta-theory. But I think he would welcome anyone serious who wants to look at the set theory part