Undergraduate math list

Stream: general

[Patrick Massot]

One the website we have a mathlib overview. Among the problems of this list are:

• It is outdated and needs constant maintaince (spoiler: I won't propose a magic fix, we only need to care more about this list)
• It doesn't tell where are all those things, and we all know that navigating mathlib is difficult
• It doesn't point out missing things, and we have many people who want to start contributing, preferably easy things

Of course the list of missing things is open-ended. But we have a well-known half-specified milestone: covering all of undergraduate mathematics. So we could list missing undergraduate stuff, either in the main list (printed in red) or in a separate list.

[Patrick Massot]

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

[Patrick Massot]

group:
  basic definitions:
    group: 'https://github.com/leanprover-community/lean/blob/master/library/init/algebra/group.lean#L35'
    group morphism: 'https://leanprover-community.github.io/mathlib_docs/algebra/group/hom.html'
    direct product of groups: 'https://leanprover-community.github.io/mathlib_docs/algebra/group/prod.html'
    subgroup: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html'
    subgroup generated by a subset: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#group.closure'
    order of an element: 'https://leanprover-community.github.io/mathlib_docs/group_theory/order_of_element.html'
    normal subgroup: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#normal_subgroup'
    quotient group: 'https://leanprover-community.github.io/mathlib_docs/group_theory/quotient_group.html#quotient_group.group'
    group action: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action'
    stabilizer of a point: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.stabilizer'
    orbit: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.orbit'
    quotient space: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.orbit_equiv_quotient_stabilizer'
    class formula: ''
    conjugacy classes: ''
  abelian group:
    cyclic group: ''
    finite type abelian groups: ''
    complex roots of unity: ''
    primitive complex roots of unity: ''
  permutation group:
    permutation group of a type: 'https://leanprover-community.github.io/mathlib_docs/data/equiv/basic.html#equiv.perm'
    decomposition into transpositions: ''
    decomposition into cycles with disjoint support: ''
    signature: 'https://leanprover-community.github.io/mathlib_docs/group_theory/perm/sign.html#equiv.perm.sign'
    alternating group: ''
  classical automorphim groups:
    general linear group: 'https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.general_linear_group'
    special linear group: 'https://leanprover-community.github.io/mathlib_docs/linear_algebra/special_linear_group.html'
    orthogonal group: ''
    special orthogonal group: ''
    unitary group: ''
    special unitary group: ''
  representation theory for finite groups:
    representations of abelian groups: ''
    Maschke theorem: ''
    orthogonality of irreducible characters: ''
    Fourier transform for finite abelian groups: ''
    convolution: ''
    examples for groups with a small cardinal: ''

[Rob Lewis]

I've always kind of hated the mathlib overview page (and the theories pages) because they so trivially go out of date. This looks like a step forward at least. With a fixed list of what should be there, it's easier to see when it needs to be updated.

[Rob Lewis]

But really, we need someone to take charge of this list and promise to keep it updated.

[Patrick Massot]

I think the existence of a fixed list would make it much easier. And people keep asking for projects to work on.

[Yury G. Kudryashov]

Some links point to the source code, some point to docs website. Is there any specific reason?

[Patrick Massot]

If I didn't mess up, only the core lib stuff points to code, because it has no doc.

[Yury G. Kudryashov]

https://leanprover-community.github.io/mathlib_docs/core/init/algebra/group.html

[Patrick Massot]

So you can start fixing my list. I'm sure I've also missed stuff that we already have.

[Patrick Massot]

I pushed my file to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml. It isn't used for anything yet, but everybody can already fix things there.

[Patrick Massot]

Let's make it a test. We have one obvious suboptimal link, and a least a couple of holes that are either already here or trivial to fill. Let's see if we can get contributions there. If yes then I'll translate all the other sections.

[Patrick Massot]

I should also point out that one advantage of this list with precise pointers to the doc (preferably specific items rather that whole pages when it makes sense) is that we can have CI hunting for broken links at every commit. So that page would become outdated only because of additions to mathlib, not because of refactors.

[Johan Commelin]

@Patrick Massot I think this is a very good idea. I'll try my best to contribute, and keep contributing.

[Yury G. Kudryashov]

Should I push or PR?

[Yury G. Kudryashov]

I'd strip the common prefix from all URLs.

[Bryan Gin-ge Chen]

I'd say push unless there's something you want to discuss or have reviewed.

[Johan Commelin]

I think the broken link detector is a must btw.

[Yury G. Kudryashov]

I fixed some URLs and translated 1.1.

[Bryan Gin-ge Chen]

Should we have space for some notes in the YAML in addition to just URLs, in case mathlib's treatment of those topics deserves additional explanation?

[Johan Commelin]

Sounds good. And isn't YAML flexible enough to just drop those notes in?
So you write

  'cyclic_group' : blablaURL
-- or
  'cyclic_group':
    - URL: blablaURL
    - note: '''some note'''

and the script can just figure out which of the two was used?
(Me doesn't know yaml too well.)

[Yury G. Kudryashov]

BTW, why do we need YAML, and not markdown with predictable structure?

[Bryan Gin-ge Chen]

I guess Patrick is thinking of parsing the YAML in Python and building pages from some templates somehow.

[Yury G. Kudryashov]

OK, let's have a YaML file

[Yury G. Kudryashov]

BTW, do we have an undergraduate student speaking French?

[Yury G. Kudryashov]

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

[Yury G. Kudryashov]

(i.e., he could use this time for something else that an undergraduate can't do)

[Yury G. Kudryashov]

Or I can translate in a comment, and let a student turn it into a list with links.

[Patrick Massot]

Yury G. Kudryashov said:

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

To be honest I feel I'm overqualified to write format_lean, leancrawler and leanproject, and rewriting the whole website infrastructure. One difference here is an undergrad may actually learn stuff about math and mathlib, so maybe I should dare suggest that @Ryan Lahfa would be perfect for this job.

[Patrick Massot]

Bryan Gin-ge Chen said:

Should we have space for some notes in the YAML in addition to just URLs, in case mathlib's treatment of those topics deserves additional explanation?

How would you like them to be displayed in the end? Actually I don't like this idea. I think this information should be in either in the module docstrings or in the theories folder if it needs to be really long.

[Ryan Lahfa]

Patrick Massot said:

Yury G. Kudryashov said:

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

To be honest I feel I'm overqualified to write format_lean, leancrawler and leanproject, and rewriting the whole website infrastructure. One difference here is an undergrad may actually learn stuff about math and mathlib, so maybe I should dare suggest that Ryan Lahfa would be perfect for this job.

I definitely can

[Ryan Lahfa]

Though, I don't really enjoy writing YAML and prefer TOML nowadays but that is a taste matter (and endless nights fighting with Ansible…)

[ROCKY KAMEN-RUBIO]

I'm happy to help with French->English translation. You just want 2020 version of the national exam topics linked in the original post right?

[Patrick Massot]

I don't care at all about YaML vs toml, especially if I'm not the one doing the translation. But I have a hard time thinking how the format could be simpler than what I wrote in https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

[Patrick Massot]

It's great that both of you want to help here. Please coordinate to avoid duplicating efforts. You can either translate without caring about what's in mathlib or do both at the same time (but please don't cheat like Johan was tempted to.

[Ryan Lahfa]

Patrick Massot said:

I don't care at all about YaML vs toml, especially if I'm not the one doing the translation. But I have a hard time thinking how the format could be simpler than what I wrote in https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

Indeed

[Ryan Lahfa]

Do we agree that real analysis should be in that overview list?

[Ryan Lahfa]

Like "Heine theorem", "continuity", etc.

[Johan Commelin]

I think the plan is to put everything from http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf into the YAML file. And then present it as a challenge to mathlib users to make sure that every item has a corresponding entry in mathlib.

[Johan Commelin]

To prevent the cheating, it might be easier to do a "dumb" translation first, without adding links to mathlib.

[Patrick Massot]

Ryan Lahfa said:

Like "Heine theorem", "continuity", etc.

This is all on pages 4 and 5.

[Ryan Lahfa]

Patrick Massot said:

Ryan Lahfa said:

Like "Heine theorem", "continuity", etc.

This is all on pages 4 and 5.

Okay, perfect ; it's clear now in my head

[Ryan Lahfa]

@ROCKY KAMEN-RUBIO What we can do is, I can let you backfill the current English version for links (if there's any), while I rewrite the overview_fr.yaml with french text and copy the current links over, and then, I add as much stuff as I can from the France teaching program, then you can translate it to the English version and get the links I found
We can do some iterations of this algorithm which is somewhat guaranteed to finish in few PRs

[Ryan Lahfa]

Quick question, @Patrick Massot @Yury G. Kudryashov wouldn't we want something like real internationalisation in the future? With something like https://weblate.org/ (they provide free instances for open source) and it's able to do automatic commits for i18n, with various review mechanisms

[Patrick Massot]

What would you want to translate? Here the goal is not to have both a French and and English version

[Johan Commelin]

I personally wouldn't worry about it too much.

[Patrick Massot]

It's simply that the convenient data set I was able to find happens to be in French

[Ryan Lahfa]

Patrick Massot said:

What would you want to translate? Here the goal is not to have both a French and and English version

Ah — Okay, it's a French → English translation only, I thought there was a goal to have a overview_fr.yaml, my apologies

[Johan Commelin]

We just want a long list that is a "certified and stamped" list of things that appear in an undergrad curriculum. And then pointers to mathlib.

[Ryan Lahfa]

Sorry for the confusion, okay, I'm writing it now then

[Patrick Massot]

I can see Ryan totally entered translator mode. He'll have a lot of fun once https://github.com/mpedramfar/Lean-game-maker/pull/12 will be merged. He'll be able to continue the work stated in https://github.com/ImperialCollegeLondon/natural_number_game/pull/83

[ROCKY KAMEN-RUBIO]

Ryan Lahfa said:

ROCKY KAMEN-RUBIO We can split the work in:
— I give you page 5 and later
— I take page < 5

Sounds good! Should we setup a shared doc to have consistent formatting?

[Patrick Massot]

@ROCKY KAMEN-RUBIO and @Ryan Lahfa, are you making any progress here?

[ROCKY KAMEN-RUBIO]

I have a draft I'll post shortly. Just tidying up some formatting

[Ryan Lahfa]

Patrick Massot said:

ROCKY KAMEN-RUBIO and Ryan Lahfa, are you making any progress here?

I have written some, I planned to get a working part of this today/tonight ; do you prefer small PR/improvements or rather a large PR implementing everything for this kind of changes?

[Jalex Stark]

the sooner you post any work, the less duplication of effort there will be, and the faster other people can make small contributions

[Johan Commelin]

Yup, nothing wrong with 37 small PRs!

[ROCKY KAMEN-RUBIO]

Here's my (still somewhat rough) draft
Aggregation_2020.pdf

[ROCKY KAMEN-RUBIO]

I'm still working on some of the grittier formatting. Let me know if anything is conceptually incorrect, or if you have any other suggestions.

[Jalex Stark]

? working hard on formatting a pdf seems wrong, since the final goal will be markdown that lives somewhere in the mathlib docs or the leanprover community website
(more to the point : post source code!)

[Bryan Gin-ge Chen]

Even better: I suggest opening a PR at the website repo which makes additions / edits to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

[Bryan Gin-ge Chen]

Patrick Massot said:

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

See this part of the first message in this thread.

[ROCKY KAMEN-RUBIO]

Jalex Stark said:

? working hard on formatting a pdf seems wrong, since the final goal will be markdown that lives somewhere in the mathlib docs or the leanprover community website
(more to the point : post source code!)

I guess by "grittier formatting" I meant things on the level of "clarifying that this is an exponent". I'll post my source code

[ROCKY KAMEN-RUBIO]

Aggregation_2020.tex

[ROCKY KAMEN-RUBIO]

Bryan Gin-ge Chen said:

Patrick Massot said:

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

See this part of the first message in this thread.

Oh I see, don't know how I missed that. I can start putting this into the .yaml file too.

[ROCKY KAMEN-RUBIO]

Ok I added the definitions from sections 5 and on as a PR. I think there are redundancies, and some definitions that could be organized better, but it's a start.
https://github.com/leanprover-community/leanprover-community.github.io/compare/newsite...iceplant:patch-1

[Bryan Gin-ge Chen]

Great! Do you mind opening a PR? It will be easier for us to make comments and suggestions on it that way.

[ROCKY KAMEN-RUBIO]

Bryan Gin-ge Chen said:

Great! Do you mind opening a PR? It will be easier for us to make comments and suggestions on it that way.

I thought I opened a PR but apparently I am still a git noob and only branched. I just opened a PR for real.

[Bryan Gin-ge Chen]

Thank you! Here's the PR link for those who don't happen to be watching the repo: https://github.com/leanprover-community/leanprover-community.github.io/pull/26

[ROCKY KAMEN-RUBIO]

I'm trying to expand links to the real analysis section since I just finished @Patrick's tutorial, but I'm noticing many of the definitions are in an auxiliary file he wrote (like the definition of a convergent sequence) and I'm having trouble finding them in mathlib. Is that because they just don't exist there yet, or am I not looking in the right place?

[Jalex Stark]

if I go to the mathlib docs site and search for "cauchy sequence", i get useful results
https://leanprover-community.github.io/mathlib_docs/

[Jalex Stark]

probably the biggest barrier for you personally contributing here is in "know the words a mathematician might say"

[Patrick Massot]

Rocky, everything which features in the tutorial is in mathlib except for stuff used in the very last file that I haven't found time to PR. However what is in mathlib can be very hard to recognize if you know only about the elementary theory. But other people can fill this. Are you done with the translation?

[Patrick Massot]

And there is no point in trying to put links to mathlib before you resolve all the issues at https://github.com/leanprover-community/leanprover-community.github.io/pull/26

[Yury G. Kudryashov]

Many definitions and theorems about limits in mathlib are formulated in a very general form (e.g. using filters, uniformity structure, or metric_spaces).

[ROCKY KAMEN-RUBIO]

Yury G. Kudryashov said:

Many definitions and theorems about limits in mathlib are formulated in a very general form (e.g. using filters, uniformity structure, or metric_spaces).

That that explains a lot. I'll leave that section to others who understand this better then. Any suggestions on how to better understand these ideas? I'm familiar with filters in Haskell but haven't used them in Lean.

Patrick Massot said:

Rocky, everything which features in the tutorial is in mathlib except for stuff used in the very last file that I haven't found time to PR. However what is in mathlib can be very hard to recognize if you know only about the elementary theory. But other people can fill this. Are you done with the translation?

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

[Patrick Stevens]

Filters are defined in order.filter.basic - they're not the same thing as List.filter : (a -> bool) -> List a -> List a. A filter on a set U is a way of defining what it means for a subset of U to be "large and not small" in whatever sense you need "large" to mean, satisfying by definition certain "large" properties. Namely: U is itself large; a superset of a large set is large; and if you intersect two large sets then you still have a large set (that is what I meant by "not small"). It turns out to be possible to define analysis using filters on the naturals; this is closely linked to Robinson's rather lovely formulation of nonstandard analysis, but it's all very much not how you're initially taught to think about analysis, so don't expect the path to understanding to be quick. I had a quick skim of https://arxiv.org/pdf/1212.5740.pdf and it seemed reasonable

[Bryan Gin-ge Chen]

@Kevin Buzzard has a blogpost on filters here.

[Patrick Massot]

@Patrick Stevens The use of filters in mathlib has nothing to do with non-standard analysis. I think it is very unfortunate that filters can be used in non-standard analysis, since this gives a bad reputation to filters, whereas filters were nice and useful long before this application.

[Jalex Stark]

Some of my friends said that looking at a proof of tychonoff's theorem with filters and one without filters was the key to getting them onto the filter train

[Jalex Stark]

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

[ROCKY KAMEN-RUBIO]

Jalex Stark said:

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

I believe I resolved all the issues that were raised (to the best of my abilities, Ryan brought up some nuance in terminology that I'm not super familiar with). Is that not showing up?

[Ryan Lahfa]

ROCKY KAMEN-RUBIO said:

Jalex Stark said:

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

I believe I resolved all the issues that were raised (to the best of my abilities, Ryan brought up some nuance in terminology that I'm not super familiar with). Is that not showing up?

Let me check

[Ryan Lahfa]

AFAIK, our comments are still there

[Ryan Lahfa]

Some of them are nuance in terminology, but others are just little typos (Euler for instance)

[Patrick Massot]

Rocky, if you don't see the "Outdated" label in yellow as in
image.png
then you probably didn't fix an issue. Once an issue is fixed, there are two options: if you are sure you fixed it, then click the "Resolve conversation" button. Otherwise post a comment saying you tried to fix it but you're not sure

[Patrick Massot]

The picture shows both the oudated label and the "Resolve conversation" button

[ROCKY KAMEN-RUBIO]

I closed most of the issues. @Ryan Lahfa I responded to your two comments that I didn't resolve.

[Ryan Lahfa]

@ROCKY KAMEN-RUBIO Answered to the 2nd comment, the 1st one can be fixed in the next PR

[Ryan Lahfa]

@Bryan Gin-ge Chen Let us know if you like the new PR, so that I can start adding stuff on the top of it

[Bryan Gin-ge Chen]

@ROCKY KAMEN-RUBIO Thanks for all the fixes! @Ryan Lahfa I'll merge it now to let you work on it.

[Ryan Lahfa]

Appreciate it!

[Ryan Lahfa]

So the first thing is this:
https://github.com/leanprover-community/leanprover-community.github.io/pull/27
I'll do a parallel PR for backfilling links wherever I can

[Ryan Lahfa]

Then, maybe we can get feedback from the people in this feed at the same time on capitalization/unicode/should include LaTeX or not/etc of some points.

[Ryan Lahfa]

https://github.com/leanprover-community/leanprover-community.github.io/pull/28

[Ryan Lahfa]

https://github.com/leanprover-community/leanprover-community.github.io/pull/33 here's a PR to generate the overview page
@Bryan Gin-ge Chen @Johan Commelin I might be looking for your feedback if you will :pray:

[Ryan Lahfa]

I rebased https://github.com/leanprover-community/leanprover-community.github.io/pull/28 and we can merge it if we want, I think getting as much links as possible even in small increments/PRs seems a good strategy

[Bryan Gin-ge Chen]

At a first glance the overview page PR looks pretty good. It looks like there's still some discussion occurring around the links. I don't want to merge before getting @Patrick Massot's opinion though.

[Johan Commelin]

Looks good to me! Thanks for all the effort!

[Patrick Massot]

Thanks a lot @Ryan Lahfa . This is not yet what I had in mind, but we are getting closer. I just let a review.

[Patrick Massot]

PS: Ryan, using / in a git branch name is a really bad idea. It interfere with remote/branch syntax

[Patrick Massot]

I merged this PR anyway because we really need people to be able to contribute to the yaml file, and the layout PR also had yaml syntactic fixes (mixing both in the same PR was also not the greatest idea).

[Patrick Massot]

But now I cannot merge https://github.com/leanprover-community/leanprover-community.github.io/pull/28 because of conflicts. @Ryan Lahfa could you fix that really soon? I don't want to steal your commit authorship by fixing things on my side.

[Patrick Massot]

I don't remember whether I wrote this publicly. But I would really really like this list to be ready to be seen on Wednesday. The reason is that I've been asked to give a propaganda talk at IAS on Wednesday.

[Patrick Massot]

So it would be really nice for the community if we could have a overview.yaml spring filling as many links as possible. You don't even need to know any git. You can simply hit the edit button (small pen in the top right corner) to propose new links.

[Ryan Lahfa]

Patrick Massot said:

But now I cannot merge https://github.com/leanprover-community/leanprover-community.github.io/pull/28 because of conflicts. Ryan Lahfa could you fix that really soon? I don't want to steal your commit authorship by fixing things on my side.

Yes, I'll do it

[Ryan Lahfa]

Patrick Massot said:

PS: Ryan, using / in a git branch name is a really bad idea. It interfere with remote/branch syntax

AFAIK, it should not, I have been using it for ≥ 5 years, it just works fine to do remote/xxx/yyy, have you a precise example in mind?

[Patrick Massot]

It prevents you to skip the remote part when you want to use the default remote

[Ryan Lahfa]

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

[Ryan Lahfa]

I answered to some of the comments on the overview generation PR

[Ryan Lahfa]

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

[Patrick Stevens]

It's also annoying in general for anyone who wants to do programmatic manipulation of git branches - there's nothing to prevent you naming a branch refs/heads/branchname if you want, but it similarly forces the tool-writer to get their manipulations exactly right. If the user had just not put any slashes in, the problem would be so simple, you could just split on the / character no matter what style of ref you were given

[Patrick Stevens]

(I have strong opinions on this - if / were simply a disallowed character in branch names, the whole system would be so much less complex)

[Ryan Lahfa]

Patrick Stevens said:

It's also annoying in general for anyone who wants to do programmatic manipulation of git branches - there's nothing to prevent you naming a branch refs/heads/branchname if you want, but it similarly forces the tool-writer to get their manipulations exactly right. If the user had just not put any slashes in, the problem would be so simple, you could just split on the / character no matter what style of ref you were given

But anyway, as it is possible, that sounds like sane to me for tool authors to not rely on this kind of behavior and perform exact manipulation, as they would have all the "information"

[Ryan Lahfa]

Patrick Stevens said:

(I have strong opinions on this - if / were simply a disallowed character in branch names, the whole system would be so much less complex)

I don't have a good visual image of how complex the system is due to this, I don't know enough git internals

[Ryan Lahfa]

I'll fix it in my further PRs/branches :)

[Patrick Massot]

Ryan Lahfa said:

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

image.png

[Patrick Massot]

Ryan Lahfa said:

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

I mean git fetch

[Ryan Lahfa]

Patrick Massot said:

Ryan Lahfa said:

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

image.png

My GitHub UI seems to be outdated/stuck, I'll rebase it again to ensure everything is fine

[Ryan Lahfa]

Done

[Ryan Lahfa]

Patrick Massot said:

Ryan Lahfa said:

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

I mean git fetch

Okay, that's a fair point :-)

[Patrick Massot]

Thanks for rebasing. I merged it. So now everybody can contribute to filling more links.

[Ryan Lahfa]

Also, @Patrick Massot @Bryan Gin-ge Chen wonder if I could get commit access to the repository (w/o master or newsite for example), that'd make a simpler workflow for some PRs which might be edited on the top (e.g. links backfilling)

[Patrick Massot]

Could you try to use some TeX in this yaml file? Mathjax is loaded on all pages of the website. So if the yaml parser doesn't get confused then it should work. And if it does get confused then maybe enclosing stuff in quote would be good enough to unconfuse it.

[Ryan Lahfa]

@Patrick Massot I was definitely going to try this

[Ryan Lahfa]

I can replace the Unicode math by some LaTeX

[Ryan Lahfa]

The result might be ugly though, like if you do inline math in respect to the line height (?), but I'm no expert, we'll see and I'll post about it

[Patrick Massot]

I see that real numbers don't even have a unicode mathbb.

[Ryan Lahfa]

:-)

[Ryan Lahfa]

That's an easy fix s/R/$\mathbb{R}$/g

[Patrick Massot]

About the repo access, I'd be happy to give you write access to branches that are not master or newsite, but I'm not sure this wouldn't mess up CI (if I need to protect branches or something), so I'll let Bryan handle that.

[Ryan Lahfa]

Patrick Massot said:

About the repo access, I'd be happy to give you write access to branches that are not master or newsite, but I'm not sure this wouldn't mess up CI (if I need to protect branches or something), so I'll let Bryan handle that.

Sure thing

[Ryan Lahfa]

@Patrick Massot Also, should we just use complex.xxx for the link syntax

[Ryan Lahfa]

And use mathlib_docs/find/{{ decl }}

[Ryan Lahfa]

Sounds like an easy way to fill links, e.g. https://leanprover-community.github.io/mathlib_docs/find/complex.exists_root for complex.exists_root

[Ryan Lahfa]

(I mean rather the module.statement syntax rather than the folder1/folder2/module.html#statement or whatever)

[Patrick Massot]

The advantage of the current format is you can fill in items while browsing the doc website and copy-pasting partial links

[Patrick Massot]

And also a dot separated format looks like Lean namespacing and we don't have any convenient way to access the fully qualified name of a declaration while staring at the file containing it.

[Ryan Lahfa]

isn't it just whatever the statement of a declaration we're looking at?

[Ryan Lahfa]

@Rob Lewis ^

[Ryan Lahfa]

But alright, I was just finding the process of browsing/copying a bit slow for massive link injection

[Ryan Lahfa]

But that's the computer scientist in me who is talking, pay no heed

[Scott Morrison]

The problem when looking at a declaration is that it can be hard to work out what namespace you're currently in (because so many mathlib files are so long). You can insert a #where to discover the namespace, but this will cause recompilation headaches if you're jumping between many files.

[Ryan Lahfa]

Okay, that's not very usable for browsing docs → injecting them in the YAML file, thanks for the clarification

[Rob Lewis]

Yes, the /find/ page just takes a (complete) identifier. Notice that the docs always print a complete identifier, so if you look at (randomly) docs#std.prec.max_plus you can copy std.prec.max_plus directly. It's trickier to find this browsing the Lean source, but you can keep a file with import all open and just use tab complete.

[Rob Lewis]

It's easy enough to expose the declaration name -> location map from the doc generator if this is useful.

[Rob Lewis]

The benefit to using this over hardcoded links, of course, is that if a declaration is moved to a new file the links won't break. Even more important if you're linking to lines in the source, which are very likely to break. src#std.prec.max_plus will stay up to date.

[Ryan Lahfa]

Maybe what we can do now is to use hardcoded links, then we can do an automatic pass to rewrite them properly using the complete identifier, so we can hit the deadline of the IAS for @Patrick Massot

[Ryan Lahfa]

But decl name → location map would be useful I guess, I don't know if it has to be exposed in the HTML or as a JSON/YAML machine-consumable

[Rob Lewis]

Your links already contain the complete identifier, right? I see things like algebra/pi_instances.html#prod.module. Everything after the # is the complete identifier.

[Rob Lewis]

Ryan Lahfa said:

But decl name → location map would be useful I guess, I don't know if it has to be exposed in the HTML or as a JSON/YAML machine-consumable

It wouldn't change the HTML at all, would just host a file leanprover-community.github.io/mathlib_docs/name_to_loc.json.

[Rob Lewis]

So if the website generator needed this info it could just grab the map there.

[Rob Lewis]

It could include more info too, e.g. the type of the declaration. I think this would be particularly nice for the 100 theorems list, to print the statement on the main page.

[Ryan Lahfa]

Rob Lewis said:

Your links already contain the complete identifier, right? I see things like algebra/pi_instances.html#prod.module. Everything after the # is the complete identifier.

Well, this was something I grabbed from the doc link, so I didn't know if it was complete or not

[Ryan Lahfa]

Sounds good @Rob Lewis — I'll see what I can do, but maybe after IAS to make it cooler

[Mario Carneiro]

Scott Morrison said:

The problem when looking at a declaration is that it can be hard to work out what namespace you're currently in (because so many mathlib files are so long). You can insert a #where to discover the namespace, but this will cause recompilation headaches if you're jumping between many files.

Earlier, someone (Kevin?) suggested that we could have theorem declarations be hoverable same as theorem uses. If the hover contained the full namespaced name, wouldn't that solve the problem?

[Patrick Massot]

Yes

[Johan Commelin]

Can someone (@Patrick Massot @Ryan Lahfa ?) tell me how complete the .yaml now is?
Is it just a matter of filling in the links, or are there also still new sections that need to be added to the .yaml?

[Patrick Massot]

Filling the links would be awesome

[Patrick Massot]

We don't plan to add sections soon. At some point we'll probably want to add more advanced sections, maybe in another file.

[Johan Commelin]

Which years does this cover? Is this like 1st and 2nd year of French math education?

[Johan Commelin]

How should I interpret this file?

[Johan Commelin]

Can we add
http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf
to the top of the file, in a comment?

[Johan Commelin]

Is this file already rendered somewhere on a public facing website?

[Patrick Massot]

There is a semi-hidden temporary rendering at https://leanprover-community.github.io/overview.html, but really you should ignore that and just fill in

[Johan Commelin]

What is the correct link for complementary subspaces: https://leanprover-community.github.io/mathlib_docs/linear_algebra/projection.html ? Do we have a statement that says that you can choose such a subspace? (@Yury G. Kudryashov)

[Patrick Massot]

Hmm, https://leanprover-community.github.io/mathlib_docs/order/bounded_lattice.html#is_compl might be a bit too abstract...

[Johan Commelin]

Exactly

[Patrick Massot]

It's still useful information that this is how it's said in mathlib. And we can always add more context in https://leanprover-community.github.io/theories/linear_algebra.html

[Yury G. Kudryashov]

Do we allow multiple links per item?

[Yury G. Kudryashov]

https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#submodule.exists_is_compl states that a complementary subspace exists.

[Yury G. Kudryashov]

See also https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/complemented.html for Banach space version (closed complementary subspaces).

[Patrick Massot]

There is no issue putting several links per item in the yaml file, but that would be hard to render if we want to keep it compact (where each listed item is a link to something).

[Johan Commelin]

We still don't have Cayley–Hamilton

[Johan Commelin]

We could link to the first item, and append little link markers for the further links

[Patrick Massot]

Yes, this is one of the goal of this list: highlighting glaring holes (although this is not how I intend to use it on Wednesday...).

[Johan Commelin]

https://github.com/leanprover-community/leanprover-community.github.io/pull/36 is what I've found for section 1.

[Yury G. Kudryashov]

Should we show formalized and not yet formalized items on different pages?

[Patrick Massot]

Yes, I think they should be on different pages

[Johan Commelin]

Maybe just an option at the top

[Johan Commelin]

Where you can toggle what you want to see.

[Johan Commelin]

With a bit of CSS classes that should be trivial

[Patrick Massot]

True, but we also want to browse the TODO list, without seeing what is done

[Johan Commelin]

That's what I'm saying, right?

[Johan Commelin]

Two radio buttons should be able to provide that.

[Johan Commelin]

Done: on/off     TODO: on/off

[Patrick Massot]

Oh ok, right. Feel free to implement, or hope Ryan will do it.

[Patrick Massot]

Johan Commelin said:

https://github.com/leanprover-community/leanprover-community.github.io/pull/36 is what I've found for section 1.

Merged, thanks!

[Ryan Lahfa]

Johan Commelin said:

Done: on/off     TODO: on/off

Sounds good

[Ryan Lahfa]

I'm doing it now

[Johan Commelin]

Coprime elements: we have coprime ideals (ideal.is_coprime) but not specifically coprime elements. To do or not to do?

[Ryan Lahfa]

I guess it's "alright"

[Johan Commelin]

@Patrick Massot Does the "boss" have an opinion? :wink:

[Yury G. Kudryashov]

ideal.is_coprime is a definition of coprime elements that uses ideals.

[Johan Commelin]

Ooh, that's an ugly name in that case

[Johan Commelin]

Divisibility in commutative integral rings what does this mean? What's an integral ring?

[Kevin Buzzard]

I guess for a general ring one can make sense of coprimality of two elements by just asking $(a)+(b)=R$, but then $X$ and $Y$ would not be coprime in $\mathbb{C}[X,Y]$.

[Johan Commelin]

What the hack is a Rupture fields:?

[Kevin Buzzard]

splitting field?

[Johan Commelin]

Nope, that's the next item

[Johan Commelin]

https://github.com/leanprover-community/leanprover-community.github.io/pull/37 here's a bunch of links for section 3 (@Patrick Massot)

[Chris Hughes]

It's just the field when you adjoin one root, but not necessarily all of them

[Johan Commelin]

So we have that, right?

[Chris Hughes]

Yes

[Alex J. Best]

https://fr.wikipedia.org/wiki/Corps_de_rupture

[Johan Commelin]

Derived polynomials: # Should this be "Polynomial derivative"? @Ryan Lahfa

[Ryan Lahfa]

@Johan Commelin Yes, it's really $P'$ when $P$ is a polynomial IIRC

[Ryan Lahfa]

as a formal polynomial

[Reid Barton]

https://en.wikipedia.org/wiki/Rupture_field

[Ryan Lahfa]

I was going to link it :D

[Reid Barton]

I definitely assumed this was a mistranslation

[Ryan Lahfa]

I double checked those because it looked fishy to me but Wikipedia proved me wrong

[Johan Commelin]

TIL

[Ryan Lahfa]

But really, sometimes, in France, there seems to be many structures which are not "directly" available in English

[Ryan Lahfa]

Also, our convergence is not the good one :-°

[Ryan Lahfa]

We call a limit, something which is rather limit by different values $\lim_{x \to a \atop x \neq a} f(x)$ (for example)

[Ryan Lahfa]

But it does not matter

[Johan Commelin]

I've pushed those two fixes

[Ryan Lahfa]

I have the desired feature

[Ryan Lahfa]

Will push it

[Johan Commelin]

Ryan Lahfa said:

I have the desired feature

You mean the radio buttons?

[Ryan Lahfa]

Yes

[Ryan Lahfa]

https://github.com/leanprover-community/leanprover-community.github.io/pull/38

[Ryan Lahfa]

Awesome PRs @Johan Commelin

[Ryan Lahfa]

We should try to use LaTeX for titles

[Ryan Lahfa]

Like "something something $\Q[X]$ something" if we have the macro for, or just $\mathbb{Q}$

[Ryan Lahfa]

Screen-Capture_select-area_20200530170650.png

[Ryan Lahfa]

LaTeX is working just fine

[Ryan Lahfa]

Will do a PR to add some examples

[Ryan Lahfa]

of course, we don't have the macro \Q

[Ryan Lahfa]

should we add some macros to our MathJax setup?

[Johan Commelin]

You could add some common macros to the top of the rendered page.

[Ryan Lahfa]

Alright, I'll do it

[Ryan Lahfa]

Shouldn't I do this in templates/_base.html ?

[Johan Commelin]

Je ne sais pas

[Ryan Lahfa]

I'll try locally, if it works fine, I'll let as-is and @Patrick Massot will do the ultimate call

[Ryan Lahfa]

:D

[Ryan Lahfa]

Does not work, so I'll put it in the base

[Patrick Massot]

I'm sorry I was away. Are there still things to discuss, or did you settle everything?

[Ryan Lahfa]

https://github.com/leanprover-community/leanprover-community.github.io/pull/39

[Ryan Lahfa]

@Patrick Massot You can take a look to 39 & 38 and see if it's okay for you

[Patrick Massot]

I think we can add a couple of LaTeX macros in _base.html.

[Ryan Lahfa]

39 implements the LaTeX macros in _base

[Ryan Lahfa]

I didn't go too far, I just added R, Q, Z, C, N

[Ryan Lahfa]

We could add GL, L, class{n} (continuity classes), S(R^d), etc. Depends.

[Johan Commelin]

@Patrick Massot By now, my PR should be uncontroversial.

[Johan Commelin]

I think GL, SL, etc are fine. But I wouldn't go overboard with the macros.

[Ryan Lahfa]

I do mathrm{GL}, etc. for them

[Ryan Lahfa]

You can see it in 39

[Johan Commelin]

Maybe the rule of three applies? If you need it more then 3 times, a macro should be fine.

[Ryan Lahfa]

GL(n, R), GL(n, C)…

[Patrick Massot]

Are those 3 PRs compatible?

[Ryan Lahfa]

O(n, 2), O(n, 3)…

[Ryan Lahfa]

@Patrick Massot Please merge Johan's ones first

[Ryan Lahfa]

Then I'll do the rebase magic for whatever happens

[Ryan Lahfa]

I'm pretty sure there are no to very few conflicts

[Ryan Lahfa]

(we're close to have everything in rings, wow!)

[Johan Commelin]

@Patrick Massot One second

[Johan Commelin]

Ryan spotted an issue in my PR

[Ryan Lahfa]

@Johan Commelin it's not that important, I'm fixing it in my PR

[Ryan Lahfa]

If you don't do it, that'll just break newsite temporarily (before merging mine)

[Johan Commelin]

@Patrick Massot Ok, you can merge now

[Patrick Massot]

I reviewed Johan's PR

[Patrick Massot]

But I could merge it since my comments are only about empty items

[Ryan Lahfa]

Nevermind my comments

[Ryan Lahfa]

Yes, I think we can merge it

[Johan Commelin]

Also, I need to go now

[Patrick Massot]

Thanks Johan, I merged it.

[Ryan Lahfa]

Fixing the conflicts

[Ryan Lahfa]

Conflicts resolved, @Patrick Massot

[Ryan Lahfa]

I'll experiment for the "show inline elements for the last depth level"

[Patrick Massot]

Great!

[Ryan Lahfa]

@Patrick Massot style question, should we do titlecase for every title?

[Patrick Massot]

I merged the switch one and this created conflict in the macro one

[Ryan Lahfa]

I'll fix the macro one

[Patrick Massot]

About titlecase, let's do whatever is convenient in the yaml, and we can add a jinja filter if we want to change it on the website

[Ryan Lahfa]

At the make_site phase, we can just give title.titlecase() if we want, it was really just should we do it or not?

[Patrick Massot]

The title of the page should change too. I think we can use "Undergraduate mathematics in mathlib".

[Ryan Lahfa]

https://github.com/leanprover-community/leanprover-community.github.io/pull/40 for deepest level

[Ryan Lahfa]

@Patrick Massot conflicts resolved on the latex one

[Ryan Lahfa]

"Done undergraduate mathematics in Lean"
:-)

screencapture-leanprover-community-github-io-overview-html-2020-05-30-17_42_06.png

[Patrick Massot]

We try to checkout your PR 40 it doesn't seem to work

[Patrick Massot]

Does it work on your end?

[Ryan Lahfa]

Patrick Massot said:

We try to checkout your PR 40 it doesn't seem to work

Maybe I misunderstood what do you mean by inline elements, is it like the latest nodes are not accordion, right?

[Ryan Lahfa]

(Remaining undergrad maths)
screencapture-leanprover-community-github-io-overview-html-2020-05-30-17_43_22-2.png screencapture-leanprover-community-github-io-overview-html-2020-05-30-17_43_22.png

[Patrick Massot]

I want the deepest level to be a single paragraph, with words separated by commas. As in the original document

[Patrick Massot]

On your screenshot, everything under "Bilinear" would be on the same line

[Ryan Lahfa]

Oh okay, makes sense, and all "mathematical statements" would be <a /> to the docs, right?

[Patrick Massot]

And there would be no "See it in mathlib documentation" anywhere. Instead of use card containing

vector space
See it in mathlib documentation

and a huge card linear map..., there would be

vector space, linear map...

[Ryan Lahfa]

I see

[Ryan Lahfa]

I'm doing it

[Ryan Lahfa]

I should have the prototype in minutes

[Patrick Massot]

Thank you very much

[Ryan Lahfa]

@Patrick Massot Just a quick question

[Patrick Massot]

Yes?

[Ryan Lahfa]

What do you do about

xxx:
    yyy: …
    zzz: …
    ttt:
        aaa: …
   uuu: …

[Ryan Lahfa]

do you show in the xxx card:
yyy, zzz
then the ttt accordion
then uuu?

[Patrick Massot]

We probably need to simplify the nesting. I think there should be only two levels of accordions.

[Ryan Lahfa]

Agreed

[Patrick Massot]

Do you have a specific example?

[Ryan Lahfa]

Take linear algebra

[Ryan Lahfa]

Linear algebra:
  vector space: 'algebra/module.html#vector_space'
  linear map: 'algebra/module.html#linear_map'
  product of vector spaces: 'algebra/pi_instances.html#prod.module'
  vector subspace: 'algebra/module.html#subspace'
  range of a linear map: 'linear_algebra/basic.html#linear_map.range'
  kernel of a linear map: 'linear_algebra/basic.html#linear_map.ker'
  quotient space: 'linear_algebra/basic.html#submodule.quotient'
  sum of subspaces: 'linear_algebra/basic.html#submodule.complete_lattice'
  direct sum: ''
  complement subspace: ''
  linear independent: 'linear_algebra/basis.html#linear_independent'
  generating sets: ''
  bases: ''
  algebra of endomorphisms of a vector space: ''
  general linear group: 'linear_algebra/basic.html#linear_map.general_linear_group'
  invariant subspace of an endomorphism: ''
  eigenvalue: ''
  eigenvector: ''
  linear representation: ''
  irreducible representation: ''
  finite dimensional representations:
    examples: ''
    Schur's lemma: ''
  finite-dimensional vector spaces:
    finite-dimensional vector spaces: 'linear_algebra/finite_dimensional.html#finite_dimensional'
    existence of bases: 'linear_algebra/basis.html#exists_is_basis'
    canonical isomorphism with K^n: 'linear_algebra/basis.html#module_equiv_finsupp'
    complementary subspaces: 'linear_algebra/basis.html#submodule.exists_is_compl'
    rank of a linear map: ''
    rank of a set of vectors: ''
    dual vector space: 'linear_algebra/dual.html#module.dual'
    rank of a system of linear equations: ''
    transpose of a linear map: ''
    dual basis: 'linear_algebra/dual.html#is_basis.dual_basis'
    bidual: 'linear_algebra/dual.html#vector_space.eval_equiv'
    orthogonality: ''
  multilinear:
    multilinear map: 'linear_algebra/multilinear.html#multilinear_map'
    determinant of vectors: ''
    determinant of endomorphisms: ''
    special linear group: ''
    orientation of a R-valued vector space: ''
  matrices:
    commutative ring valued matrices: 'data/matrix/basic.html#matrix'
    field valued matrices: 'data/matrix/basic.html#matrix'
    elementary operations on matrices' rows: ''
    elementary operations on matrices' columns: ''
    determinant: 'linear_algebra/determinant.html#matrix.det'
    invertibility: 'linear_algebra/nonsingular_inverse.html#matrix.nonsing_inv'
    rank of a matrix: ''
    matrix representation of a linear map: 'linear_algebra/matrix.html#linear_map.to_matrix'
    coordinates change: ''
    Gauss' pivot: ''
    row-reduced matrices: ''
  endomorphism invariant subspaces: ''
  kernel lemma: ''
  characteristic polynomial: ''
  endomorphism polynomials: ''
  cancelling polynomials: ''
  minimal polynomial: ''
  Cayley-Hamilton theorem: ''

[Ryan Lahfa]

necessarily, I need a way to determine when to stop the inline display for leaves

[Ryan Lahfa]

I think I can work out some prototype but just want to warn about the strange result it might give

[Patrick Massot]

Here I think we are actually missing nesting. The issue is that some stuff is dumped at level 2 but should be level 3 (ie leaves).

[Ryan Lahfa]

I think too, I didn't work on the organization and wanted to get something out ASAP

[Patrick Massot]

The end is clearly missing a heading, something like 'endomorphism polynomials'

[Ryan Lahfa]

Anyway, I'll implement the following solution:
When I encounter a leaf, I just show it inline with <a /> and add a , if I'm not the last node of the current iterator (doable in Jinja magic)
When I encounter an internal node, I create an accordion
That should work

[Ryan Lahfa]

Patrick Massot said:

The end is clearly missing a heading, something like 'endomorphism polynomials'

We already have endomorphism polynomials, but you have this annoying issue
If you do a heading
Then you have to repeat it in order to link to the concept

[Ryan Lahfa]

Like, endomorphism polynomials have a lot of things around, but are themselves a specific kind of polynomials… I don't know how to solve "this"

[Patrick Massot]

I don't think this is a big issue

[Ryan Lahfa]

Okay

[Patrick Massot]

You can let people with more math experience going over the yaml file to sort this out

[Ryan Lahfa]

screencapture-localhost-8000-overview-html-2020-05-30-17_59_00.png

[Ryan Lahfa]

@Patrick Massot Yes, definitely, I don't want to fight this :) — I'm still too green

[Ryan Lahfa]

Here's a prototype

[Ryan Lahfa]

Do you want I do something before I commit this?

[Patrick Massot]

I think it looks much better. But there is still the issue that inner card should extend horizontally to match outer ones

[Ryan Lahfa]

Screen-Capture_select-area_20200530180156.png
do you mean something like this ?

[Ryan Lahfa]

because all cards applied padding on their stuff, so when I nest them, obviously…

[Ryan Lahfa]

but I don't think that's a bad thing per se, that gives space and looks not that bad on mobile AFAIK

[Ryan Lahfa]

we can reduce padding in the inner cards I guess

[Patrick Massot]

No, I mean no space at all on sides of inner cards.

[Patrick Massot]

Also I'd prefer to keep a white background. It looks weird to have this all grey background only on this webpage of the website

[Ryan Lahfa]

Okay for bg color

[Ryan Lahfa]

For the space, I'll try something, you'll let me know, worst case, you can edit the PR or guide me again

[Ryan Lahfa]

Should have something in 10 minutes hopefully

[Patrick Massot]

Also, I'm not the only one deciding stuff here. If everybody likes those margins I'll have them.

[Ryan Lahfa]

Then we should ping them for their advice, @Bryan Gin-ge Chen @Rob Lewis @Kevin Buzzard @Yury G. Kudryashov @Mario Carneiro @Scott Morrison

[Patrick Massot]

You should have waited to get a prototype incorporating everything (including switches and updated page title)

[Ryan Lahfa]

Why?

[Patrick Massot]

Because this way they don't have to read all messages, they can look at the result

[Patrick Massot]

Those are busy people

[Ryan Lahfa]

You're right

[Ryan Lahfa]

Apologies

[Patrick Massot]

Don't worry

[Ryan Lahfa]

It's now online on the inline branch, @Patrick Massot

[Ryan Lahfa]

It is also rebased over newsite, I'll just verify & repull just in case

[Kevin Buzzard]

Did somebody call?

[Kevin Buzzard]

I am just having a break from marking, what should I look at?

[Kevin Buzzard]

Only 80 algebraic geometry questions to go :D

[Ryan Lahfa]

I'm getting full page screenshots, if you don't want to do make_site on the branch

[Ryan Lahfa]

In the order: complete (todo & done), done, todo
screencapture-file-home-raito-dev-projects-Lean-leanprover-community-github-io-build-overview-html-2020-05-30-18_26_24.png screencapture-file-home-raito-dev-projects-Lean-leanprover-community-github-io-build-overview-html-2020-05-30-18_26_15.png screencapture-file-home-raito-dev-projects-Lean-leanprover-community-github-io-build-overview-html-2020-05-30-18_25_46.png

[Ryan Lahfa]

Let us know what you think of the design and what would you want to see

[Ryan Lahfa]

https://github.com/leanprover-community/leanprover-community.github.io/pull/40

[Patrick Massot]

There is something funny going on with "Affine and Euclidian Geoemtry (finite dimensional only)" (besides the typo and the restriction)

[Ryan Lahfa]

The PR is there for the ones who want to try it live

[Ryan Lahfa]

@Patrick Massot YAML stuff most likely

[Ryan Lahfa]

Can fix it in a future PR

[Patrick Massot]

I'd like the accordion to be folded when you open the page, so that people can navigate quickly. And also the todo switch should be off by default, so that people first get the information about what is there and where.

[Patrick Massot]

And I still don't like the horizontal margins :stuck_out_tongue:

[Patrick Massot]

But otherwise it really starts looking like what I dreamed of.

[Ryan Lahfa]

Patrick Massot said:

I'd like the accordion to be folded when you open the page, so that people can navigate quickly. And also the todo switch should be off by default, so that people first get the information about what is there and where.

• Default switch to off is easy for TODO
• Folded accordions is easy too

Can add them, right now, should I go for it?

[Ryan Lahfa]

Patrick Massot said:

And I still don't like the horizontal margins :stuck_out_tongue:

I will have to wait the vote from the people

[Patrick Massot]

yes, please

[Mario Carneiro]

those screenshots are massive and zulip doesn't let me zoom in easily. could you show a representative sample?

[Patrick Massot]

You'll have more votes when I'll merge the PR and we'll see it live

[Ryan Lahfa]

@Mario Carneiro You can load them in your browser or enable pan & zoom to review them easily

[Ryan Lahfa]

But yes, let's merge the PR @Patrick Massot

[Patrick Massot]

when I click on them it zooms

[Ryan Lahfa]

Let me just get the latest changes you want

[Patrick Massot]

Did you fixed the two defaults?

[Patrick Massot]

Yes, let's do that

[Ryan Lahfa]

I'm doing it, only one left

[Mario Carneiro]

with pan & zoom the frame doesn't change shape so I'm peering through a very slim vertical window

[Mario Carneiro]

zulip's implementation really needs work

[Patrick Massot]

Mario, you should hold on for 5 minutes

[Ryan Lahfa]

Just open the link in the browser

[Mario Carneiro]

what is being reviewed?

[Mario Carneiro]

the margins?

[Ryan Lahfa]

@Mario Carneiro the looks mostly

[Mario Carneiro]

the spacing is all over the place

[Mario Carneiro]

there is 0px spacing between cards but significant (20px?) margins on left and right and at the bottom of a group

[Ryan Lahfa]

here we go for the defaults

[Mario Carneiro]

also there is no spacing after the text and before the cards

[Ryan Lahfa]

+1 @ spacing pre/post cards

[Ryan Lahfa]

the indentation "spacing" is by default

[Mario Carneiro]

What's wrong with a simple bullet list?

[Ryan Lahfa]

it's not an accordion (?)

[Ryan Lahfa]

you can fold/unfold those cards

[Ryan Lahfa]

@Patrick Massot wants to remove horizontal space on cards I think (if I understood well, I won't speak in its place)

[Mario Carneiro]

I'm not sure why this particular list is getting web-designed

[Patrick Massot]

I don't understand why it doesn't look like https://getbootstrap.com/docs/4.4/components/collapse/#accordion-example

[Mario Carneiro]

I would have just chucked some markdown on a page

[Patrick Massot]

Mario, this list is too big to be unfolded by default

[Ryan Lahfa]

@Patrick Massot I can take a look why

[Ryan Lahfa]

It might be a class missing

[Mario Carneiro]

I've seen mile long bullet lists before

[Patrick Massot]

Mario didn't need CSS in metamath...

[Ryan Lahfa]

Screen-Capture_select-area_20200530183933.png

[Ryan Lahfa]

that was it

[Ryan Lahfa]

but it broke the toggle button

[Patrick Massot]

I still think the inner list should extend horizontally to fill the container (and there should be no leaf next to them, but this is a yaml content issue)

[Mario Carneiro]

Patrick Massot said:

Mario didn't need CSS in metamath...

Interesting that you mention that, just this week we had a conversation about upgrading our HTML validator and the new one yells at us for using <FONT> tags

[Ryan Lahfa]

@Patrick Massot I pushed the fix for accordions

[Ryan Lahfa]

The thing now is that due to this kind of styling

[Ryan Lahfa]

When I hide todo sections, Bootstrap cannot put the border-bottom, because it's in display: hidden and the selector is like "apply the bottom border on the last element in the DOM"

[Ryan Lahfa]

I'm not sure I see easy workarounds

[Ryan Lahfa]

I'll have to manually force-style the previous element in the section, I'm not sure

[Ryan Lahfa]

Anyway, if we can get this PR merged, we can get more improvements later, @Patrick Massot is this okay with you?

[Ryan Lahfa]

:tada:

[Patrick Massot]

Yes, I think this will help people discussing it. Everybody will be able to play with it. Hopefully this will also increase motivation for working on the yaml file.

[Patrick Massot]

Everybody, we are discussing https://leanprover-community.github.io/overview.html

[Patrick Massot]

This is currently live but without any link pointing towards it.

[Ryan Lahfa]

this bottomless stuff is making me crazy

[Ryan Lahfa]

Oops @Patrick Massot

[Ryan Lahfa]

I'll fix it…

[Patrick Massot]

No

[Patrick Massot]

Don't fix it

[Patrick Massot]

It's not ready for links

[Kevin Buzzard]

https://mathlib_docs/algebra/char_p.html#frobenius isn't a valid URL

[Patrick Massot]

I very carefully checked there was no link to it

[Kevin Buzzard]

Why does Fields have fields as a subthing?

[Patrick Massot]

We need at least one pass over the whole yaml file before linking to this webpage

[Ryan Lahfa]

I meant the fact that mathlib_docs are not pointing correctly is a bug

[Kevin Buzzard]

Does "todo" mean "we need to add a link" or "we need to formalise this"?

[Ryan Lahfa]

@Kevin Buzzard It means both currently

[Patrick Massot]

It currently means either of these

[Patrick Massot]

Fields has fields as a subthing because the big one should read "Field theory"

[Ryan Lahfa]

@Patrick Massot https://github.com/leanprover-community/leanprover-community.github.io/pull/41

[Kevin Buzzard]

So "Distributions on Rd" is not LaTeX'ed up, presumably you know this

[Ryan Lahfa]

It'll fix the mathlib links

[Ryan Lahfa]

@Kevin Buzzard Yes, LaTeX-ification is open to improvements :-)

[Patrick Massot]

Kevin, it wouldn't take more time to fix it on github than to write it here

[Kevin Buzzard]

but of course in general it's a really nice resource.

[Kevin Buzzard]

Yeah but I need to go

[Patrick Massot]

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

[Johan Commelin]

There are commas at the and of the lists. Is that intended?

[Ryan Lahfa]

Unfortunately

[Ryan Lahfa]

When the next element is hidden

[Ryan Lahfa]

I don't do adjustements to make the comma disappear

[Kevin Buzzard]

\"Usual\" functions in single variable real analysis

[Johan Commelin]

Ok

[Patrick Massot]

If this is all too painful we can still make a different webpage with the todoes

[Ryan Lahfa]

Kevin Buzzard said:

\"Usual\" functions in single variable real analysis

That's an easy fix, \ should be dropped in the YAML, it can be edited online

[Kevin Buzzard]

I will take a very good look at this on Tues when my deadlines are over

[Kevin Buzzard]

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

[Ryan Lahfa]

Patrick Massot said:

If this is all too painful we can still make a different webpage with the todoes

I don't think that'd be hard, but it just require that I think about the problem seriously and not implement workarounds on the top of workarounds

[Johan Commelin]

We could add "Expand all / Collapse all"

[Ryan Lahfa]

Johan Commelin said:

We could add "Expand all / Collapse all"

That's easy to do

[Johan Commelin]

Kevin Buzzard said:

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

Yup, but that list was ad hoc. This one has an official "stamp" from French education...

[Ryan Lahfa]

Can add it but not right now, I'm hungry

[Ryan Lahfa]

Johan Commelin said:

Kevin Buzzard said:

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

Yup, but that list was ad hoc. This one has an official "stamp" from French education...

And ours has links !

[Kevin Buzzard]

Is it somehow possible to make that mathlib-overview page have the same format I wonder? Do we even want that though, or is the simpler formatting of the overview page better perhaps?

[Kevin Buzzard]

For the overview page there is no particular "goal" -- here we have a very well-defined and, in my opinion, extremely exciting, goal.

[Johan Commelin]

I think that eventually the two lists should be merged

[Johan Commelin]

And we could generate different pages from the same source .yaml file

[Ryan Lahfa]

Definitely possible

[Kevin Buzzard]

Is it possible to add (not right now, but at some point) more stuff? For example at Imperial they learn Jordan Canonical Form

[Ryan Lahfa]

It might be already there implicitly as the french name of "reduction techniques"

[Ryan Lahfa]

I don't recall if Jordan is part of agrég

[Kevin Buzzard]

I am 100% sure there will one random thing on our curriculum which is not on this list, that's what I'm saying basically

[Patrick Massot]

Sure, all this is possible. We can add a page with more advanced stuff, or add more sections

[Kevin Buzzard]

or on Cambridge's curriculum or whatever

[Ryan Lahfa]

FWIW, https://laurent.claessens-donadello.eu/pdf/lefrido.pdf should represent a decent part of the agrég

[Patrick Massot]

I'm pretty sure Jordan is there somewhere, maybe implicitly

[Ryan Lahfa]

But it's French

[Johan Commelin]

I think the next step would be to add tags in the list:

Linear Algebra:
  Matrices:
    Inverse:
      link: 'link/to/docs.html#inverse'
      tag: [agreg, icl]

[Ryan Lahfa]

Jordan is 9.13

[Kevin Buzzard]

OK I'm going back to the treadmill. It looks really nice. I don't really have a feeling for what it will look like on Wednesday when it's complete, but hopefully it looks respectable.

[Ryan Lahfa]

we have it Screen-Capture_select-area_20200530185822.png

[Ryan Lahfa]

Johan Commelin said:

I think the next step would be to add tags in the list:

Linear Algebra:
  Matrices:
    Inverse:
      link: 'link/to/docs.html#inverse'
      tag: [agreg, icl]

it requires just minor adjustement in the Python code, but we can very much support it

[Patrick Massot]

No Johan, the next step is to finish the first pass on the yaml linkifying

[Ryan Lahfa]

:DDDDDD

[Johan Commelin]

Ok, sure. I meant the next next step

[Johan Commelin]

Like, after your IAS talk

[Patrick Massot]

Ok, I'll have a go at Section 6: Single variable real analysis.

[Bryan Gin-ge Chen]

@Ryan Lahfa I've given you write access to the repo. Also, the CI now builds all branches (except master and oldsite), and deploys only happen for newsite.

[Patrick Massot]

Oh crap, the very first item I picked is hard. Topology on R...

[Patrick Massot]

R gets its topology as a uniform space

[Yury G. Kudryashov]

Metric space?

[Patrick Massot]

Yes

[Patrick Massot]

I linked to real.metric_space

[Patrick Massot]

Oh we still have underlined links in the API docs :sad:

[Patrick Massot]

Another tricky one: cluster point of a sequence. Of course we have that as a special case of filter stuff, but do we have a specific definition? If not then I'll let this blank

[Bryan Gin-ge Chen]

The underlined links will hopefully be addressed by doc-gen#20. @Ryan Lahfa, are you still around? :smile:

[Patrick Massot]

I think he's having dinner.

[Patrick Massot]

But I don't understand how a young nerd can have dinner away from his keyboard.

[Ryan Lahfa]

Patrick Massot said:

But I don't understand how a young nerd can have dinner away from his keyboard.

That's because my kitchen is not yet integrated!

[Ryan Lahfa]

Bryan Gin-ge Chen said:

The underlined links will hopefully be addressed by doc-gen#20. Ryan Lahfa, are you still around? :smile:

I'm around, I still need to do something which is good for everyone :D

[Ryan Lahfa]

I can try to move it forward today

[Ryan Lahfa]

By curiosity, do we even have distributions in Lean?

[Patrick Massot]

Distributions in the sense of Schwartz?

[Patrick Massot]

We don't.

[Patrick Massot]

@Sebastien Gouezel or @Yury G. Kudryashov do you know whether we have the description of connected subsets of R? The closest I can find is https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#is_preconnected_iff_forall_Icc_subset

[Yury G. Kudryashov]

We don't. We have is_preconnected_iff_forall_Icc_subset and is_preconnected_I??.

[Yury G. Kudryashov]

How would you formulate real.is_(pre)connected_iff to make it useful?

[Patrick Massot]

I think we could at least say connected iff convex

[Patrick Massot]

Do you know whether we have convergent numerical series. I know about has_sum, but this is a stronger notion. I know we can state "partial sums converge", but do we actually have a def?

[Patrick Massot]

It's dinner time. See you later

[Yury G. Kudryashov]

has_sum uses tendsto (λ n, ∑ i in range n, a i) at_top (nhds s).

[Yury G. Kudryashov]

is_preconnected_iff_convex is is_preconnected_iff_forall_Icc_subset.trans convex_real_iff.symm (no, one of them has x≤y)

[Patrick Massot]

There are two different has_sum then

[Patrick Massot]

Where is yours?

[Yury G. Kudryashov]

Sorry, I meant that the file about has_sum uses this tendsto when talking about normal series convergence.

[Yury G. Kudryashov]

I should read my messages before sending them.

[Patrick Massot]

Yes there are things like https://leanprover-community.github.io/mathlib_docs/topology/algebra/infinite_sum.html#has_sum_iff_tendsto_nat_of_summable

[Patrick Massot]

But we still miss a def here

[Paul van Wamelen]

How do I help edit this on github? (without submitting a PR from a fork?)

[Patrick Massot]

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

[Patrick Massot]

Do you see the little pen button on the top-right corner?

[Patrick Massot]

(I'm asking because I admin rights on this repo, so I'm not 100% sure what is visible by everybody)

[Patrick Massot]

Please don't edit Section 6 before I say I'm done with it, otherwise we may duplicate efforts.

[Paul van Wamelen]

I see the pen, but because I don't have write permissions it will still create a fork, But I guess that is fine. Can I help with just the styling and some of the English? Top level titles should be all capitals (except for articles and short conjuctions). Next level should at least start with a capital. Others all lower case?

[Paul van Wamelen]

I don't see where to edit this, but want to mention: "This page tracks usual mathematical theories that are or not are in mathlib currently" should be "This page tracks usual mathematical theories that are or are not in mathlib currently"

[Patrick Massot]

Sorry I misunderstood. Technically it does create a fork, but nothing happens on your hard-drive.

[Patrick Massot]

The answer to your second question is: https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/overview.html

[Patrick Massot]

Fixes to the English and styling are welcome of course

[Paul van Wamelen]

Did a VERY small PR just to see how it works...

[Patrick Massot]

Merged!

[Patrick Massot]

I need reviewers for https://github.com/leanprover-community/leanprover-community.github.io/pull/44, especially @Sebastien Gouezel In this PR I also discuss my general ideas about how to work on these links.

[Patrick Massot]

I should add that this PR took me a lot more time that I anticipated, but I also learned stuff about mathlib (some items were good surprises whose existence in mathlib was unknown to me).

[Sebastien Gouezel]

I am not sure I can see where the threshold is to say we have something. For instance, we don't have a definition of absolutely converging series, but we have the theorem

lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
summable_of_norm_bounded _ hf (assume i, le_refl _)

And I don't think we should (ever) define absolutely converging series, since it is just summable (λa, ∥f a∥), and the interesting bit is the above theorem. Does this mean that we will never consider this item as done in mathlib?

[Patrick Massot]

As I wrote in the PR, there will always be borderline case. If we think something will never be added then it's a good indication something is wrong. We should then either reformulate the line (or even remove it in extreme cases) or link to something close. In this case, I would agree with you if we had converging series instead of summable families.

[Patrick Massot]

I mean I would fill this item with a version of this lemma involving converging series

[Sebastien Gouezel]

But this lemma is stronger than the version for converging series, with

lemma has_sum.tendsto_sum_nat {f : ℕ → α} (h : has_sum f a) :
  tendsto (λn:ℕ, ∑ i in range n, f i) at_top (𝓝 a)

(in infinite_sum.lean). To me, it only highlights the fact that this curriculum is not optimized for higher-level applications, not a deficiency in mathlib.

[Patrick Massot]

Don't you think we should still have a predicate saying that a series converge? And then people will look for the weaker statement (although its proof will use the stronger one)

[Sebastien Gouezel]

You mean, give a name to the fact that the partial sums tend to to some limit? I don't really have an opinion on this: it wouldn't hurt but it wouldn't be very useful either, except to say that we have all undergrad maths.

[Kevin Buzzard]

Alternatively we could just not fuss and point to something like summable_of_summable_norm and leave it to people to figure out what we mean.

[Kevin Buzzard]

One could similarly argue that we'll never have group homomorphisms because we only have monoid homomorphisms

[Patrick Massot]

Sure, we can use this link, but the question of converging series still stansd

[Sebastien Gouezel]

Same question for positive series. We have a good deal on ennreal and nnreal-valued series in topology/instances/ennreal.lean (notably that an ennreal-valued series always has a sum, that an nnreal-valued one converges if and only if the sum of the ennreal-valued coe is not infinite, and consequences for real-valued series whose terms are all nonnegative. What more could you add?

[Patrick Massot]

Of course for positive series there is nothing to add, they converge only when they are summable

[Patrick Massot]

Does anyone know the English translation of "Réduction des endomorphismes"?

[Johan Commelin]

Context? Analysis?

[Patrick Massot]

It's the grab bag where you put the study of eigenvalues, eigenvectors, trigonalization, Jordan normal form etc.

[Patrick Massot]

Also, given a matrix A, how would you call a polynomial P such that P(A) = 0?

[Patrick Massot]

The yaml file calls it a cancelling polynomial but it sounds fishy to me

[Bryan Gin-ge Chen]

I learned it as the characteristic polynomial.

[Johan Commelin]

I don't know of a name for such polynomials... but knowing that the minimal polynomial divides them is the only interesting property that they have, right?

[Alex J. Best]

Patrick Massot said:

Also, given a matrix A, how would you call a polynomial P such that P(A) = 0?

You mean any polynomial with that property? We have minimal polynomial for the smallest one and characteristic for det(x-A) but otherwise no name for this.

[Patrick Massot]

Yes any polynomial

[Bryan Gin-ge Chen]

Right, I misread. I agree with Alex.

[Patrick Massot]

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

[Patrick Massot]

What about "Réduction des endomorphismes"?

[Patrick Massot]

Does anyone has a translation?

[Patrick Massot]

I need a header for the following list:

    eigenvalue: ''
    eigenvector: ''
    diagonalization: ''
    trigonalization: ''
    endomorphism invariant subspaces: ''
    characteristic subspaces: ''
    kernel lemma: ''
    Dunford decomposition: ''
    Jordan normal form: ''

[Bryan Gin-ge Chen]

Patrick Massot said:

What about "Réduction des endomorphismes"?

Finite-dimensional spectral theory?

[Patrick Massot]

By the way, the translation "kernel lemma" also sounds fishy

[Alex J. Best]

Patrick Massot said:

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

If I had to make one up annihilating polynomial sounds more natural.

[Johan Commelin]

Patrick Massot said:

By the way, the translation "kernel lemma" also sounds fishy

What does it mean?

[Alex J. Best]

Hmm it seems this term is used https://www.maths.ed.ac.uk/~tl/minimal.pdf

[Patrick Massot]

https://fr.wikipedia.org/wiki/Lemme_des_noyaux

[Johan Commelin]

Nope... the only other place on earth where such a lemma exists is in Catalan...

[Patrick Massot]

annihilating polynomial is the direct translation of the French name, I like it

[Patrick Massot]

Seriously, Johan, didn't you study linear algebra?

[Johan Commelin]

Not really... actually. I skipped all the lectures.

[Bryan Gin-ge Chen]

Hmm, a comment on this math stackexchange page suggests "primary decomposition": https://math.stackexchange.com/questions/3077162/name-for-the-kernel-lemma

[Patrick Massot]

So we need to prove this in mathlib. Then people will see this strange name "kernels lemma" and click the link to start learning linear algebra properly.

[Patrick Massot]

I see there is a "unitary ring" line. Do we plan to have non-unital rings in mathib at some point?

[Johan Commelin]

I wouldn't know the axioms... mul_assoc? But not has_one?

[Patrick Massot]

https://en.wikipedia.org/wiki/Ring_(mathematics)#Multiplicative_identity:_mandatory_vs._optional

[Johan Commelin]

I guess the answer to your question is no.

[Paul van Wamelen]

I submitted another PR

[Johan Commelin]

We have noncommutative rings in mathlib... isn't that good enough?

[Patrick Massot]

Crap, this PR is super conflicting what I was doing

[Paul van Wamelen]

I can try and "hand merge" it... Gimme a sec.

[Patrick Massot]

There is no conflict on GitHub. It conflicts my open PR and my local modifications. But it's ok, I'll handle it.

[Patrick Massot]

Let's do both actually: I'll my merge my PR and you'll fix yours

[Patrick Massot]

And then I'll fix conflicts with my local changes

[Patrick Massot]

Done. Now you have conflicts

[Kevin Buzzard]

https://fr.wikipedia.org/wiki/D%C3%A9composition_de_Dunford -- this is the first time I've seen the French choose to name some lemma after someone who isn't French, when there was a perfectly good French option (décomposition de Jordan-Chevalley)

[Patrick Massot]

And how do you say "réduction des endomorphismes"?

[Reid Barton]

Is this "structure theory of endomorphisms"?

[Reid Barton]

I guess that's kind of a mixed metaphor

[Paul van Wamelen]

I think I cleared the conflicts

[Patrick Massot]

Awesome.

[Ryan Lahfa]

Patrick Massot said:

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

My whole problem, I even warned about it before :D

[Ryan Lahfa]

Hahahaha, this thread has really turned into how does you say X in english :'D

[Kenny Lau]

what a surprise, a second language is not just the first language plus a dictionary

[Scott Morrison]

I think we'll eventually want non-unital rings, sadly. For example you might want continuous functions vanishing at infinity on a locally compact space as a non-unital algebra, to state the version of Stone-Weierstrass for locally compact spaces.

[Patrick Massot]

I just pushed some beginning of structure cleanup, but I need to go. Everybody should feel free to work on this file, I won't touch it in the next 10 hours.

[Ryan Lahfa]

Kenny Lau said:

what a surprise, a second language is not just the first language plus a dictionary

But it's surprising for cancelling/annihilating polynomials to not have any equivalent, like while I was learning linear algebra, this term was pronounced like 30 times per day during exercises

[Ryan Lahfa]

And same goes for many terms I guess

[Alex J. Best]

I think we just got away with let $P$ be a polynomial s.t. $P(M) = 0$, as its not really longer to say the full definition in this case!

[Ryan Lahfa]

Alex J. Best said:

I think we just got away with let $P$ be a polynomial s.t. $P(M) = 0$, as its not really longer to say the full definition in this case!

Yes but sometimes you want to say things like
"Method to compute $\exp(M)$ when you have a $P$ such that $P(M) = 0$"
vs
"Method to compute $\exp(M)$ using an annhilating polynomial"

[Ryan Lahfa]

Anyway, I'm getting sidetracked… :D

[Kevin Buzzard]

Hecke algebras are something which will be within reach soon, and they're rings without 1

[Johan Commelin]

#5 is about affine spaces. I'm kicking #2816 on the merge queue. Once it lands, we can fill out this section. @Joseph Myers please let us know if you would like to contribute.

[Johan Commelin]

@Oliver Nash and/or @Anne Baanen Would you mind filling out #4 on bilinear and quadratic forms?

[Johan Commelin]

If any of you doesn't have time/energy/interest in contributing, just say so. No hard feelings.

[Johan Commelin]

#7 is on single variable complex analysis, and it's going to make us look ridiculous...

[Johan Commelin]

I'll start on #8. Topology now.

[Patrick Massot]

Maybe it would make more sense to work on an algebraic section since I would have an easier time doing topology than algebra

[Johan Commelin]

The first item is interesting. We don't have metric_space.to_topological_space I guess. So what do we do? metric_space.to_uniform_space?

[Patrick Massot]

I found rather link a lemma saying something is open if it contains an open ball around each point, or something like that

[Johan Commelin]

Aha, makes sense

[Johan Commelin]

The remaining sections are:

#09. Differential Calculus
#10. Integral Calculus
#11. Probability Theory
#12. Distribution calculus
#13. Numerical Analysis

I fear that the last 3 will stay empty.

[Patrick Massot]

Don't we have at least the definition of a probability measure?

[Johan Commelin]

pmf ­– Probability mass function

[Johan Commelin]

But otherwise, not much, I think

[Oliver Nash]

Johan Commelin said:

Oliver Nash and/or Anne Baanen Would you mind filling out #4 on bilinear and quadratic forms?

I would be delighted to fill this out. I'll try and find time this evening though it might not happen till tomorrow.

[Patrick Massot]

Don't hesitate to reorder and slightly reword stuff if it makes more sense.

[Oliver Nash]

Thanks, will do. Needless to say I'm happy for @Anne Baanen to do this too / instead.

[Patrick Massot]

Also keep in mind the structure is not yet fully compliant. We want to have exactly three levels: main heading, sub heading, leaf containing a link.

[Oliver Nash]

Understood, I will stick to a three-level structure.

[Johan Commelin]

Thanks for helping!

[Oliver Nash]

My pleasure!

[Johan Commelin]

https://github.com/leanprover-community/leanprover-community.github.io/pull/48 fills links in basic topology (there's a lot left for the experts :wink:)

[Johan Commelin]

Note: affine spaces have been merged

[Patrick Massot]

Ok, I merged but indeed we have several more links to add to this section. I'll do it right now

[Patrick Massot]

Each time I type leanproject up in mathlib, elan downloads something... :grinning:

[Patrick Massot]

Why can't I find that a real normed space is finite-dimensional iff the unit ball is compact? Is it really missing?

[Patrick Massot]

I've updated the metric topology section.

[Sebastien Gouezel]

The useful implication is there (finite_dimensional.proper). The useless implication has been done by a student of Kevin, if I recall correctly, but it never made it into mathlib.

[Kevin Buzzard]

https://github.com/LAC1213/compact_unit_ball

[Patrick Massot]

Ok, so I can't really tick that one off. Too bad this project never went to mathlib...

[Ryan Lahfa]

Patrick Massot said:

Ok, so I can't really tick that one off. Too bad this project never went to mathlib...

If there was a license, this could be salvaged

[Patrick Massot]

I'm pretty sure you can discuss this with the author. That would be a nice little project.

[Patrick Massot]

Of course turning this into something PRable means work.

[Patrick Massot]

But it would be a nice way to get familiar with both linear algebra and topology in mathlib.

[Sebastien Gouezel]

If I remember correctly, there is the useless assumption that the field is complete in this project, but this is not crazy to have this assumption.

[David Wärn]

Shouldn't this argument be phrased using docs#riesz_lemma ?

[Patrick Massot]

Indeed it looks like someone started this road but gave up.

[Patrick Massot]

It seems to be Jean. @Jean Lo what is the status of this?

[Joseph Myers]

What I defined for affine spaces is very minimal at present, so there won't be much from that list (on the Euclidean side, I suppose #2865 provides at least "Angles of vectors"). It's not yet PRed, but I do have the result that (not necessarily bijective) isometries between Euclidean affine spaces are affine maps that preserve the inner product (the list wants rather more about isometries than that, however).

[Johan Commelin]

@Joseph Myers Sure... but all small bits help.

[Patrick Massot]

Joseph, did you coordinate with https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/mazur_ulam.html?

[Johan Commelin]

Is "C is algebraically closed" somewhere on the agreg list?

[Patrick Massot]

I hope so

[Patrick Massot]

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

[Joseph Myers]

@Patrick Massot No, I just wrote a separate proof (for Euclidean spaces, the (easy) result isn't limited to bijective isometries, and the "preserves inner product" part is something useful for describing the effect of an isometry (from a finite-dimensional space to itself) on coordinates, once a frame has been chosen, as the combination of an orthogonal matrix and a translation).

[Yury G. Kudryashov]

Actually, you don't need a Euclidean space here. Only a normed_add_torsor over a normed_vector_space with strictly convex balls.

[Yury G. Kudryashov]

Actually you can prove the following fact. Let f be an isometry, and its codomain is a normed_add_torsor R E such that 0 < r → dist x y = r → dist x z = r → r < dist x (2 * y - z). Then f is affine.

[Johan Commelin]

Patrick Massot said:

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

I've never heard of this name before...

[Joseph Myers]

Feel free to add these more general results! I think for isometries of Euclidean spaces there should be a function mapping f (such that isometry f) to an affine_map (for whatever type classes that include the case of Euclidean spaces), and a proof that the corresponding linear_map preserves the inner product, but I'm not particularly concerned with how we get there.

[Yury G. Kudryashov]

BTW, do you prove that for an affine isometry the corresponding linear_map is an isometry as well?

[Ryan Lahfa]

Johan Commelin said:

Patrick Massot said:

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

I've never heard of this name before...

https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_fondamental_de_l%27alg%C3%A8bre
That's the name we give it, maybe we love too much to give names to theorem.
I even heard that the fact that the continuous image of a compact is a compact is called Weierstrass' theorem :D in France…

[Yury G. Kudryashov]

English Wikipedia never mentions this name, just "Fundamental theorem of algebra"

[Ryan Lahfa]

That's an invitation to change the name into "fundamental theorem of algebra" I believe

[Yury G. Kudryashov]

https://github.com/leanprover-community/leanprover-community.github.io/commit/bebb1e9cafaee64414639bc9714f09d9b124ca0f

[Patrick Massot]

Some algebraists will hate you Yury. I know more than one that is really pissed off when an analysis theorem is called the "fundamental theorem of algebra".

[Kevin Buzzard]

It's because algebra := polynomials and matrices in 1800 or something, right?

[Yury G. Kudryashov]

@Patrick Massot Is there a title that is both widely recognizable (in English) and won't make algebraists hate me?

[Johan Commelin]

The algebraists should be happy that they have opportunity to invade the territory of the analysts!
Geometers don't even have a "fundamental theorem".... look at them :stuck_out_tongue_wink:

[Patrick Massot]

The title could be "$\mathbb C$ is algebraically closed"...

[Johan Commelin]

Such a boring theorem name... you've been influenced too much by mathlib naming conventions.

[Patrick Massot]

I can see you don't know what this theorem is called in mathlib...

[Johan Commelin]

polynomial.complex_exists_root?

[Johan Commelin]

That's just because we don't have class algebraically_closed (K : Type*) [field K] yet.

[Johan Commelin]

Otherwise it would be complex.algebraically_closed.

[Joseph Myers]

@Yury G. Kudryashov I didn't prove that particular result that the corresponding linear_map is an isometry, but it's a straightforward consequence of the other facts in this area.

[Yury G. Kudryashov]

E.g., from #2907

[Joseph Myers]

Actually it's true more generally than that, for the map (at a particular base point) on vectors induced by any isometry between two normed_add_torsors. Does this belong in mathlib?

import analysis.normed_space.add_torsor
import topology.metric_space.isometry

variables (V1 : Type*) {P1 : Type*} [normed_group V1] [metric_space P1] [normed_add_torsor V1 P1]
variables (V2 : Type*) {P2 : Type*} [normed_group V2] [metric_space P2] [normed_add_torsor V2 P2]

/-- The map on vectors corresponding to a map from P1 to P2, at a base
point p. -/
def vector_map_of_point_map (f : P1 → P2) (p : P1) : V1 → V2 := λ v, f (v +ᵥ p) -ᵥ f p

/-- The map described by `vector_map_of_point_map` is an isometry if
the original map is one. -/
lemma isometry_vector_map_of_point_map {f : P1 → P2} (h : isometry f) (p : P1) :
  isometry (vector_map_of_point_map V1 V2 f p) :=
begin
  rw isometry_emetric_iff_metric at *,
  unfold vector_map_of_point_map,
  intros x y,
  rw [dist_eq_norm, dist_eq_norm, add_torsor.vsub_sub_vsub_right_cancel],
  convert h (x +ᵥ p) (y +ᵥ p),
  { rw add_torsor.dist_eq_norm V2 },
  { rw [add_torsor.dist_eq_norm V1, add_torsor.vsub_vadd_eq_vsub_sub, add_torsor.vadd_vsub] }
end

[Johan Commelin]

@Joseph Myers I think it does, but I wouldn't make a new definition. (Or at least, don't use the definition in the lemma. Rather, take any random map g : V1 → V2 and the hypothesis hg : \forall v, g v = f (v +ᵥ p) -ᵥ f p. In this way, the lemma will also be applicable to maps that aren't definitionally a vector_map_of_point_map. My intuition says that is what will happen in practice.

[Yury G. Kudryashov]

Note that with #2907 you can represent your map as a composition of known isometries, and get the proof from isometry.comp.

[Yury G. Kudryashov]

Probably we should stop hijacking Patrick's thread.

[Johan Commelin]

@Ryan Lahfa There's something wrong with the statement-todo and statement-done classes. Currently cards are also getting these classes, but not in an intuitive way.

[Johan Commelin]

I think a card should only be marked statement-done if all of its children are completely done.

[Johan Commelin]

Otherwise our todo-list is much too optimistic.

[Johan Commelin]

image.png
This doesn't really look as I would expect. The todo toggle seems to be inverted...

[Johan Commelin]

I'm seeing todo's but the toggle is off, and when I switch it on, the items that are not links go away

[Ryan Lahfa]

Johan Commelin said:

Ryan Lahfa There's something wrong with the statement-todo and statement-done classes. Currently cards are also getting these classes, but not in an intuitive way.

There might be a bug

[Ryan Lahfa]

I'll look into it

[Johan Commelin]

Thanks!

[Johan Commelin]

Alternative: strip out the classes and generate two files...

[Ryan Lahfa]

Johan Commelin said:

I'm seeing todo's but the toggle is off, and when I switch it on, the items that are not links go away

I think it's also due to the fact you don't want to show parts when they are empty (e.g. all children are todos), but I'm not sure, I'll look at it again

[Ryan Lahfa]

Hahahaha

[Johan Commelin]

Let's just make sure that the list works for the IAS talk, and then we can add the fancy buttons afterwards.

[Ryan Lahfa]

Agreed ; if I don't find a trivial solution quickly enough, I'll send directly a PR to produce two files, sounds good?

[Kevin Buzzard]

So I'm having a look at the current state of this (the yaml file). For "direct sum" (line 12) we have the unnamed instance direct_sum.semimodule. This is an "external direct sum". From the context of the list it looks like an internal direct sum though, i.e. a sum of two submodules within a big module, where the submodules happen to have trivial intersection. Should we just not care and link to the external direct sum? And can one link to an unnamed instance name?

[Johan Commelin]

Internal direct sum = sup in the lattice semimodule _ _??

[Kevin Buzzard]

It's no different to internal sum though

[Johan Commelin]

internal direct sum is an awkard notion, where you want to know that things are orthogonal, and then take a sup.

[Kevin Buzzard]

I remember learning this as an UG too. I think the idea is that abstract direct sum of two vector spaces is supposed to be too difficuilt, and this internal direct sum -- if V and W are subspaces of some large vector space X and V and W intersect trivially, then the space spanned by V and W satisfies the universal property of the abstact direct sum -- was taught first.

[Johan Commelin]

We just totalise the function...

[Johan Commelin]

And define it for non-othogonal submodules as well

[Patrick Massot]

The idea is to find a good entry point for people that may not know much about formalization, but want to use this notion. Sometimes the best entry point for a definition is actually a lemma saying that some funny mathliby way of doing stuff is giving you the expected behavior.

[Kevin Buzzard]

https://github.com/leanprover-community/leanprover-community.github.io/pull/50 bilinear and quadratic forms

[Patrick Massot]

Merged!

[Patrick Massot]

But I'll probably need to fix structure

[Kevin Buzzard]

Did I do something wrong? Let me know now because I'm about to start on affine spaces

[Kevin Buzzard]

And I didn't know how to check if the links work.

[Kevin Buzzard]

(e.g. I might have missed a namespace)

[Patrick Massot]

Patrick Massot said:

Don't hesitate to reorder and slightly reword stuff if it makes more sense.

Also keep in mind the structure is not yet fully compliant. We want to have exactly three levels: main heading, sub heading, leaf containing a link.

[Patrick Massot]

Hold on for two minutes

[Patrick Massot]

You can have a look at https://github.com/leanprover-community/leanprover-community.github.io/commit/90a877595a2bc219ac0642d1f9d6fae477f15972

[Patrick Massot]

That's what I call "fixing structure", following the guidelines quoted above.

[Kevin Buzzard]

I see, so actually changing the structure of the yaml to be a bit more sane

[Kevin Buzzard]

keep precisely the same leaves but we can move them around a bit

[Patrick Massot]

Yes. Actually I'm pretty disappointed by the source document. I thought it was more structured.

[Kevin Buzzard]

it probably wasn't written by a computer scientist!

[Johan Commelin]

https://github.com/leanprover-community/leanprover-community.github.io/commit/90a877595a2bc219ac0642d1f9d6fae477f15972#diff-25c153ec778dc59bca8f669ad98bcad4R241
Should that be cross product?

[Patrick Massot]

Sometimes I even change leaves a bit (and I added Jordan normal form). But the main point is that leaves should be at level 3.

[Patrick Massot]

https://en.wikipedia.org/wiki/Triple_product

[Patrick Massot]

Oh, the preceding line is a wrong translation

[Patrick Massot]

"vector product" means cross product

[Johan Commelin]

I'm learning new stuff everyday...

[Patrick Massot]

But we call it "produit vectoriel" in French.

[Kevin Buzzard]

We don't have any of these crazy things which assume finite-dimensionality (or in this case 3-dimensionality)

[Patrick Massot]

The triple product thins is about computing determinants using the Euclidean structure

[Kevin Buzzard]

3 is overrated

[Patrick Massot]

That's why I named this section "low dimensions"

[Kevin Buzzard]

why not just call it n-ary product and link to det :-)

[Patrick Massot]

The fact that you can compute determinants using the Euclidean structure has some content

[Patrick Massot]

But I wouldn't say this has super high priority, unless you specifically work towards low-hanging fruits in this list

[Ryan Lahfa]

Kevin Buzzard said:

We don't have any of these crazy things which assume finite-dimensionality (or in this case 3-dimensionality)

That's for people who does physics

[Patrick Massot]

I thought physics was all about dimension 4.

[Kevin Buzzard]

I thought 10?

[Ryan Lahfa]

Sometimes they forget about time and wrapped dimensions, :-°

[Johan Commelin]

@Yury G. Kudryashov Didn't you do stuff on Grönwell in mathlib at some point? I can't find it.

[Yury G. Kudryashov]

https://leanprover-community.github.io/mathlib_docs/analysis/ODE/gronwall.html

[Johan Commelin]

Aah, I made a typo...

[Johan Commelin]

Thanks!

[Johan Commelin]

We don't really have a definition of a sigma algebra :expressionless:

[Yury G. Kudryashov]

We have [measurable α]

[Johan Commelin]

Yup... it's just that the name isn't recognisable

[Johan Commelin]

I've filled in a couple more links in analysis and measure theory. The part on integration I didn't really touch... I've never used that part of the library.

[Sebastien Gouezel]

A sigma algebra is exactly an instance of measurable_space α

[Johan Commelin]

It's just that the list has 'measureable spaces' and 'sigma algebras' as seperate items :expressionless:

[Reid Barton]

We also have measurable spaces https://github.com/leanprover-community/mathlib/blob/master/src/measure_theory/category/Meas.lean#L31 :upside_down:

[Gabriel Ebner]

What is the difference between a measurable space and a set with a sigma algebra?

[Reid Barton]

Those are the same, the issue is that (by analogy with group, etc.) the structure measurable_space is named after the bundled concept, when it actually is the unbundled one. Same with topological_space.

[Johan Commelin]

We really need this automated "rename declarations" bot, that will just go through the entire source to rename things while I sleep.

[Patrick Massot]

Thanks Johan. Some items are wrong and a lot are missing but it still helps. I'll merge it and improve it.

[Reid Barton]

FWIW I'm not suggesting renaming the mathlib definitions, just explaining why they don't exactly align with the math names: basically because we don't really use the bundled objects so we have just one name for both "measurable space" and "sigma-algebra".

[Patrick Massot]

I think the module docstring of https://leanprover-community.github.io/mathlib_docs/measure_theory/measure_space.html could be easier to read...

[Sebastien Gouezel]

Ah, this is a docstring from the ancient times!

[Patrick Massot]

Sébastien, do you know whether counting measures are hidden somewhere?

[Patrick Massot]

And non-discrete probability measures?

[Sebastien Gouezel]

The counting measure is in measure_space.lean

/-- Counting measure on any measurable space. -/
def count : measure α := sum dirac

[Johan Commelin]

Patrick Massot said:

Thanks Johan. Some items are wrong and a lot are missing but it still helps. I'll merge it and improve it.

Sorry for the mistakes

[Patrick Massot]

Oh, I should have checked here before pushing, I missed Sébastien's message.

[Johan Commelin]

You can push again... it's free.

[Patrick Massot]

Done

[Patrick Massot]

@Sebastien Gouezel would you mind going over https://github.com/leanprover-community/leanprover-community.github.io/blob/c2631dcdfe279ebe5869eb62e6289a6e7d426681/data/overview.yaml#L505-L585 to tell us if we missed stuff?

[Sebastien Gouezel]

Monotone convergence is lintegral_supr_ae in integration.lean.

[Sebastien Gouezel]

Fatou is lintegral_liminf_le in integration.lean.

[Sebastien Gouezel]

By the way, just before Fatou there are the two lines

-- for some reason the next proof fails without changing the priority of this instance
local attribute [instance, priority 1000] classical.prop_decidable

It won't be a surprise to anyone that, with current awesome Lean, they can be safely removed.

[Patrick Massot]

I just skipped that file because it seems to be all about the mysterious ∫⁻. Isn't there a version for actual integrals?

[Sebastien Gouezel]

The usual textbook versions of these theorems are for nonnegative functions that are allowed to take the value $+\infty$, so they really talk about the ∫⁻. I just checked in Rudin, for instance, and both monotone convergence and Fatou's lemma are just given in this version.

[Patrick Massot]

Thanks. We really need some md file describing how to navigate that part of mathlib.

[Johan Commelin]

Well, a yaml file is a good first start (-;

[Patrick Massot]

The YaML file doesn't explain what this crazy ∫⁻ symbol means

[Patrick Massot]

Sébastien, since you're clearly not working on this referee report, would you mind handling Section 9?

[Patrick Massot]

https://github.com/leanprover-community/leanprover-community.github.io/edit/newsite/data/overview.yaml

[Sebastien Gouezel]

I got through the interesting part of the paper, now it's the boring technical part, so any excuse for procrastination is good. I'll have a look.

[Patrick Massot]

At this stage you can write to the editor: I think the theorem is interesting and the new ideas are nice, now I'm waiting for the formalization of the technical details.

[Sebastien Gouezel]

People still need to get their paper published in a reasonable amount of time, especially if they're young. I could do this when I refer papers whose authors are all tenured :)

[Johan Commelin]

If that catches on, you'll find authors scrambling for getting a phd student or postdoc as coauthor

[Patrick Massot]

@Ryan Lahfa since you didn't fix the bugs quickly enough for my talk, I went ahead and split the display into two files. I also added a link.

[Patrick Massot]

I also cleaned up the remaining sections so that the structure should be consistent now. I'm convinced there are still missing links, but people should now track them by comparing https://leanprover-community.github.io/undergrad_todo.html with what they think is in mathlib.

[Sebastien Gouezel]

Patrick Massot said:

Ryan Lahfa since you didn't fix the bugs quickly enough for my talk, I went ahead and split the display into two files. I also added a link.

How did the talk go, by the way?

[Johan Commelin]

It's at 1200 tonight

[Johan Commelin]

So around 1215, Patrick is going to demo Zulip, and we should all be making silly jokes

[Gabriel Ebner]

I'm sorry the widgets didn't make it in time for the talk, but the vscode extension still has some rough edges and Ed is a bit busy at the moment.

[Gabriel Ebner]

@Johan Commelin Which timezone?

[Johan Commelin]

Midnight in Amsterdam, Paris, Berlin

[Johan Commelin]

I think it's 1800 Princeton time

[Gabriel Ebner]

So in 3 hours, i.e. 24:00? I was confused by the 12.

[Patrick Massot]

It's getting dangerously close.

[Reid Barton]

I see 5:30 pm on the IAS website which I assume is US/Eastern

[Patrick Massot]

Yes, 3 hours

[Patrick Massot]

5:30 is the beginning of discussions, but the talk starts half an hour later.

[Patrick Massot]

It's a crazy format.

[Reid Barton]

Interesting idea to discuss the talk before it happens

[Patrick Massot]

I replaces a very informal seminar featuring wine and cheese.

[Patrick Massot]

Before the talk peoples are randomly distributed in Zoom rooms with 6 participants.

[Patrick Massot]

Then there is the talk and then general discussion.

[Kevin Buzzard]

We had this with my OWLS talk and it worked really well, but we did it after not before.

[Patrick Massot]

The talk went fine, discussion just stopped (almost two hours after the talk stopped).

[Johan Commelin]

#2946 Eisenstein criterion (thanks @Chris Hughes :tada: ) is on the merge queue.

[Johan Commelin]

So we can update this yaml in a moment (-;

[Johan Commelin]

@Patrick Massot @Bryan Gin-ge Chen What do you think of hosting things like overview.yaml in mathlib? Then PRs that add new stuff can also add it to that file directly.

[Johan Commelin]

(And it makes it easier for a reviewer to say: Hey, please update that file as well.)

[Patrick Massot]

Of course I don't have anything against that. I don't know what would be the best strategy. Maybe the website CI could simply download the file from mathlib before running the site building script.

[Bryan Gin-ge Chen]

I think it's probably a good idea. Moving overview.yaml to mathlib will change an informal dependency (we have to remember to make changes in two repos) to a technical one (rebuilding the website will require wget from mathlib github as Patrick says).

[Johan Commelin]

Yup, that's the kind of thing I was meaning

[Johan Commelin]

Same applies to 100.yaml

[Johan Commelin]

And stacks.yaml, when we ever get there (-;

[Patrick Massot]

The case of 100.yaml is slightly different because it also lists stuff from outside mathlib

[Johan Commelin]

But only very little right? Even archive/ is in the mathlib repo

[Johan Commelin]

So it's only CH that is outside, I think.

[Patrick Massot]

We also have more polishing work to be done on this list stuff. We only have the minimal version. We need to get a better idea about interaction between this list and https://leanprover-community.github.io/mathlib-overview.html.

[Patrick Massot]

One option is to rename overview.yaml into undergrad.yaml, create a file advanced_topics.yaml for everything else, and start by porting whatever is list in the overview page but not in the undergrad page to this new file.

[Patrick Massot]

The border between undergrad and the rest is pretty blurry, but I think it's interesting anyway.

[Patrick Massot]

Because it allows to also have https://leanprover-community.github.io/undergrad_todo.html which would not make sense with an open ended scope.

[Patrick Massot]

Also note that I don't have anything against resurrecting the switches gathering stuff and todo stuff on the same page, but they were simply too buggy for now.

[Johan Commelin]

Yup, no worries.

[Johan Commelin]

I think the switches are more user friendly (when they work correctly). But separate pages is developer friendly, and that's also worth something :rofl:

[Patrick Massot]

Yesterday I also modified Ryan's python code at https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/make_site.py#L134 in a way that would probably make it easier to fix the bugs. In defense of Ryan's code, I need to say that he worked on a badly specified issue. It wasn't clear in the beginning what kind of structure we wanted to support. The idea that we want exactly three levels (topic, subtopic, item) emerged while working on the list. This is now fully enforced in the YaML file (unless I missed something) and this should make everything easier (including CSS styling).

[Patrick Massot]

Another call to contributions: now that the list is visible on the website, it would be nice to write the little piece of CI that checks that urls don't break (and are correct to start with). One needs to be careful since having a successful http request is not enough to guarantee that the anchor is there: requesting https://leanprover-community.github.io/mathlib_docs/topology/basic.html#poincare_conjecture will not give you any http error.

[Johan Commelin]

I think it is time to go through https://leanprover-community.github.io/undergrad_todo.html again, to check if some stuff has been done already. Here's a first set of remarks/questions. I think there is more.

Linear algebra

• @Sebastien Gouezel Didn't you do Gaussian elimination
• Is the matrix exponential now a consequence of some very general exponential in Banach algebras or something?
• The special linear group is done, I think

Group theory

• Maschke is done a PR exists for this: #9398

Ring theory

• Algebra over a commutative ring. @Patrick Massot do you mean something that docs#algebra doesn't provide?
• rational fraction fields with one indeterminate over a field: #9563

Bilinear and Quadratic Forms Over a Vector Space

• real classification --- is this something else than Sylvester's inertia? Because we have that

[Bryan Gin-ge Chen]

#9398 by @Scott Morrison addresses Maschke.

[Sebastien Gouezel]

There are many flavors of gaussian elimination. The most classical one is where you are only allowed operations on the rows of a matrix, but where you need sometimes to exchange two rows, if there is a zero at the bad place. I did another version where I don't exchange two rows, but where I do operations on rows and columns. I am not sure it qualifies as gaussian elimination (although it is just as good in practice, and in fact better for what I wanted to do (docs#measure_theory.measure.map_linear_map_add_haar_eq_smul_add_haar) since it avoids the discussion of rows exchanges).

[Patrick Massot]

I agree this list needs cleaning (probably also remove a couple of meaningless items and fix some translations mistakes). The reason why algebra is not crossed out is I guess we waited to have non associative algebras (or even non-unital?). I don't know what is the current status.

[Johan Commelin]

@Eric Wieser @Oliver Nash we have non assoc rings now? How about algebras?

[Patrick Massot]

About Maschke, do we have the usual statement (involving sums of irreducible representations) now?

[Oliver Nash]

Yes, though it's not quite as pretty as it might be. E.g., we have docs#non_assoc_semiring but no non_assoc_ring.

[Patrick Massot]

The question about algebra is: do we have a structure that cover both the docs#algebra and docs#lie_algebra?

[Oliver Nash]

Johan Commelin said:

Eric Wieser Oliver Nash we have non assoc rings now? How about algebras?

Also since our bundled algebra class is (unfortunately) still stuck in the (unital) associative world, the following is how to declare a non-assoc algebra:

variables (R A : Type*) [comm_semiring R] [non_assoc_semiring A]
variables [module R A] [is_scalar_tower R A A] [smul_comm_class R A A]

[Patrick Massot]

About matrix exponential, I guess we are missing some glue, but maybe I'm wrong. @Anatole Dedecker ?

[Patrick Massot]

Oliver, this has a unit, right? It doesn't happen so often for Lie algebras.

[Oliver Nash]

Yes, that has a unit. There is a flavour without a unit. You just write non_unital_non_assoc_semiring A.

[Yury G. Kudryashov]

I have a definition of exp that works in any Banach algebra.

[Yury G. Kudryashov]

I mean, in a local branch.

[Yury G. Kudryashov]

And defined using analytic functions.

[Yury G. Kudryashov]

I think that eventually we should replace complex.exp and real.exp with this definition but it's not PR-ready yet.

[Yury G. Kudryashov]

(and I don't have a migration path yet).

[Patrick Massot]

Yury, we already have https://github.com/leanprover-community/mathlib/blob/ef139bd08ff414f0f6354461d26274c18a6c405d/src/analysis/normed_space/exponential.lean

[Yury G. Kudryashov]

Indeed. Then just ignore my comments.

[Patrick Massot]

Actually it probably requires no glue. We should check that type class inference is happy to provide this on real or complex valued matrices and selected one declaration to link.

[Patrick Massot]

And I agree it would be nice to replace the elementary versions, but clearly mathlib is going in the opposite direction (removing calculus from proofs about exponential to untangle calculus and measure theory).

[Oliver Nash]

Patrick Massot said:

The question about algebra is: do we have a structure that cover both the docs#algebra and docs#lie_algebra?

Sort of. Since Lie algebras use the has_bracket typeclass and rings use the has_mul typeclass, it's not quite so simple. I believe the only place where we connect these two worlds is in the construction of the free Lie algebra as a quotient of the free non-unital, non-associative algebra.

E.g., here a has_mul is turned into a has_bracket: https://github.com/leanprover-community/mathlib/blob/5926f103c66a17a60eafc1aaec387d9db85a21ad/src/algebra/lie/free.lean#L115

[Sebastien Gouezel]

Patrick Massot said:

And I agree it would be nice to replace the elementary versions, but clearly mathlib is going in the opposite direction (removing calculus from proofs about exponential to untangle calculus and measure theory).

Apparently this should still be possible, using the bare definition of analytic functions and of the exponential (which does not require anything on derivatives) to define the power function, prove its basic properties, and then import it into measure theory.

[Patrick Massot]

And we managed to put several discussions in the same thread, it looks like we're back to the gitter days...

[Eric Wieser]

Ah, but unlike gitter we can move messages between threads if needed :) (edit: done, hope I didn't tread on anyone's toes)

[Yury G. Kudryashov]

I have a proof that exp in a normed algebra does not depend on the base field (at least if the base field is a normed algebra over rat).

[Anatole Dedecker]

I'm a bit late to the party, but the only thing lacking for matrix exponential is a normed algebra instance on matrices (I remember searching for it and not finding it). @Yury G. Kudryashov is docs#exp_eq_exp_of_field_extension similar to what you did ?

[Eric Wieser]

There's a PR open that adds a norm of some kind to matrices, right?

[Eric Wieser]

Just not the normed_algebra instance

[Yury G. Kudryashov]

Why do you need the char_p assumption?

[Yury G. Kudryashov]

I mean, can't you say "let p be the characteristic of K" in the proof?

[Yury G. Kudryashov]

I assumed that both fields are normed algebras over rat.

[Yury G. Kudryashov]

And made no assumptions like is_scalar_tower.

[Anatole Dedecker]

Yury G. Kudryashov said:

I mean, can't you say "let p be the characteristic of K" in the proof?

You are right, that is just an artifact of the original version I did. I'll PR a change soon.

[Anatole Dedecker]

Do you think it is possible to completely hide the base field ?

[Patrick Massot]

This is my periodic message about the missing undergrad math list. I think there is a lot of cleanup to do. Some people have important propaganda talks to deliver in mid-January and it would be nice to have an undergrad list sprint before then. Today I created two new wiki pages: trivial targets and low hanging fruits. The border between those categories is a bit fuzzy but I think the first list could be wiped out in one week. And both lists could be handled in one month if we manage to get some community dynamics here. Feel free to edit those wiki pages to claim items. I think that anyone having access to mathlib branches can edit them. You can also post messages here of course.

[Patrick Massot]

Of course if you feel more ambitious, the big targets list still exists.

[Heather Macbeth]

@Patrick Massot Regarding the classical groups, what we have in mathlib currently is

• matrix and endomorphism GL
• matrix SL (we should correct your wiki which says it's missing) but not endomorphism SL
• matrix O and U but not endomorphism O and U (they will be unlocked soon by @Frédéric Dupuis' work on the adjoint)
• neither matrix nor endomorphism SO, SU

So the currently accessible targets are endomorphism SL and matrix SO, SU. Do you agree?

[Eric Wieser]

Those new pages are great @Patrick Massot!

[Patrick Massot]

As explained in the wiki pages, some of the "trivial targets" are simply waiting for declaration names that already exist.

[Patrick Massot]

And indeed some stuff already exist for classical groups. The satisfactory situation would be to have, for each case, the matrix version, the endomorphism version and a group isomorphism when a suitable basis is given.

[Heather Macbeth]

My point is that endomorphism O, U, SO and SU are not actually trivial targets.

[Patrick Massot]

What is non-trivial?

[Heather Macbeth]

Defining the adjoint endomorphism, that's what @Frédéric Dupuis is working on but it needs all the new work on conjugate-linear maps.

[Eric Wieser]

Is it worth having a dedicated zulip stream for the undergrad math list?

[Patrick Massot]

Oh, I thought we already had adjoints!

[Yaël Dillies]

Maybe not the undergrad maths list per say, but for short easy projects?

[Patrick Massot]

I was tricked by the existence of docs#is_self_adjoint

[Heather Macbeth]

We have the adjoint (=conjugate-transpose) for matrices, docs#matrix.star_ring, but not yet for endomorphisms.

[Patrick Massot]

But there is a loophole, you can define self-adjoint whithout adjoint.

[Yaël Dillies]

Note that continuity of convex functions is tackled by someone somewhere already, but I can't find it now... Maybe a branch?

[Patrick Massot]

Eric Wieser said:

Is it worth having a dedicated zulip stream for the undergrad math list?

Maybe. We can also create topics in the maths or general stream.

[Heather Macbeth]

Yaël Dillies said:

Note that continuity of convex functions is tackled by someone somewhere already, but I can't find it now... Maybe a branch?

By @Malo Jaffré maybe?

[Patrick Massot]

Continuity of convex functions should be a nice exercise, especially since it's in the one-variable section.

[Patrick Massot]

Heather, feel free to edit the wiki page with details about the status of classical groups.

[Heather Macbeth]

I just did, please check the diff and see if you agree.

[Heather Macbeth]

Couple more points: I don't think we can define and diagonalize "normal endomorphisms" until we have the adjoint. So I'd like to remove that from "trivial targets" also (it's definitely on my to-do list once we have it). OK?

[Yaël Dillies]

Heather Macbeth said:

Yaël Dillies said:

Note that continuity of convex functions is tackled by someone somewhere already, but I can't find it now... Maybe a branch?

By Malo Jaffré maybe?

I think so, yeah

[Patrick Massot]

Heather Macbeth said:

I just did, please check the diff and see if you agree.

It's fine except you modified a section header, making it more difficult to locate the item on the undergrad todo page.

[Heather Macbeth]

simultaneous diagonalization of two real quadratic forms, with one positive-definite: This should very easily follow from what we already have.

I think the difficulty here is in expressing "two separate real quadratic forms" -- this is related to the mess with our various definitions of bilin_form, sesq_form, inner_product_space, etc, which have been causing @Moritz so many headaches. I think it is only fair to call it a "trivial target" if you or another expert will write up a sketch in Lean for the proposed formulation.

[Heather Macbeth]

piecewise $C^k$ functions

Wasn't there some subtlety in how to define these (so again, not a "trivial target" in the sense that a casual user could knock it off easily)? I think @Yury G. Kudryashov had an idea for how this should be done.

[Patrick Massot]

Feel free to move stuff from the first list to the second one (and add comments).

[Heather Macbeth]

Also: In a sense, we have the classification of elements of $O(2, \mathbb{R})$, since we have the classification of real-linear isometries of $\mathbb{C}$. Does this count?

[Heather Macbeth]

docs#linear_isometry_complex

[Patrick Massot]

It would be nicer to deduce from this a result that is explicitly about $\mathbb{R}^2$.

[Heather Macbeth]

It would be nice, but I'm not sure about how to formulate it. Do you want to say that a choice of inner product and of orientation on on a real 2d vector space $V$ together determine an almost-complex structure, and then say that an orientation-preserving linear isometry of $V$ is a complex rotation for that almost-complex structure? Or do you have something more co-ordinate based in mind?

[Patrick Massot]

Good question. I guess the simplest way to claim that item is a coordinate version.

[Joseph Myers]

I expect some form of that statement about orientation-preserving linear isometries corresponding to rotations in the complex numbers to come up as part of defining oriented angles. (We have quite a lot of API for isometries in the complex numbers and for complex.arg that it seems to make sense to reuse as part of defining oriented angles rather than duplicating, provided the resulting API for oriented angles is properly proved independent of choice of basis and can be used without caring about how complex numbers might have been used in its definition. So after #10737 I'm thinking of showing that (in positive dimension) there exist a basis (and an orthonormal basis, in the inner product space case) corresponding to a given orientation, then proving whatever's needed about mapping along basis.isometry_euclidean_of_orthonormal and complex.isometry_euclidean.symm to set up oriented angles and justify the definition.)

[Heather Macbeth]

This seems like the principled way to do it.

[Yury G. Kudryashov]

About piecewise $C^k$ functions. There are at least two useful notions here: an abstract property of being a $C^k$-smooth function, and a way of defining piecewise functions from some data (intervals and formulas on these intervals).

[Yury G. Kudryashov]

If we want to formalize approximation methods for ODEs (Euler, Runge–Kutta) as approximations to a solution on the whole interval (not a discrete set of pts), then it may be useful to have a way to define piecewise functions from some recursion formulas.

[Johan Commelin]

I suggest that if you make a PR that deals with item(s) on this list, we should label it with a undergrad label.

[Johan Commelin]

I will try to PR a definition (+ basic API) of matrix.rank later today.

[Johan Commelin]

#10826

[Malo Jaffré]

Heather Macbeth said:

Yaël Dillies said:

Note that continuity of convex functions is tackled by someone somewhere already, but I can't find it now... Maybe a branch?

By Malo Jaffré maybe?

Yes, I will try to cleanup and PR the one-dimensional version next week

[Johan Commelin]

I was away from home for two days. But rank of a matrix should now be done.

[Johan Commelin]

@Yury G. Kudryashov what is the status of matrix exponentials? Doesn't that follow from some abstract generic theory that is already done?

[Yury G. Kudryashov]

It does but possibly we need some glue code. @Anatole Dedecker is the right person to ask about this file.

[Johan Commelin]

I've started a thread about the cross product here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cross.20product

[Yury G. Kudryashov]

Should we add definitions like these?

def has_jump_discontinuity {α β : Type*} [linear_order α] [topological_space α] [topological_space β] (f : α → β) (a : α) :=
∃ b c, tendsto f (𝓝[<] a) (𝓝 b) ∧ tendsto f (𝓝[>] a) (𝓝 c) ∧ b ≠ c

def has_removable_discontinuity {α β : Type*} [topological-space α] [topological_space β] (f : α → β) (a : α) :=
∃ b ≠ f a, tendsto f (𝓝[≠] a) (𝓝 b)

[Yury G. Kudryashov]

(I'm grading a 1st year calculus exam, my problem asks about the type of discontinuity of a function)

[Yury G. Kudryashov]

I've started calculus-defs in branch#YK-calculus-defs. I don't know whether we want to have it somewhere in mathlib.

[Kevin Buzzard]

"I've got a ton of exams to mark and am in the middle of several projects, so I started another one because I don't want to mark the exams" ;-)

[Yaël Dillies]

Sounds like experience, Kevin!

[Johan Commelin]

Johan Commelin said:

what is the status of matrix exponentials? Doesn't that follow from some abstract generic theory that is already done?

@Anatole Dedecker what do you think about :this:

[Anatole Dedecker]

The only missing thing is a docs#normed_algebra instance for matrices. I could work on that but I don't know which norm we want on matrices. To me there are at least two sensible possibilities :

• the operator norm, which we could get by pulling back along linear_map.to_continuous_linear_map \comp matrix.to_lin'
• the Hilbert-Schmidt norm, induced by the usual inner product $\langle A, B\rangle := \mathrm{Tr}(A^\intercal B)$ (aka docs#matrix.dot_product)

[Johan Commelin]

So maybe we don't make it an instance, but provide two defs?

[Anatole Dedecker]

(Note that we have docs#matrix.normed_space as a def, but this isn't an algebra norm)

[Anatole Dedecker]

Johan Commelin said:

So maybe we don't make it an instance, but provide two defs?

That makes sense to me. And then I guess lemmas that are specifically about matrix exponential (there are none yet, but maybe they will come) should just have a normed_algebra assumption so you can use them with whatever norm you made a local instance of ?

[Eric Wieser]

Don't we already have a norm on matrices?

[Eric Wieser]

I thought that was PR'd a few weeks ago. Maybe docs#matrix.normed_group? nevermind, that's mentioned above

[Yury G. Kudryashov]

Can we have multiple defs that reuse the same topological_space (or even uniform_space) structure?

[Yury G. Kudryashov]

Then matrix exponent can be defined as tsum that uses pi topological space structure, and proofs can use (localized) normed_group + complete_space instances for proofs.

[Yury G. Kudryashov]

Kevin Buzzard said:

"I've got a ton of exams to mark and am in the middle of several projects, so I started another one because I don't want to mark the exams" ;-)

Exactly!

[Eric Wieser]

Are there algebras where the tsum exponential approach works but the norm exponential approach doesn't, or vice versa?

[Jireh Loreaux]

I was just discussing this with @Frédéric Dupuis. I think it makes sense not to impose a global instance as Johan suggested. There are lots of norms on matrices. And for example, when the entries lie in a C^*-algebra, you can even get a C^*-norm, but it's not exactly a "standard one" unless you develop the theory of Hilbert C^*-modules.

[Yury G. Kudryashov]

@Eric Wieser E.g., for matrices the norm approach "doesn't work" because we don't want to have a global instance.

[Eric Wieser]

I ask in the context of an exponential on the exterior and clifford algebras, where usually I see it used as "well the Taylor expansion obviously converges for this x I care about" without any real claim as to whether it is a total function

[Tomas Skrivan]

I'm not following this discussion too closely but I think some basic numerical analysis could be nice undergrad topic. ODE solvers, polynomial approximation, numerical integration, root finding etc. Once mathlib gets ported to Lean 4 I could actually use these theorem to properly formalize numerical library I'm working on.

[Patrick Massot]

Tomas, there is indeed some numerical analysis in the full list but I didn't put any of it in my short term targets because we currently don't have anything. So this is not part of what I would encourage people to work one, but everybody is free to work on anything.

[Eric Wieser]

Johan Commelin said:

Yury G. Kudryashov what is the status of matrix exponentials? Doesn't that follow from some abstract generic theory that is already done?

I've made a first pass of this in #13520, which has grown quite a dependency tree

[Eric Wieser]

30 PRs later, the branches of that tree have been pruned; it's ready for review!

[Eric Wieser]

I've left det (exp _ _ A) = exp _ _ (trace A) as an exercise for some poor undergrad to pick up

[Reid Barton]

By the way, I can kind of understand making the field argument of exp explicit (even though it seems unnecessary with an adjusted definition) but why is the algebra argument explicit? Isn't it just the type of A?

[Eric Wieser]

Yes, I agree we should remove that argument

[Eric Wieser]

Done in #13986

[Eric Wieser]

What exactly is meant by "endomorphism" in the "endomorphism exponential" entry? docs#module.End (which has no norm yet)? V →L[K] V (docs#continuous_linear_map)?

[Anatole Dedecker]

The latter I would say

[Eric Wieser]

https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets#exponential suggests something about finite dimensions, making me suspect the former

[Eric Wieser]

Which would essentially just be a case of inducing a norm via docs#linear_map.continuous_of_finite_dimensional

[Anatole Dedecker]

Oh yeah maybe

[Frédéric Dupuis]

In the finite dimensional case, shouldn't it already just work, since now we don't need an actual norm, but only the right topology?

[Frédéric Dupuis]

(Or do we not have a topology either?)

[Eric Wieser]

No topology either

[Eric Wieser]

But even if we had the topology, we wouldn't be able to use docs#exp_add without the norm too

[Eric Wieser]

We also don't have the topology on continuous maps when only a topology is available on the (co)domains

[Eric Wieser]

(cc @Jason KY. who had some thoughts on discord about that)

[Frédéric Dupuis]

In that case I think we should just declare victory on that undergrad math list bullet point, because it's very likely to just stay that way.

[Eric Wieser]

I'm not sure I agree; inducing the operator norm in the way I describe above sounds fairly straightforward

[Eric Wieser]

So I think it's place on the "trivial targets" list is justified

[Eric Wieser]

A warmup task for the position in Orsay perhaps ;)

[Frédéric Dupuis]

But do we want to do this? It makes sense to say that we simply don't put a default topology on linear_map because there are too many choices, in which case it's very reasonable to say that "endomorphism exponential" refers to continuous linear maps.

[Jason KY.]

Eric Wieser said:

(cc Jason KY. who had some thoughts on discord about that)

I'll copy what I wrote on discord here (the question is how to generalize the topology on the space of bounded linear operators between normed spaces to TVS. No promise what I've written is at all correct):

Since the space of operators is also a topological vector space it suffices to give a basis of open sets at 0. I think since this basis for the topology induced by the norm is given by $B_\epsilon(0) = \{T(B_1) \le \epsilon B_1\}$ we can do the similar for the not norm case. So since bounded is defined in general for all TVS (Yael pointed out this is the von Nuemann boundedness which we have), maybe a compatible basis at 0 is all sets of the form $\{T(U) \le V\}$ for bounded open neighborhood $U, V$ of 0 in $X$ and $Y$ resp.

[Eric Wieser]

Frédéric Dupuis said:

But do we want to do this? It makes sense to say that we simply don't put a default topology on linear_map because there are too many choices, in which case it's very reasonable to say that "endomorphism exponential" refers to continuous linear maps.

Are there more choices for the topology on linear_map than there are for continuous_linear_map?

[Eric Wieser]

Jason, I'm going to extract that post and my comments to a new thread since I've probably just confused things here - but thanks for the paste (edit; done)

[Frédéric Dupuis]

In the infinite-dimensional case there's a whole bunch of them; for continuous_linear_map we've picked one.

[Frédéric Dupuis]

So I guess what you would want to do is put the operator norm on it in the finite-dimensional case, and have no topology otherwise?

[Frédéric Dupuis]

I see, yes that would make sense.

[Eric Wieser]

We already have a norm only for the finite case for docs#pi.normed_group, so I think "no instance for infinite things" is not too weird a situation

[Peter Scholze]

As an undergrad, I once started a course on functional analysis given by Jens Franke (he's famous for work in number theory, but started his career as a functional analyst). In the first lecture, he introduced the seven topologies on the dual space...

(Shameless advertisement: In condensed math, the space of linear maps between two condensed vector spaces is canonically itself a condensed vector space.)

[Colleen Robles]

I'll supervise an undergraduate project on Lean later this summer. Am I correct in understanding that we should use Lean 3 (rather than Lean 4)? And
https://leanprover-community.github.io/undergrad_todo.html
is the right place to look for potential project ideas? Anything else I should be aware of or think about?

[Kevin Buzzard]

Right now the community is in a transition period, so your question is a little difficult to answer. I would say that the big advantage of Lean 3 over Lean 4 is that there are more learning resources, and the big advantage of Lean 4 over Lean 3 is that by the end of 2023 Lean 3 will be dead as the transition becomes complete.

I would say that the undergraduate todo list is not a great place to look without some discussions with the community. The problem with that list is that it does not do a good job of explaining that some things are on that list because the community wants them done in a specific way, and it may need a Lean expert to do them. Also targetting mathlib is really complicated right now again because of the ongoing porting process. This is a temporary issue, but there is also a more long-term issue that in general students tend to want to work on projects for just one summer and then quit at a certain skill level, whereas contributing to mathlib requires what one might call "expert level code", and many students I supervise never reach expert level in the 8 or so weeks I work with them, and then when the project is over they don't go back to it. This makes contributing to mathlib almost impossible for these people.

I would say that you would be better off making a project which depends on mathlib (either 3 or 4, depending on how brave you are) and then just formalising what the heck you want, and who cares if it's in mathlib or not. I've supervised plenty of projects formalising stuff which is already in mathlib; students who don't know much about Lean when they begin will probably find that by the end of the summer many of the proofs in mathlib are still incomprehensible, but that they can also write their own proofs of things (possibly even things which are in mathlib) which are much easier to read. Mathlib is written in a rather obfuscated style, for better or worse.

[Eric Wieser]

whereas contributing to mathlib requires what one might call "expert level code", and many students I supervise never reach expert level in the 8 or so weeks I work with them, and then when the project is over they don't go back to it.

Note that this isn't necessarily an argument against _trying_ to contribute to mathlib. Sometimes these abandoned PRs contain useful results that someone else needs, and then that someone else does the cleanup the students never got around to

[Matthew Ballard]

Hi Colleen. If you want to play it safe, then Lean 3 is a good choice. But your students may naturally be pulled toward Lean 4 given the existing momentum. If using Lean 4 is an option, use of Mathlib 3 or Mathlib 4 can depend pretty strongly on the project itself and which projects are in focus. For example, most of Combinatorics has been ported (or is almost there) whereas Analysis is about 1/3 ported. You can poke around at https://leanprover-community.github.io/mathlib-port-status/ to see which files have made it into ML4 so far.