The Type Theory of Lean
#論文
#lean
https://github.com/digama0/lean-type-theory
Corollary6.8
Lean is consistent if
$ \mathsf{ZFC} + \{\text{there are $n$ inaccessible cardinals} \mid n \in \omega\}
is.