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.