Comment by sheafification

It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.

I guess it could be AI turtles checking and summarizing all the way down, but is that any more credible than a single AI checking it? I doubt it.