Different proofs for the same theorem

Stream: mathlib4

[Fred Rajasekaran]

Does mathlib allow for different proofs of the same theorem? If so, how would these appear in mathlib (and if you could point me to any examples that already exist, that would be great). In particular, how is the naming of the theorems with different proofs done? If only one proof is allowed, how do you decide which proof deserves to be in mathlib?

For example, in random matrix theory, there are two different techniques (one being the moment method which is combinatorial and the other using resolvents and complex analysis) that can be used to prove the same theorems. Would one proof via the moment method and another via resolvents be allowed to coexist in mathlib, or is only one allowed?

[Eric Wieser]

If it breaks a tie, mathlib uses the proof which holds in greater generality, but of course in that the case they are no longer the same theorem!

[Eric Wieser]

Otherwise in general mathlib indeed keeps only one proof of each theorem; it's arguably intended as a library of theorems with verification that they are true, and not as a library of proofs.

[Yaël Dillies]

In the past what I've done is keep the old proof around in my repo, which I maintain

[Ruben Van de Velde]

But all proofs of the same theorem are equal :)

[Ruben Van de Velde]

Maybe those two proof approaches can be imagined as some kind of "induction principle" that you could wrap up into a lemma, and then you'd have two different lemmas that could both be in mathlib

[Ruben Van de Velde]

Otherwise that's only happened in Archive/