>>57
実際一階述語論理に基づいたZFCがLeanライブラリにないのでうまく証明が構成できないということは1年前から言ってる
ただそういう問題でもなさそうだとも分かってきたから今回の弱気な発言とショルツェ側の新メンバー招集なんだと思う