Maybe what you mean is that kernels of proof assistants must be small. Here I am referring to a geometry processing kernel (that is formally verified by a proof assistant). The implementation of the algorithm can be very long, the proof that it conforms to the spec can be very long. But lean checks the proof. And so you only have to trust the spec and that the lean proof assistant is correct.

In the 93 lines I assumed a reviewer already trusts that the kernel of the Lean proof assistants is correct. We have to trust somethings.

▲

agentultra 3 hours ago | parent [-]

What I’m wondering about is why we don’t need to understand/verify the generated kernel and only the spec?

Is there an implicit trust we must put in that kernel?

	▲	permute 2 hours ago \| parent [-]
		The implementation of a function is in the CSG/Impl folder. A proof is in the CSG/Proof folder. They are both imported and tied together in the human reviewed file in a theorem that makes a mathematical statement about the function. Lean checks mechanically that the theorems are proven via the supplied proofs. Here you have to trust the Lean checker, but neither the proof nor the implementation. Then you know that the statement in the file you reviewed holds about that function.