publications based on mathlib

Stream: mathlib4

[Emily Riehl]

I'm hoping folks could point me to examples of publications based on mathlib (in either math or CS journals). What I'm specifically curious about was how authors/journals go about archiving whatever version of mathlib corresponded to the formalizations described in the paper. And is it easy for someone who currently has mathlib installed to roll back to a specific version?

(If it matters, let's assume for the purposes of this question that I'm talking about Lean4, though of course publications might have referred to Lean3 formalizations.)

[Eric Wieser]

And is it easy for someone who currently has mathlib installed to roll back to a specific version?

I think considering mathlib to "be [globally] installed" is the wrong way to think about things; more accurate is "a separate copy is installed in each lean project you have downloaded", and the contents of the lake-manifest.json prescribes exactly which copy that should be. So it doesn't matter at all if the version in the paper is different to what you are using in your own projects, as long as the paper authors distribute a full project with lake-manifest.json and lakefile.lean and lean-toolchain.

[Ruben Van de Velde]

Like https://leanprover-community.github.io/papers.html ?

[Eric Wieser]

(there is of course then the question of whether the journal needs to archive those versions of lean / mathlib, or whether they can trust the FRO / mathlib maintainers / github itself to keep all the old links working)

[Emily Riehl]

Ruben Van de Velde said:

Like https://leanprover-community.github.io/papers.html ?

Thanks for pointing me to this great resource!

[Emily Riehl]

Eric Wieser said:

(there is of course then the question of whether the journal needs to archive those versions of lean / mathlib, or whether they can trust the FRO / mathlib maintainers / github itself to keep all the old links working)

This is a good question. What do folks here think?

[Jireh Loreaux]

Unfortunately, I think it's currently unsustainable to expect journals to archive versions of Mathlib, as each one would take at least a gigabyte. I think the standard approach here (both in the Lean community and more generally when authors distribute code in their papers) is to have a public GitHub repo.

[Rob Lewis]

We danced around this question with the AFM without taking it head on. In the end, we ask authors to provide a SWHID for their artifact, but this doesn't enforce anything for dependencies. In the end, with various systems/languages with different architectures, build processes, and development cultures, a one-size-fits-all policy seemed impossible. Authors could provide a docker image with their work and all dependencies but even that isn't totally reliable. NixOS has something to say here, I think, but I don't know enough about it to comment.

[Rob Lewis]

I think the question of whether you can access upstream dependencies is subtly different from whether you can actually use them. There's a decent guarantee right now that given a Lean 3 repo you can find the corresponding mathlib source. Starting up an interactive Lean 3 environment for that repo gets harder by the month.

[Rob Lewis]

Ultimately I decided to try to not let this bother me too much. A runnable artifact (ideally) shouldn't be needed to appreciate the lesson of a paper. Something is lost if you can't open up the project, and something more is lost if you can't even see the dependencies that the project builds on, but hopefully the paper has a message that stands apart from the artifact.

[Rob Lewis]

Ruben Van de Velde said:

Like https://leanprover-community.github.io/papers.html ?

Worth pinging that this is always in need of updates, everyone please add your papers!

[Riccardo Brasca]

Sorry for being self-advertising, but we very recently published a paper in math journal using a reasonably nice solution by @Adam Topaz

[Kevin Buzzard]

If you add your paper to that website then it advertises for you :-) I was going to ping Dagur and point out that it wasn't there yet :-)

[Riccardo Brasca]

I just opened the PR :)

[Jireh Loreaux]

Riccardo Brasca said:

using a reasonably nice solution by @Adam Topaz

what is this solution exactly?

[Kim Morrison]

Riccardo Brasca said:

I just opened the PR :)

@Riccardo Brasca, you have a typo in the title of the paper. It is "categorical", not "categorial" (I've seen this typo previously, so I'm guessing it is a common multilingual problem. :-)

[Rob Lewis]

Also I merged your PR too fast -- the bib entry is missing a tags field, which means it won't show up on the list of papers :whoops:

[Riccardo Brasca]

Sorry, I will fix it.

[Riccardo Brasca]

mmm, something went wrong in merging https://github.com/leanprover-community/leanprover-community.github.io/pull/570 but I am not sure what

[Ruben Van de Velde]

ValueError: Couldn't find a url for bib item ABKNT_2024

[Ruben Van de Velde]

Every entry that has tags seems to need a link, url, or eprint field

[Ruben Van de Velde]

https://github.com/leanprover-community/leanprover-community.github.io/pull/571 makes CI catch the issue before merging

[Martin Dvořák]

In my last paper, I wrote it as follows.
image.png
In addition to that (and perhaps more importantly), there is a link to my repo, which specifies version of all dependencies.