How to check whether a notion is already in mathlib?

Stream: new members

[Jakob Scholbach]

I am algebraic geometer making my very first steps with lean. As an "exercise" I wanted to see if I can turn the first page of Matsumura's book into a lean code. So here is another newbie question: how do I find whether a particular concept has already been encoded, say the Zariski topology on the spectrum of a ring? Right now I am clicking through all the .lean files in the algebra folder, but this is surely not the way to find things?

[Johan Commelin]

The easiest way is probably to ask here

[Johan Commelin]

We are working on making it easier to navigate the library. But this is a slow process...
Usually people are happy to give you pointers if you ask here.

[Johan Commelin]

There is a separate library where schemes are defined. It is on several peoples todo list to move that into mathlib. But it needs cleaning up, and everybody is too busy with other things :stuck_out_tongue_wink:

[Johan Commelin]

So atm there is no Zariski topology in mathlib yet

[Johan Commelin]

This is the scheme repo: https://github.com/ramonfmir/lean-scheme

[Kevin Buzzard]

+1 to Johan's first comment. The scheme repo doesn't compile with current mathlib, however Ramon and I are going to fix it up this month (That reminds me to ask my git bisect question).

There are two things you can think about as a beginner with a background in mathematics: (1) can I type [random proof/definition] into Lean (e.g. p1 of Matsumura) and (2) is it there already? In some sense these are different questions. The code written in mathlib is often extremely hard for beginners to follow, it is written in a particular style which computer scientists seem to really like ("golfed term mode") but, crucially, the proofs are not written in such a way that mathematicians can read them. The idea is that most proofs are trivial so you may as well get them over with as quickly as possible. Even the ones which are long are typically written with no comments (I don't know why this is, this is just apparently the style). Of course once you know what's going on you can read the proofs anyway.

[Johan Commelin]

@Jakob Scholbach There are actually other techniques to see if something is there. But they work on the level of a specialized lemma, not on the level of a "big" theory. There is a tactic called library_search. If you state a lemma in Lean, and try to prove it using by library_search then Lean will look through the imported part of the library to see if it can prove your lemma as (a special case of) a lemma in the library. You can also call library_search when you are halfway a proof and believe that you have reduced it to something that is already there. Lean will then tell you the name.
A more general (and slower) tactic is suggest. It will return a list of lemmas that it thinks are applicable to the current goal.

[Kevin Buzzard]

One thing I've found instructive to do with undergraduates is do things like prove sup(S)+sup(T)=sup(S+T), stuff like that. I do this by defining my own sup and then proving all the basic things about it. But it's all already there -- but this doesn't matter to me because I want to show the students how to build a theory rather than just showing them 100 theorems in mathlib and then saying "look, that's all you need to know about sup, now let's move on to tensor products of modules, oh look, here's 100 theorems about them too".

[Scott Morrison]

Even the ones which are long are typically written with no comments (I don't know why this is, this is just apparently the style).

We should change this style.