What areas of matlib need contributions?

Stream: new members

[Martin C. Martin]

I'd like to contribute to matlib. What's the best area for a new member? For example, is everything in a first and second year of undergraduate education covered, or are there some gaps that would be good to fill?

[Eric Rodriguez]

this is some of the undergraduate stuff not in mathlib: https://leanprover-community.github.io/undergrad_todo.html

[Martin C. Martin]

Thanks! How up to date is that page? For example, under "Single Variable Real Analysis," it mentions Convergence of real valued-series. There seems to be a lot of stuff under analysis/ and order/ involving tendsto. What specifically is still missing from mathlib, and what files should I look in for contributing?

[Eric Rodriguez]

I mean, what are you interested in? I'll have to defer on why that's there, as far as I know the page is kept reasonably up-to-date

[Martin C. Martin]

Well, I'd be happy to contribute anything covered by Spivak's Calculus, for example.

[Martin C. Martin]

I haven't read Baby Rudin, but I'd consider read and contributing anything from that too.

[Kevin Buzzard]

Comparison of an infinite sum and an integral should be doable right now. The only reason convergence of real-valued series isn't there is that we have absolute convergence which turns out to be the important notion.

[Martin C. Martin]

Thanks. So what's a good thing for me to contribute, and where in matlib should I start looking?

[Eric Wieser]

Martin C. Martin said:

Thanks! How up to date is that page?

That page should be very up-to-date, as usually the entries are added at the same time as the feature, as both live in the source code

[Eric Wieser]

A less up to date, but more explanatory reference is https://github.com/leanprover-community/mathlib/wiki/Undergrad-low-hanging-fruits

[Eric Wieser]

(and the two harder lists linked from there)

[Martin C. Martin]

That seems very concrete! convergent_series seems like a great place to start. A related question: how do I find the definition of a term in Lean? For example, lots of files seem to use tendsto, but in VSCode using "go to definition" just says it can't find the definition.

[Johan Commelin]

That's weird. That ought to work.

[Johan Commelin]

Is your Lean extension in VScode up to date?

[Johan Commelin]

As an annoying work around, you can use the online docs, see e.g. docs#tendsto

[Jireh Loreaux]

docs#filter.tendsto

[Martin C. Martin]

It might be a RAM issue, I have an 8GB laptop and lean was taking 10+GB. Anyway, thanks for the work around

[Eric Rodriguez]

do you get mathlib caches?

[Martin C. Martin]

Not sure, I just did a checkout from git. Would that include the caches?

[Eric Rodriguez]

no! you'll want to get leanproject, not sure where the insturctions are

[Eric Wieser]

Johan Commelin said:

Is your Lean extension in VScode up to date?

There was a one-day window where I broke "goto definition" in a bad way; it's possible you ended up with this broken version somehow

[Martin C. Martin]

I tried renaming my matlib folder out of the way, then leanproject get mathlib. Now lean is only taking 459 MB, and not much CPU! When I want to update, how should I do it? I did git pull --rebase in my matlib folder earlier today, is that a mistake?

[Martin C. Martin]

"Go to definition" is still not working for me. Specifically, line 93 of order/liminf_limsup.lean:
lemma not_is_bounded_under_of_tendsto_at_top [preorder β] [no_max_order β] {f : α → β} {l : filter α} [l.ne_bot] (hf : tendsto f l at_top) : ¬ is_bounded_under (≤) l f :=
I still get "No definition found for tendsto". Do I need to do anything special to configure VSCode, or just point it at the directory? The Lean extension was last updated 5/20.

[Eric Rodriguez]

I think that's the right lean extension version! And for updating, you can use leanproject pull, this will get you the precompiled files which make things much faster :)

[Eric Rodriguez]

I sadly can't reproduce with this issue on that exact line, just pointing it at the repository should work :/ try restart VSCode + Lean one more time?

[Martin C. Martin]

Every time I start it, it says "Folder contains a Dev Container configuration file. Reopen folder to develop in a container." Do I need to do that?

[Kevin Buzzard]

Your installation sounds totally borked. Are you trying to install Lean 3 or Lean 4? If Lean 3, did you carefully follow the instructions on the community website?

[Martin C. Martin]

Yes, and it worked a few months ago when I last tried it. I'll try a re-install.

[Kevin Buzzard]

The two issues we see in practice are (1) people don't have the right oleans (compiled lean files) for mathlib (fixed with leanproject get-mathlib-cache) and (2) people aren't opening a lean project in VS Code (a lean project is a directory formatted in a certain way with a leanpkg.toml file and you need to open it with the "open folder" functionality of VS Code). But I've never seen your error before! If you continue to have problems then maybe send a screenshot of your VS Code.

[Alex J. Best]

The dev container message isn't an error, it's just an option that you likely want to ignore.

[Patrick Massot]

Martin C. Martin said:

Thanks! How up to date is that page? For example, under "Single Variable Real Analysis," it mentions Convergence of real valued-series. There seems to be a lot of stuff under analysis/ and order/ involving tendsto. What specifically is still missing from mathlib, and what files should I look in for contributing?

This has been discussed many times. A rather recent instance is at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/New.20to.20lean.2Fmathlib.2E.20Trying.20to.20understand.20the.20library.2E What is missing is mostly an entry point for people interested in undergrad teaching. You could create a file series.lean somewhere in the analysis folder and add definitions like

open finset filter
open_locale big_operators topological_space


def tendsto_series {M : Type*} [topological_space M] [add_comm_monoid M] (u : ℕ → M) (m : M) :=
tendsto (λ n, ∑ k in range n, u k) at_top (𝓝 m)

def cvgt_series {M : Type*} [topological_space M] [add_comm_monoid M] (u : ℕ → M) :=
∃ m, tendsto_series u m

and then search mathlib for all lemmas that could be restated in that file. Presumably that file would stay a leaf file, not really used by other files.

[Patrick Massot]

There are clearly things in analysis.specific_limits

[Patrick Massot]

Working on this would be a very nice way to learn how topology and analysis are handled in mathlib

[Patrick Massot]

See also #13179 that was merged recently

[Kevin Buzzard]

How about we put a link on the mathlib todo page to Patrick's Zulip mesage above? And similarly a link to a similar message about special linear groups. That would not be the usual style of that page but it might help us having to answer the same question again and again.