Advertising a course

Stream: Lean for teaching

[Monica Omar]

What's a good and eye-grabbing way of advertising an introductory course on Lean and formalising mathematics in lean to PhD students? What has worked well in the past?

[Martin Dvořák]

I can only hint what did NOT work well for me:
[deleted on request]

[Monica Omar]

can't believe you've actually done that hahaha

[Martin Dvořák]

Well, my friends were mocking me for being a Lean user for so long that I decided to own it...

[Monica Omar]

how did the school let you do that though?! it's subliminally advertising drugs to students

[Martin Dvořák]

Well, my online Lean course featuring our fox mascots has been much more popular:
image.png
It is the one I mention here:
https://leanprover-community.github.io/teaching/courses.html

[Monica Omar]

awww that's adorable! but what does that have to do with Lean?

[Eric Wieser]

is the link I think

[Riccardo Brasca]

I don't think mathlib is the largest library of formal proof, isn't Isabelle's one bigger?

[Jireh Loreaux]

I think Riccardo is correct.

[Monica Omar]

think they meant to say the largest library of formal pure abstract mathematical proof

[Jireh Loreaux]

How is that different?

[Martin Dvořák]

Riccardo Brasca said:

I don't think mathlib is the largest library of formal proof, isn't Isabelle's one bigger?

Maybe I was wrong! I only checked Mizar; it had less than 10^5 theorems, so I concluded that Mathlib was probably the largest.

[Martin Dvořák]

Martin Dvořák said:

Well, my friends were mocking me for being a Lean user for so long that I decided to own it...

To be fair, my friends were also making fun of me for having played with Coq. Hence I conclude that no name is completely free of problems.

[Eric Wieser]

Riccardo Brasca said:

I don't think mathlib is the largest library of formal proof, isn't Isabelle's one bigger?

I think the more plausible claim is probably that mathlib is the "largest interconnected library of formal proof", but that's much harder to quantify

[Martin Dvořák]

To be honest, the simplest correction will be to admit that I was simply wrong.

[Martin Dvořák]

Another issue you might rightfully criticize me for is that I used something that resembles the Lean logo but isn't the official Lean logo.

[Riccardo Brasca]

I just mean that usually it is better to say things like "one of the largest" or similar :)

[Kevin Buzzard]

Isabelle's AFP might be bigger than mathlib, but a lot of what is in AFP is quite far from what I would call mathematics -- it is far more CS-oriented.

[Martin Dvořák]

Riccardo Brasca said:

I just mean that usually it is better to say things like "one of the largest" or similar :)

I agree with you, but I feel that saying "Mathlib is one of the largest" is a terrible understatement.

[Mario Carneiro]

it's not though

[Mario Carneiro]

There are other very large libraries out there

[Martin Dvořák]

Sorry for the OT but...
How is it with Isabelle's AFP or Mizar's MML?
Can you download and import the entire library somehow?
Are the "papers" mutually compatible?

[Mario Carneiro]

The MML yes, AFP I'm not sure but I think so

[Mario Carneiro]

it would be pretty weird to import the whole AFP

[Mario Carneiro]

that's kind of like doing apt install <everything>

[Martin Dvořák]

Ah, it's cool that MML maintainers managed to keep the library consistent for so many decades! I just learnt something new.

[Martin Dvořák]

Mario Carneiro said:

that's kind of like doing apt install <everything>

I don't do import Mathlib either, but I find it very important that it can be done in principle (and many Lean users appreciate that it can be done in practice as well, but...).

[Shreyas Srinivas]

Mario Carneiro said:

There are other very large libraries out there

not sure if this is the right channel for this question, but it seems like a natural follow up. It is also probably a phenomenon worth understanding in the history of theorem provers: why do we keep reinventing formal math in new theorem provers? I kinda get that some provers were experimenting with different approaches at the foundational levels and maybe ways to embed proof automation, but it does seem wasteful effort to redo the math part again and again. For example, what was lean doing differently that it made sense to not do it in Coq? I read Sebastian's thesis (specifically motivations in Page 9), but I don't know why these goals were unachievable in existing provers. Why did current mathlib devs choose a new theorem prover over something well established like Isabelle or Mizar? I got a partial answer to the last one from Kevin about post-Grothendieck math and simple type theory, but the explanation doesn't translate to Coq. I also recall an article that Kevin tried Coq and then switched to Lean. But all this suggests is that one or two mathematicians got the ball rolling based on their experiences and it snowballed. It doesn't explain the "why it didnt happen before or differently"

[Martin Dvořák]

For me personally, it was an aesthetic preference. Coq is ugly syntax. Lean is beautiful.

[Kevin Buzzard]

The problem with the community, as I percieved it, in 2017 was precisely that it was not doing the mathematics which we teach to the undergraduates in mathematics departments across the world! This is because at that time the area was dominated by computer scientists who typically had no feeling for what was actually important to mathematicians (for example there was a big emphasis on constructivism, which has not been taught in mathematics departments for 100 years). The computer scientists would pick and choose from the curriculum or do mathematics which was relevant to whatever theory groups were studying or whatever. There was no coherent development of an undergraduate mathematics curriculum in any theorem prover before the mathlib effort. I am pretty sure that it could have been done in pretty much any theorem prover, it could well have just been chance that it was done in Lean.

[Monica Omar]

exactly ^

[Monica Omar]

Also, when I was an undergraduate trying to learn Coq and others on my own, I found it pretty difficult. Lean was far easier for me personally.

[Monica Omar]

Martin Dvořák said:

For me personally, it was an aesthetic preference. Coq is ugly syntax. Lean is beautiful.

As Martin said, Lean has a nicer and easier syntax

[Monica Omar]

Although, I feel Lean3 has a nicer syntax than Lean4, in my opinion :eyes:

[Martin Dvořák]

Monica Omar said:

Also, when I was an undergraduate trying to learn Coq and others on my own, I found it pretty difficult. Lean was far easier for me personally.

Also for me, a huge part of Lean's appeal in the beginning was its accessibility via the NNG.

[Monica Omar]

There you go. Gamifying it made it far more appealing.

[Martin Dvořák]

Kevin Buzzard said:

I am pretty sure that it could have been done in pretty much any theorem prover, it could well have just been chance that it was done in Lean.

Then I am really thankful for the fluke that Lean happened to be the language!

[Monica Omar]

Monica Omar said:

There you go. Gamifying it made it far more appealing.

I guess that's what we should advertise in the course advert then? That we can gamify things in mathematics and make it more appealing? or something along those lines?

[Johan Commelin]

I think it's not just chance. Lean offers many little quality-of-life improvements over other systems. Even if the underlying foundations are basically the same as in Coq, that is only a tiny aspect of the story. To name a somewhat trivial example: back in 2017, Coq didn't have a VScode extension. It's sounds silly, but I think those things matter.

[Martin Dvořák]

If they are very advanced math students, printing some posts by Terence Tao from his Mathstodon page will probably appeal to them.

[Monica Omar]

Martin Dvořák said:

If they are very advanced math students, printing some posts by Terence Tao from his Mathstodon page will probably appeal to them.

I wouldn't say very advanced lol, just advanced enough. But, that's smart!

[Shreyas Srinivas]

Kevin Buzzard said:

The problem with the community, as I percieved it, in 2017 was precisely that it was not doing the mathematics which we teach to the undergraduates in mathematics departments across the world! This is because at that time the area was dominated by computer scientists who typically had no feeling for what was actually important to mathematicians (for example there was a big emphasis on constructivism

Was this also the case for Isabelle? I thought their HOL was just classical stuff

[Mario Carneiro]

To name a somewhat trivial example: back in 2017, Coq didn't have a VScode extension. It's sounds silly, but I think those things matter.

Note that Coq's vscode extensions (VsCoq 1 & 2, coq-lsp) still don't have go-to-definition across files, it seems to be vaguely in the "open research question" camp

[Mario Carneiro]

Shreyas Srinivas said:

Kevin Buzzard said:

The problem with the community, as I percieved it, in 2017 was precisely that it was not doing the mathematics which we teach to the undergraduates in mathematics departments across the world! This is because at that time the area was dominated by computer scientists who typically had no feeling for what was actually important to mathematicians (for example there was a big emphasis on constructivism

Was this also the case for Isabelle? I thought their HOL was just classical stuff

Isabelle has never been constructivist, this is a Coq / Agda thing mostly. Isabelle, Mizar, Metamath, HOL4, HOL light are all classical

[Monica Omar]

Also, Lean's Mathlib has awesome documentation, where it's easy-to-read. Not so sure about the rest?

[Monica Omar]

Let's be honest tho, if Kevin and other mathematicians didn't go for Lean at the time, then Lean wouldn't be this big right now.

[Mario Carneiro]

Shreyas Srinivas said:

Why did current mathlib devs choose a new theorem prover over something well established like Isabelle or Mizar?

I think this is the wrong way to look at it. When it comes to language use and evolution, society as a whole is always exploring all paths to some extent. There are people working in existing languages, and there are people trying something new, and then there is an evolutionary selection process that builds on itself to determine what actually takes hold in the large scale. So there are some small nudges here and there due to the language design itself, leading some influential people to have a preference in one direction, leading others to join in and then after a few more doubling iterations the new language becomes another contender next to the old guard.

[Monica Omar]

^ kind of like natural language

[Kevin Buzzard]

The thing about the HOL languages is I suspect that they're not really suitable for a big chunk of post 1950s mathematics (all the homological algebra / category theory stuff). Of course you can do it, but it might be super-painful. On the other hand they are probably better at automation (because they have a simpler type theory), at least historically, so there is a certain amount of swings and roundabouts here.

[Mario Carneiro]

Of course you can do it, but it might be super-painful.

Keep in mind that what this actually means is that the tooling isn't there, this isn't an argument for one foundation vs another

[Mario Carneiro]

HOL is also not particularly suited to direct ATP applications. People have tried to do so, but the SOTA is all FOL not HOL. So this is really another tooling issue

[Shreyas Srinivas]

Mario Carneiro said:

Shreyas Srinivas said:

Why did current mathlib devs choose a new theorem prover over something well established like Isabelle or Mizar?

I think this is the wrong way to look at it. When it comes to language use and evolution, society as a whole is always exploring all paths to some extent. There are people working in existing languages, and there are people trying something new, and then there is an evolutionary selection process that builds on itself to determine what actually takes hold in the large scale. So there are some small nudges here and there due to the language design itself, leading some influential people to have a preference in one direction, leading others to join in and then after a few more doubling iterations the new language becomes another contender next to the old guard.

As an overarching narrative this makes sense. But it needs some details to be fleshed out. Much of Lean's mathlib community comes from academia which has a publish or perish incentive structure. Formalisation would have been a fairly risky endeavour for an academic mathematician (funding, tenure eval, positions etc). Further I can't imagine that it would be helpful to say "we verified a trivial piece of undergrad math" as opposed to some frontier results. Lean would have (at that time, say 2017) compounded this with the uncertainties of a new and untried system.

[Mario Carneiro]

Much of Lean's mathlib community comes from academia which has a publish or perish incentive structure. Formalisation would have been a fairly risky endeavour for an academic mathematician (funding, tenure eval, positions etc).

Seems like you have it backwards: Academia likes new things, so working on a new system is encouraged if you can describe some unique benefits as a result. That's why if you watch a CS conference you will see 10 never before seen languages presented, because the language is the vehicle for a new idea

[Kevin Buzzard]

Further I can't imagine that it would be helpful to say "we verified a trivial piece of undergrad math"

That's why I spent three years training undergraduates to do this.

[Mario Carneiro]

However, this is clearly not an attractive proposition for mathematics departments: formalization circa 2017 is mostly dead math, so it's not clear why you would want to invest in it.

[Mario Carneiro]

That's why formalization circa 2017 is CS dominated, it's a new tech validating old math

[Mario Carneiro]

The actual academic mathematicians only started flowing in in the past 2-3 years, once we got past the boring stuff built by people like me (with a hybrid CS/Math background) and undergraduates (who aren't yet at the point of risking their careers). Before then all the mathematicians involved were definitely taking a risk

[Mario Carneiro]

Even now it's somewhat risky to get heavily involved in formalization as a pure mathematician

[Kevin Buzzard]

For example I could afford to take that risk because when my line manager asked me where all my brilliant new number theory papers were I just replied that for technical reasons there were not going to be any such papers in the foreseeable future, and because I am an established professor and a popular teacher my line manager reluctantly agreed that this was OK. But I was/am in an extremely privileged position.

[Shreyas Srinivas]

Attracting undergrads takes decent UX. Makes sense. As long as only PhDs and above (in the academic career ladder) are doing formalization

1. there would be a disincentive to work on basic stuff. Even in CS, I don't know of many pure math formalization projects targeting undergrad math.
2. Once they are committed to formalization, they would be willing to swallow the bitter pill of poor UX to get the job done. It happened to me in a different context and I have seen it happen to people in formalization heavy areas like PL

[Shreyas Srinivas]

"Get them early" and all that

[Jireh Loreaux]

Likewise, I'm in a department with modest research expectations, and after I published enough to get tenure, I was able to spend two years not publishing much to focus on Lean.

[Alok Singh]

Martin Dvořák said:

I can only hint what did NOT work well for me:
image.png

This is what the whole advertisement looked like:
image.png

LMFAO

[Monica Omar]

Jireh Loreaux said:

Likewise, I'm in a department with modest research expectations, and after I published enough to get tenure, I was able to spend two years not publishing much to focus on Lean.

that's deffo the smart way to do it

I'm a PhD, and I focus on Lean to focus on my research, which is definitely such a backwards way of doing research and a big waste of time in everyone's opinion. Think of something -> prove it on paper -> Lean it for week(s) -> move on

[Apurva Nakade]

By weeks do you mean months?

[Monica Omar]

sometimes haha. I guess it depends

[Martin Dvořák]

I mean years.

[Andrés Goens]

Martin Dvořák said:

I can only hint what did NOT work well for me:
image.png

This is what the whole advertisement looked like:
image.png

this reminds me a lot of a slide by @Orestis Melkonian

[Andrés Goens]

(from this talk)