The de Bruijn ratio for formalizing informal mathematical proofs in the Lean theorem prover is often 20 to 1 or higher