As I understand it, Lean's consistency strength is "\(\omega\) inaccessible cardinals":
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?
Suppose that while writing software, or doing research, or whatever, you need to pick between pursuing one of several mutually exclusive options. The basis point difference between how often you pick the platonically-correct option and how often an AI model does is multiplicative in effect, because any project of sufficient complexity has many of these decisions. Picking the correct option 80% of the time might work in the short term, but quickly spirals. Increasing correctness by 100 basis points is more valuable when your baseline is 90% correctness than 80%.
Practically, this means that even if human experts retain only a few basis points of advantage over AI models, humans might contribute more value in the limit than naively predicted.
