Alternative proofs

Stream: maths

[Vladimir Goryachev]

If someone formalised a proof of a fact that was already in mathlib, but via a different route (e.g. algebraic closedness of C famously has many very different proofs), would this new proof be accepted to mathlib?

[Eric Wieser]

It doesn't make much sense for mathlib to contain multiple proofs of exactly the same statement, but sometimes the new proof can replace the old one if it is shorter, faster, or more readable.

[Eric Wieser]

However, a collection of different proof strategies of the same statement might still be a good fit for the archive folder, as they likely provide educational value to both human users and possibly linter metaprograms.

[Kevin Buzzard]

Putting them in the library means more work for the maintainers when in two years' time a proof breaks and you're nowhere to be found

[Kevin Buzzard]

This would be perfect either as a separate project (you could call it the algebraists closure project or whatever) and then write the code yourself and put a bunch of comments explaining what you're doing. That would be more helpful then a second mathematics proof. Mathlib is unfortunately many things but I don't think it's a repository for random proofs of things which we already have

[Kevin Buzzard]

I have plenty of students who have done random lean projects and just leave them up as github repos. There's some link to "student projects" on the Xena Project blog

[Vladimir Goryachev]

Thank you, this makes sense!

[Mario Carneiro]

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

[Alex J. Best]

I definitely think it would be nice to have things like that in archive, if only so that any useful api for the proof gets pr'ed to the main library too

[Filippo A. E. Nuccio]

Would it be reasonable then to add some doc of the official mathlib file pointing to the other repo? Because I would imagine that someone wondering about which proofs of algebraic closeness of $\mathbb{C}$ exist in mathlib would have nowhere else to look but in there.

[Johan Commelin]

Sure, I think that makes sense.

[Johan Commelin]

I guess src/field_theory/abel_ruffini.lean could do something similar