Think of Lean proofs as a kind of inductive proof where if you trust the kernel then you trust every proof the kernel says is true.

▲

agentultra 3 hours ago | parent [-]

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?

	▲	saithound 2 hours ago \| parent [-]
		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.