Formalizing different proofs of the same theorem

Stream: general

[Seewoo Lee]

Hi, I want to ask a question on a project I have in my mind. I found that most (all?) of the theorems in mathlib have a single proof, and I definitely think that it worths to formalize other proofs of the same theorem somewhere, but I don't know if there's a place in mathlib repository for such a purpose (maybe Archive, but I'm not sure about it). For example, I think the quadratic reciprocity is a perfect example of a theorem which is important and with at least 20 different proofs in Oswald Baumgart's book (for a moment, let's not discuss about when two proofs are the same or different). There's one proof in mathlib, but only one (with slightly different versions, not different proofs). I can definitely make a repository and ask people to contribute, but I want to ask your opinions first. It doesn't need to be the quadratic reciprocity - any theorem with many proofs would also count (e.g. infinitude of primes, Pythagoras theorem, ...).

[Winston Yin (尹維晨)]

I can see the value of this in several ways. It allows certain theorems to be proven through a different file dependency. Maybe this has performance benefits. It also serves as a test of the existing library to see if anything is missing. It can also be pedagogical to present different approaches. However, I worry that it has the opportunity cost of labour that could be used to prove new theorems that do all of the above while expanding mathlib.

[Kim Morrison]

I think for quadratric reciprocity or infinitude of primes or pythagoras, there is an easy answer: write a beautiful file for Archive showcasing all the different proofs!

Once you get past some short list of famous statements with famously many proofs, I think the value of having alternate proofs drops rapidly.

[Yaël Dillies]

As an example, LeanCamCombi contains a proof of the Cauchy-Davenport theorem from Kneser's theorem

[Michael Rothgang]

I also agree with Winston: this can be useful.
It's an interesting question if formalising the n-th proof of Pythagoras/infinitude of primes/quadratic reciprocity/... is worth it --- but that shouldn't stop you from doing it. (It might only mean not many people join your project.)

[Seewoo Lee]

Thanks! At least it looks worth to do, and also I can put things under Archive as suggested without making new repo. This is mainly for my own practice, but feel free to join if you are also interested. I may look up infinitude of primes first (easier than quadratic reciprocity?).

[Yaël Dillies]

Note that the proof of quadratic reciprocity in mathlib was recently changed by Michael Stoll. It previously was the combinatorial proof

[Seewoo Lee]

Oh that's interesting to know, may I ask why? Also, does it mean that the proof is completely replaced, or the old one remains somewhere in the master branch?

[Yaël Dillies]

The point was that the new proof is more general (don't quote me on this). I think the old proof was completely removed, but you will need to check

[Michael Stoll]

The ingredients of the combinatorial proof are still there: file#Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas