@jdw

Thanks for this link. Very interesting research.

But of course I'm working under the assumption that one cannot prove "False" in lean in the same way I work under the assumption that ZFC is consistent.

At some point you have to rely on an external system, but it's good to keep this in mind.