From my understanding, the libraries written in Lean are also formally proven by the kernel. They may be hodge-podge or incomplete, but they are (by constructio

From my understanding, the libraries written in Lean are also formally proven by the kernel. They may be hodge-podge or incomplete, but they are (by construction) not "buggy" in a way that could lead to incorrect proofs, right?