As I understand it, Lean's consistency strength is "\(\omega\) inaccessible cardinals":

• ZFC + "there are \(\omega\) inaccessible cardinals" proves \(Con(Lean)\)
• Lean proves Con(ZFC + there are n inaccessible cardinals) for each \(n \in \omega\)

This means there are statements independent of ZFC that Lean can prove. (\(Con(ZFC)\) is an easy one).

As a result, it seems possible to end up in a very strange world where some statement (like P vs NP) is independent of ZFC, and yet we have a proof of it (or its negation) in Lean. Imagine trying to explain that result to the average scientist!

If we found ourselves in this hole, would we be able to dig ourselves out of it, or would it be a monumental task of reverse mathematics?