For the highlighted kernel (con-leche) , they postulate a set theory. Godel doesn't get involved because the proof is effectively saying Lean+ZFC entails Con(Lean), but even that isn't quite right, because the kernel doesn't include all the features of Lean. But even that isn't quite right, because they're actively modifying the kernel to be "simpler" to check.

It's a marketing post at the end of the day is what I'm trying to say. Regardless, Lean is probably the most trustworthy proof assistant on the planet at this point.

The question is if Godel matters in practice, or if its is just a limiting behaviour with infinite resources

> we will hit Godel

It seems no one understands how useless this theorem is in practice.