According to [0], "Rocq’s kernel spans approximately 41K lines of OCaml code, while Lean’s kernel consists of approximately 8K lines of C++ code."

[0] https://dl.acm.org/doi/pdf/10.1145/3747511