Leanの無矛盾性について
Lean
メモ
随分前に集合論の先輩からLeanってどの程度には強いんですか？と言われて
$ \sf ZFC
になんか足したやつですと曖昧に答えて濁した
今でもこの実装なら，次のCpr 6.8が成立しているらしい．
https://github.com/digama0/lean-type-theory
どこかにpdfがあったはず
https://github.com/digama0/lean-type-theory/releases
Cor 6.8
$ \mathsf{ZFC} + \{ n \in \omega \mid \text{there are $n$ inacessible cardinals} \}
が無矛盾ならLeanも無矛盾．