38
$\begingroup$

There are two online, evolving, collaborative "foundational text" projects for research mathematicians that I am aware of:

(1) The Stacks Project for algebraic geometry

(2) Kerodon for categorical homotopy theory

They are sort of Bourbaki for the internet age. I'd like to know if there are others of the same nature that are ongoing or in the offing.

Please note that I am not looking for texts or monographs available online which is why I have highlighted the adjectives in the first line.

$\endgroup$
8
  • 8
    $\begingroup$ Polymath seems pretty close. By the way, since this is clearly a {big-list} question with no right answer, you probably want to make it Community Wiki, which you do by flagging it for moderator attention. $\endgroup$
    – LSpice
    Commented Aug 22, 2020 at 18:20
  • $\begingroup$ @LSpice: Yes, thanks! How do I flag it? Polymath as I understand it is not for writing foundational research-level texts collaboratively, but for doing research collaboratively. $\endgroup$
    – user164113
    Commented Aug 22, 2020 at 18:51
  • 8
    $\begingroup$ Neither Kerodon nor the Stacks Project is collaborative. Kerodon is written exclusively by Jacob Lurie. The Stacks Project theoretically allows for external submissions, but Johan de Jong wrote 703685 out of 709534 lines in the Stacks Project, i.e., 99.18%. $\endgroup$ Commented Aug 22, 2020 at 19:41
  • 2
    $\begingroup$ @DmitriPavlov: That is interesting and good to know! I was not aware of it. Their "About" sections suggest that they aim to be collaborative, but the reality may well be different. $\endgroup$
    – user164113
    Commented Aug 22, 2020 at 19:47
  • 10
    $\begingroup$ @DmitriPavlov The line count in the repository is not an ideal system, because Johan plays two roles in the Stacks project: editor and (main) author, and either way he will be assigned his name to the line count. stacks.math.columbia.edu/tag/06LB lists major contributions by others, often edited for consistency by Johan, but that doesn't take away that Johan has indeed written the great majority. There are many small contributions by others though. And we are looking into ways to get more external contributions. $\endgroup$
    – pbelmans
    Commented Aug 23, 2020 at 4:42

6 Answers 6

31
$\begingroup$

Mathlib is an online, evolving, collaborative project, aiming to be a foundation for all of modern pure mathematics. It is fully searchable, and here is its homepage. It is hosted on github, and it is all checked with the Lean Theorem Prover.

A great place to see the current state of mathlib is this overview page, which the community keeps up to date.

There are still some parts of undergraduate mathematics not covered by mathlib, but on the other hand there is plenty of advanced mathematics there; for example recent (2020) achievements include a bunch of MSc level commutative algebra (e.g. DVRs), a start on homological algebra, Lie algebras, a bunch of abstract measure theory and Haar measure, manifolds and bundles. My list will go out of date quickly however -- check out the overview page for recent achievements.

Around 100 people have contributed so far, ranging from high school kids to full professors (in particular it is genuinely collaborative); all you have to do is to learn the Lean programming language so you can express mathematics in Lean, and then formalise something that we want in the library. We welcome contributions from many areas of mathematics -- as well as standard UG and MSc material in number theory, geometry, topology, analysis and algebra there is combinatorial game theory, Euclidean geometry and lots of other things. Here is a list of undergraduate-level material which we still do not have.

Three years ago the library had essentially nothing (no complex numbers, no sine and cosine, for example). But it is growing fast and my personal belief is that ultimately it is a more modern way of presenting mathematics than the Stacks Project and Kerodon. Within the next few years, all being well, part of mathlib will be integrating with the Stacks Project; both the mathlib people and the stacks project people are interested in the collaboration, and this recent PR by Scott Morrison (one of the founders of MathOverflow!) is another stepping stone towards schemes; we should have them in mathlib within the next few weeks (they already exist in Lean code but we have learnt the hard way that stuff not in mathlib is liable to bitrot). The reason I think mathlib will ultimately be more important that the Stacks Project or Kerodon is that mathlib is machine-readable, enabling computers to read research-level mathematics. Unfortunately computers still cannot understand natural language, meaning that it is difficult for AI to use e.g. ArXiv to do mathematics at research level, so right now it seems to me that formalisation is a natural way to proceed. I believe that it is inevitable that one day machines will be doing mathematics well, just like it was inevitable that one day they would play chess and go well; indeed one of the reasons I am motivated to work on mathlib is that I want machines to do arithmetic geometry well and this will only happen if professional arithmetic geometers like me explain arithmetic geometry to a computer.

People interested in contributing can take a look at the Zulip chat -- this is a focussed chat room where people use their real names and experts work on questions which have arisen from the formalisation of mathematics. There are sometimes 1000 posts in a day and a lot of the conversation is highly technical, but there is a #new members stream where beginners can ask questions. Please read the community guidelines. In short -- be nice. It's as simple as that.

Mathematicians wishing to learn something about how to contribute might find the Youtube videos from last month's introductory workshop Lean for the curious mathematician interesting. There is also the ongoing book Mathematics in Lean.

$\endgroup$
22
$\begingroup$

I wouldn't say Kerodon is collaborative, but why the $n$Lab isn't in the list?

Personally, I would mention two books:

Kennington's "Differential geometry reconstructed" http://www.geometry.org/tex/conc/dgstats.php the author develops everything in great detail from the start, and by "the start" I mean his personal views on metamathematics, predicate logic, sequent calculus, algebra, analysis, and all the topology you'll ever see/need.

The last release of "Foundations of almost ring theory" https://arxiv.org/abs/math/0409584 where the authors take personally the absence of a comprehensive textbook on 2-category theory.

$\endgroup$
16
  • 1
    $\begingroup$ Speaking of non-collaborative-ness, is either of your references collaborative? $\endgroup$
    – LSpice
    Commented Aug 22, 2020 at 18:23
  • 2
    $\begingroup$ @Fosco: Thanks for the suggestions, but I am only looking for online projects that qualify on all the counts mentioned in the first line of my post, so online textbooks you mention don't come under its purview. There is no dearth of online texts which, of course, are also admirable, valuable and suited to our times. $\endgroup$
    – user164113
    Commented Aug 22, 2020 at 19:05
  • 3
    $\begingroup$ @Fosco: $n$Lab in my view is not a systematic foundational text development enterprise. It seems to be more of an encyclopedia for certain areas of mathematics, although certainly online, evolving, collaborative and aimed at research mathematicians. $\endgroup$
    – user164113
    Commented Aug 22, 2020 at 19:09
  • 7
    $\begingroup$ @DmitriPavlov, "(open-source software) model" means just the model of open-source software (regardless of the actual software used); so an open-source textbook is one in which anyone can see the source (of the text) and, more importantly, can contribute. For example, if I want to add something to the Stacks Project, I can do so easily, via git; but, if I want to add something to a 2-author paper, then both technology and social expectation are against me. The fact that one author did the vast body of the work doesn't, I think, mean it's not collaborative; it just means it's got a leader. $\endgroup$
    – LSpice
    Commented Aug 22, 2020 at 21:12
  • 2
    $\begingroup$ @DmitriPavlov The fact that I technically can download the source code of an arXiv paper and edit it is not so relevant, because if I then share this with another mathematician I will probably have completed some ethical breach like plagiarism or putting words in someone else's mouth. The only way to change the publicly accessible copy is to email the author. Of course if I email them that I found a mistake, they will probably fix it, but this is because of a failure (a mistake). $\endgroup$
    – Will Sawin
    Commented Aug 25, 2020 at 19:28
14
$\begingroup$

An extremely exciting project belonging to this list is Yiannis Sakellaridis's Automorphic Project!

$\endgroup$
3
  • 1
    $\begingroup$ Would you please provide an explicit link to a PDF or to where the book can be read online? $\endgroup$ Commented Aug 24, 2020 at 10:07
  • $\begingroup$ @MusaAl-hassy From what I understand, Sakellaridis is working on setting up a website for the book (http://math.jhu.edu/automorphic/), but (for now) it only works when accessed from the JHU intranet. I think currently the only way to get a PDF is to clone the repo and compile it from the source... $\endgroup$
    – Emily
    Commented Aug 24, 2020 at 22:44
  • 2
    $\begingroup$ @MusaAl-hassy, the website seems to be up now! PDF $\endgroup$
    – Emily
    Commented Oct 27, 2020 at 21:53
8
$\begingroup$

I've released today the Clowder Project, which aims to essentially become a Stacks Project for category theory.

I plan to eventually make it into a comprehensive resource for category theory, in the same way that the Stacks Project is a comprehensive resource for algebraic geometry.

As of writing, it consists of 578 pages, with around 4000 more pages of material on category theory being slowly polished and converted into a form that works with Gerby. There are also 6000 more pages of material on other subjects which might eventually also make their way into it, as they either serve as either illustrating examples or stepping stones.

Here are some links:

  • The website: https://clowderproject.com
  • The GitHub project with the source files: link
  • Everything currently released in PDF form: link
  • The Discord server for the project, for discussions and updates: link
$\endgroup$
3
$\begingroup$

The 1Lab is an online, collaborative reference for univalent mathematics formalised in Cubical Agda.

$\endgroup$
2
$\begingroup$

For number theory, there is this very interesting project similar to the Stacks project that seems to cover in great detail all of the main subfields of modern number theory:

https://github.com/holdenlee/number-theory

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .