A critical examination of Lean4

LessWrong user Milo Moses published an article critically examining the trustworthiness of the formal proof tool Lean4. He points out that Lean4 is based on its own dependent type theory rather than ZFC, and that there is currently no public proof that it is consistent relative to ZFC plus arbitrarily large cardinal axioms, and says he is 90% confident that the Lean4 currently on GitHub contains a True=False proof that the community would regard as a bug. The article mentions that after soundness bug #14576, Lean FRO found seven more kernel bugs, and Leo de Moura said AI is very good at exploiting kernel soundness bugs, and that research on nested inductive types is still in its early stages and may bring hidden dangers that are consistent but behave out of control. The author also criticizes Anthropic for turning off the sandbox that isolates untrusted proof code when running the comparator in the formalization of Fermat's Last Theorem, and says that having GPT-6 Astra search for an embedding of Lean4 into set theory took about 25 hours and thousands of dollars without success.