Carneiro's Result in FFL

[SnO2WMaN]

Lean (3) can prove the consistency of ZFC + "there are ω inaaccessible cardinals". (Carneiro 2020)

[iehality]

Lean4 can prove the consistency of $\mathsf{ZFC} + \text{"there are } n \text{ inaccessibles"}$ for each standard $n \in \mathbb N$ (Universe.{n} is exactly the models of this axiom), but I think Lean4 cannot prove the consistency of $\mathsf{ZFC} + \text{"there are } \omega \text{ inaccessibles"}$.