Research points to there being a quadratic relationship between automated proof and code size: https://trustworthy.systems/publications/nictaabstracts/Matichuk_

Research points to there being a quadratic relationship between automated proof and code size: https://trustworthy.systems/publications/nictaabstracts/Matichuk_MAJKS_15.abstract https://trustworthy.systems/publications/nictaabstracts/Mati.... Specifically, the relationship is between the _specification_ and the proof, and it was done for proofs written in Isabelle and not Lean. The good news is that more and more automation is possible for proofs, so the effort to produce each proof line will likely go down over time. Still, the largest full program we've fully verified is much less than 100,000 LOC. seL4 (verified operating system) is around 10,000 lines IIRC.