You might be interested in the con leche project. A subset of the Lean theorem prover which was sufficient to prove the entire contents of Lean mathlib has been proven consistent.
It seems like very important work and was discussed in the article with some caveats.
Maybe I am being too skeptical about something I don't understand very well, but I'm not completely convinced it means no more kernel bugs will be found.
What does it mean for con leche if further lean kernel bugs are found? What if the bugs affect con leche's correctness itself?
> What does it mean for con leche if further lean kernel bugs are found?
There is so much that needs to go wrong with our current understanding of math, so that it's a bit like asking "What if we find tachyons that allow us to send messages into the past?" Most likely we will not find them.
Yes, I am. The kernel soundness bugs in con leche that allow to prove False, to be precise. Crashes, hardware bugs, cosmic rays flipping bits and such don't count as qualifying bugs.
