The De Bruijn ratio is often 20 lines of Lean code or more for each line of informal mathematics.

“And it's very high, 20 to 1, often higher. Mathematicians don't generally see the reason to invest that additional time just to verify the correctness of something.”