Right, I’m thinking of the de Bruijin criterion applied to the generated kernel in this case. That generated kernel sounds large, and being generated, I’m curious as to why or how we don’t have to verify/understand it?
You're confused because the word kernel is used in two different senses.
The "generated kernel" refers to a "geometric modeling kernel", which has absolutely nothing to do with the proof-checking kernel that the de Bruijn criterion talks about. The proof can be verified by Lean's ordinary proof-checker, or external checkers.
Okay so in the sense of Lean’s kernel, we can trust it as long as we understand it. Verifying it cannot be automated therefore, according to the criterion, it must be small so that it can be verified by a human.
Does it not also follow that we should also understand the geometric kernel using a similar criterion or, what I’m trying to understand, is there a mechanism in play in this project that verifies it for us automatically so that we only need to understand the specification and can trust the generated parts?
There are some pointers to answer this question myself that I’m looking into. Neat stuff.
The "generated kernel" refers to a "geometric modeling kernel", which has absolutely nothing to do with the proof-checking kernel that the de Bruijn criterion talks about. The proof can be verified by Lean's ordinary proof-checker, or external checkers.