alt Hacker NewsThink 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.
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.
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?