How much redundancy should Mathlib have?

Stream: mathlib4

[J. J. Issai (project started by GRP)]

Judging from the activity here on channel, there is a lot of generalization, refactoring, and manipulation of structures to handle a lot of instances of proof. Mathlib is supposed to "handle it all", or most of it, being the 21st century (or at least for this decade) foundations of mathematics.

How much redundancy is there? More specifically, how much redundancy is planned?

For this post, the main kind of redundancy is two or more proofs of the same concept. For purposes of pedagogy alone, I would like to see a proof of $\sum_{1 \le k \le n} k = \frac{n(n+1)}{2}$ by induction, by algebra, and by "geometry" (stacking blocks, however that might look in Lean). There are more elaborate examples, but I imagine there are other reasons for redundancy.

Note: the redundant proofs might be instantiated in an alternate repository like Batteries or Plausible. They might be of such a nature that they are less perfomant but more robust, and not subject to breakage upon addition of new features and extensions to mathlib. Then those who would trade stability for performance could use this alternate repository.

Has this idea/issue been raised before? Where can I read more about the philosophy in the design of Mathlib?

[Eric Wieser]

My understanding is that mathlib is not at all interested in collecting proofs, and really only cares about proven statements

[Eric Wieser]

(a possible exception is the Archive folder)

[J. J. Issai (project started by GRP)]

So if I have an acceptable proof of the Goldbach conjecture in Lean, someone runs the kernel on it, and if the proof is accepted, then the proof is forgotten and only the (formalized) conclusion is added into Mathlib? (To extremize an example.)

[Eric Wieser]

well, the proof has to be in mathlib so as to demonstrate it was really proved in the latest version, but we only want the "best" proof

[Jireh Loreaux]

In a very literal sense, Lean itself forgets (or doesn't care) about which proof you have. That is, if P : Prop is some statement and you produce two proofs proof1 : P and proof2 : P of that statement, then proof1 = proof2 by definition in Lean.

Now, that's not to say it is impossible for readers of a proof to extract value from the structure of the proof, as of course there is value in such things. However, at this time it is not Mathlib's purview to collect different proofs. Nevertheless, this could be done in a repository downstream of Mathlib. If you wanted to be a bit cheeky, you could call such a repo TheBook.

[Michael Rothgang]

There are already two repositories formalising proofs from The Book (by Ziegler and Aigner), fwiw.

[Michael Rothgang]

I see two exceptions to the rule above:

• a second really nice proof, which is added to the Archive (this is very very rare)
• a second proof develops lots of nice theory: in this case, the supporting theory should be added (but the proof itself not). As a case in point, there are two in-flight proofs that the alternating group on at least five letters is simple, following different strategies: the theory-building ingredients of both should be merged, but only one proof of the result.

[J. J. Issai (project started by GRP)]

Jireh Loreaux said:

Now, that's not to say it is impossible for readers of a proof to extract value from the structure of the proof, as of course there is value in such things. However, at this time it is not Mathlib's purview to collect different proofs. Nevertheless, this could be done in a repository downstream of Mathlib. If you wanted to be a bit cheeky, you could call such a repo TheBook.

All due respect to (appropriate unicode rendering of Erdos Pal), I would name it MyBook. Indeed, this question is inspired by a rewrite of one of his ?!slick!? proofs.

So perhaps for other purposes, such a collection of other proofs should not be in Mathlib proper, but in another repository (let's call it Alternative, or Alsoran) for the purpose of pedagogy or robustness.

Regarding Michael's exceptions, I have a hard time imagining the theory of a second proof being added without at least an isomorphic entry also added that would be a restatement of the proof existing in Mathlib. Is there not room in (the ecosystem of) Mathlib for a statement and a restatement?

[Bryan Gin-ge Chen]

I don't have too much to add to what other maintainers have already said, but here's a post in my starred messages from when this came up a few years ago:

Mario Carneiro said:

Note that it is very common for different proofs (in the usual mathematical sense) of the same statement to generalize in different directions, so having multiple generalized statements is one way to get alternate proofs in mathlib

[J. J. Issai (project started by GRP)]

Hmm. So it sounds like after I submit my proof of Goldbach's Theorem, I could then submit my proof of BachGold's Theorem (for every even n > 100, n = p +q where p is a prime of the form 4n+1 and q is another prime), and both statements would be accepted?

[J. J. Issai (project started by GRP)]

Bryan Gin-ge Chen said:

I don't have too much to add to what other maintainers have already said, but here's a post in my starred messages from when this came up a few years ago:

Mario Carneiro said:

Note that it is very common for different proofs (in the usual mathematical sense) of the same statement to generalize in different directions, so having multiple generalized statements is one way to get alternate proofs in mathlib

Can you post a link to the context around this? It sounds quite intriguing.

[Bryan Gin-ge Chen]

The "said" is a link that should take you to the original thread.

[J. J. Issai (project started by GRP)]

Sorry, the glare here is hiding the blue. Thanks.