Where does proof code go?

Stream: new members

[Alex Altair]

Hi all, I have a general question about how the Lean community works (or aspires to work)

[Alex Altair]

I understand that mathlib is currently being built up to be the standard library that contains the foundations for mathematical fields. On the other end of the spectrum, researchers can write Lean proofs of their own theorems, and keep these proofs somewhere publicly accessible, like github. I guess I have a couple questions;

[Alex Altair]

1) Are there currently any libraries that are standardized, community-maintained projects that are more specialized than mathlib, but less specialized than the work of individual people? What (or who) determines what goes into mathlib itself?

[Alex Altair]

2) For individual researchers who do produce their own proofs, is there any standardized place for those to be hosted? It would be nice, for example, when you find a Lean proof someone wrote, to be able to see that it's a valid proof, without having to download the file yourself and run it in an instance of Lean.

[Ruben Van de Velde]

For 1, there's a number of projects aiming to formalize various results, from sphere eversion over the prime number theorem to (parts of) Fermat's Last Theorem, as well as projects whose scope are less clear to me like LeanCamCombi and SciLean. Not sure that answers your question. What and who - basically the same answer: the maintainers have to approve incoming code, and incoming code needs maintainers who have at least some interest or expertise to do the reviews

[Ruben Van de Velde]

For 2, does "GitHub" count as an answer? There's also reservoir, but I haven't looked at it

[Alex Altair]

My question is more like, where is the code for those projects going? Presumably a lot of the code developed for FLT (for example) will go into mathlib, but maybe not all of it? And where will that other code live afterwards? Are people planning to keep it "live" (in the sense that that proof will remain valid for the more recent version of Lean/mathlib)?

[Ruben Van de Velde]

Typically, first in an external repository that depends on mathlib (e.g. https://github.com/ImperialCollegeLondon/FLT), and indeed, some of the code is already being moved into mathlib (see https://github.com/leanprover-community/mathlib4/pulls?q=is%3Apr+label%3AFLT). FLT is a bit special here in the sense that the current goal isn't to formalize everything down to the axioms, but to take results from the 1980s and before as given - so anything that depends on those assumptions will stay out of mathlib.

In general these projects stay up to date with mathlib for as long as someone's motivated to keep them up to date :)