あのノート書いた方だったんですね。数学書３００冊・・・。
ZFCから形式的に証明なんてすごいですね。
Whitehead の本はZFCで証明できるのでしょうが、
今のLurieの数学などはできないような気がします。
そこで ZFCではなくhomotopy type theory とかCoqはどうでしょうか。
型理論の方が集合論よりも多くを扱えるそうです。
こちらの方がはるかに厳密で、一部の基本群の計算の自動化もやっています。
一般コホモロジーとかホモトピー論はカテゴリーがたくさんでますし、
JechやKunennを読むよりカテゴリーの方がリターンは大きいでしょうね。