What's the average length of a Lean proof?

Stream: general

[Ayhon]

Or in other words: how long does a proof need to get before you decide to slice it up in multiple different theorems?

I was thinking about the parallels between proof engineering and software development, and became curious about the question in the title. Of course, not all proofs are equal, and while I haven't found many proofs in the standard library which are longer than 10 lines (maybe I haven't been looking in the right places), I have seen other users talking about proofs over a thousand lines long (maybe they didn't mean in a single statement). In any case, I am curious about people's answers!

[Kenny Lau]

@Ayhon it's hard to have a hard number, but ideally 1 line long, but that's a very ideal case, most of the time it can take 5 lines, 10 lines, or even 20 lines; but the point is, it's considered (at least by me) a better thing to have 100 lemmas with short proofs, than to have 1 lemma that is 100 line long.

I always advocate for factoring out lemmas whenever possible.

[Mario Carneiro]

a proof needs to be very hard and specific to take more than 40 lines IME

[Mario Carneiro]

the average size of lemmas in mathlib tends to be smaller than in your big project depending on mathlib, because the nature of the formalization is slightly different

[Ayhon]

Kenny Lau said:

Ayhon it's hard to have a hard number, but ideally 1 line long, but that's a very ideal case, most of the time it can take 5 lines, 10 lines, or even 20 lines; but the point is, it's considered (at least by me) a better thing to have 100 lemmas with short proofs, than to have 1 lemma that is 100 line long.

I always advocate for factoring out lemmas whenever possible.

I agree, and I feel this stems a bit from the discipline of sofware engineering. I was just wondering how widespread it was among actual Lean users.

[Mario Carneiro]

in mathlib I would say 10 lines is more typical for hard proofs and 1 line for easy proofs

[Mario Carneiro]

Lemmas get longer than that not because they are very hard, but because they are very specific and there is no benefit to splitting out pieces of them without having the statements overwhelm the proof

[Mario Carneiro]

this is frequently a sign of bad or missing abstractions, so after refactoring the lemma length tends to go back down

[Kenny Lau]

For more concrete data, I used a Python script to look at my most recent file (#26804 Mathlib/SetTheory/ZFC/Model.lean), and here is the result:

1 : 71
2 : 2
3 : 6
4 : 1
5 : 1
6 : 5
7 : 1
8 : 4
9 : 1
11 : 1
13 : 1
19 : 1
20 : 1

[Kenny Lau]

i.e. most (71) of the proofs/definitions are 1 line long, but there are also a few that go up to 19 and 20 lines long

[Kenny Lau]

pie.png

[Martin Dvořák]

Most of my proofs are under 10 lines but some outliers are enormous (as a matter of fact, yesterday I finished a proof that has 1200 lines — that is the longest atomic proof I have ever written).

[Mario Carneiro]

1200 lines is a ridiculous size for a theorem, at that point you will have serious problems getting lean to be responsive on it

[Martin Dvořák]

The length doesn't make me happy, but splitting the lemma intro sublemmas would not make me happy either.

[Mario Carneiro]

it might make lean and your readers happy though

[Martin Dvořák]

Speaking of readers, I focus on minimizing the trusted code length, not on minimizing the total code length.

[Martin Dvořák]

By trusted code, I mean the statement of the final theorem and all definitions that are transitively reachable for the theorem statement. Currently we are at circa 300 lines of trusted code
https://github.com/Ivan-Sergeyev/seymour/blob/main/Seymour.lean
modulo some basic Mathlib definitions that hopefully nobody will be worried about.

If I were to invest my time into shortening something, it would definitely be shortening the trusted code, not the long proofs.

[Martin Dvořák]

Kenny Lau said:

have 100 lemmas with short proof

Having 100 lemmas with short proofs sounds great until you realize you have to name all of them.

[Mario Carneiro]

naming is hard but it's not that hard

[Mario Carneiro]

usually you can just start listing the constants used in the theorem statement until you get bored

[Bhavik Mehta]

For things which make up a long proof, you always have the good old private lemma aux47

[Martin Dvořák]

Yeah, I also do that (ok, not exactly that).

The real reason why I sometimes fail to break a lemma into smaller lemmas is that I would have to repeat too much context all over again. In the end, I usually isolate things that depend on something like 3 things in the local context into a separate lemma, but if it needed like 30 things, I keep it in place (some people would say inlined but this word really doesn't sound right in this context).

[Martin Dvořák]

I've heard some people use ProofData terms or something like that.

[Michael Rothgang]

I was about to say: that sounds exactly like you're looking for the ProofData pattern.

[Ayhon]

Hmmm, ReaderT ProofData <actual-proposition-here>?

[Michael Rothgang]

The best written explanation I know is https://zenn.dev/pandaman64/articles/lean-proof-data-en, but I believe some of Floris van Doorn's slides about the Carleson project also mention it.

[Martin Dvořák]

Thanks for the link!

[Weiyi Wang]

ProofData looks very similar to certain pattern in regular programming

[Winston Yin (尹維晨)]

The length of a proof seems to be a misguided line of thinking here. What we optimise for should be (1) reusability (opposite of code duplication) and (2) readability, both of which are only somewhat anti-correlated with length.

In analysis proofs, where one sometimes constructs long and complicated proof terms (such as particular functions), I only split out lemmas or definitions for these terms if I think they have a good chance of being reused in other similar proofs. This way, it is clear in the context of the current proof why this term is constructed in this form. On the other hand, if an argument seems to go on and on, or if the proof is multiply nested, then I will pick an intermediate step to split out as an auxiliary lemma, so that its goal state can be explicitly stated in the code, even if the lemma may never be reused.

I find it less readable to unnecessarily split out lots of smaller lemmas, as the logical flow of the main proof is disrupted as you reference these lemma statements. My 2¢.

[Martin Dvořák]

This is exactly my approach! Split proofs into multiple proofs and split files into multiple files based on their logic, not based on the number of lines.

[Patrick Massot]

Michael Rothgang said:

The best written explanation I know is https://zenn.dev/pandaman64/articles/lean-proof-data-en, but I believe some of Floris van Doorn's slides about the Carleson project also mention it.

It is also mentioned in the sphere eversion project paper.

[Michael Rothgang]

Paper link: https://dl.acm.org/doi/10.1145/3573105.3575688, arXiv version: https://arxiv.org/abs/2210.07746

[Kenny Lau]

Martin Dvořák said:

This is exactly my approach! Split proofs into multiple proofs and split files into multiple files based on their logic, not based on the number of lines.

Yes, of course the "number of lines" is not the real objective, but rather an indicator; but 1200 lines signifies to me that there might be some inefficiencies here

[metakuntyyy]

I don't know, sometimes constructions are just fugly and splitting them into multiple lemmas makes it so that you have very useless one off lemmas. At that point you just make searching for lemmas harder, as every specialised one off lemma clutters the code base. I'd then advocate to just make those lemmas private.

[Martin Dvořák]

Of course. The majority of lemmas in my code are private.

[Martin Dvořák]

Kenny Lau said:

1200 lines signifies to me that there might be some inefficiencies here

I am absolutely sure there must be an inefficiency somewhere in my proof.

[Niels Voss]

One advantage to having short proofs is not readability, but rather, reproducibility. When definitions in mathlib change, proofs break, and sometimes the best solution is to just rewrite the broken proofs from scratch. Keeping proofs short makes this possible.