[jpt4]

> Every definition and theorem in mathlib and this project have been checked by Lean’s trusted kernel, which computationally verifies that the proofs we have constructed are indeed correct.

From a foundational perspective, it is also important to note that this proof is one of equiconsistency between NF and the Lean kernel, which itself is handchecked. Mechanized theorem provers preserve that level of correctness imputed to them via outside injection, from humans or other out-of-band systems.

[randallholmes]

It certainly isnt a proof of equiconsistency between NF and the Lean kernel. The theory implemented in the Lean kernel is considerably stronger than NF.