Advertising Lean

Stream: general

[Trebor Huang]

I'm writing a 50 page essay on type theory, in which I would like to introduce Lean with about 1-2 pages of text. I would like this to grab the attention of mathematicians (or university math professors), but not get into too much detail. What are the tried-and-worked things that I can do? For instance, What are some good showcases, interesting projects or some stories that I can tell?

[Patrick Massot]

50 pages on type theory is "not get into too much detail"??

[Kevin Buzzard]

Why do you think that a university maths professor (who has probably never heard of type theory and thinks it's a weird computer science thing) is going to look at a 50 page essay on type theory? When I talk about lean I tend to talk about the mathematical successes but never mention type theory at all!

Highlights this year off the top of my head include: completion of the LTE (no paper as yet AFAIK), completion of the sphere eversion project (paper by Patrick Oliver and Floris just accepted) and Bhavik Mehta and Thomas Bloom formalising Bloom's resolution of an old Erdos conjecture before the paper got refereed.

[Trebor Huang]

It's mandatory coursework, and I can choose any subject, so might as well choose one that I'm more interested in. I would also like an opportunity to collect my thoughts on the subject and write something that people speaking my language instead of English would benefit from.
I'm focusing on the history part (like starting from Russell), so I would leave just a small part for Lean. I hope Lean is making history, and not being history anytime soon!

[Winston Yin]

Though I’m not a university maths professor, I’d love to give it a read when you’re finished with it. I’m an editor of Wikipedia and wouldn’t mind buffing up its article on Lean in English and Chinese

[Andre Graubner (安德)]

I'd also be more than interested in reading this once it's done!

[Trebor Huang]

I put it online here for preview. It will be ready in a few weeks, probably. I hope it is okay to ping @Andre Graubner (安德) @Winston Yin

[Andre Graubner (安德)]

Thanks this is great, I'll check it out. Time to learn some type theoretical terms in Chinese I guess :grinning_face_with_smiling_eyes:

[Martin Dvořák]

I also started advertising Lean:
https://youtu.be/6cmcZl-0x-0

Each of us could maybe make a video about Lean in their mother tongue, to reach a wider audience.
I am going to do more in the future.

[Bulhwi Cha]

I'll try to make introductory videos about Lean in Korean in the future, but it'll take quite a lot of time.

[Winston Yin (尹維晨)]

We can make it a starting goal to at least beef up the English Wikipedia article on Lean. It doesn't even mention LTE or the history of various versions!

[Martin Dvořák]

What is LTE?

[Hanting Zhang]

it's the Liquid Tensor Experiment

[Niels Voss]

I think the Wikipedia article should at least mention mathlib somewhere

[Winston Yin (尹維晨)]

If somebody wants to dump links to articles on Lean (ideally not written by Lean people) here, I can take a crack at the wiki article.

[Alex J. Best]

We have some examples of this collected in the #general > Lean in the wild thread

[Floris van Doorn]

Here are some links of articles in nature and quanta:
https://www.nature.com/articles/d41586-021-01627-2
https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/
https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/
https://www.quantamagazine.org/can-computers-be-mathematicians-20220629/
it is also mentioned in
https://www.quantamagazine.org/the-year-in-math-and-computer-science-20201223

Maybe we should collect these centrally somewhere ("Lean in the press" or something)?

[Niels Voss]

The YouTube video associated with the last link you posted is actually the way I found out about Lean in the first place

[Kevin Buzzard]

My partner still hasn't forgiven me for not removing the dishcloth from the back of the chair in that video

[Martin Dvořák]

I think we completely overlook trends among young people, which is why we don't have almost any people under the age of 15 in our community. For example, this is how the .NET community embraces current trends on TikTok:
https://www.tiktok.com/@dotnetdevelopers
I'm not saying their PR is perfect, but they give it a good try and they stir some reactions.
Overall, I'd say that internet memes are a powerful tool for outreach, and we don't use it enough.

[Shreyas Srinivas]

We'd be lucky if a non trivial number of under 15s can be interested in math enough to care about proofs in the first place, let alone lean

[Martin Dvořák]

In my country, many people under the age of 15 are interested in math competitions. After the age of 15, anything mathematical becomes a very niche hobby.

[Violeta Hernández]

I feel like the prerequisites for entry are just too high to have any sizable young population. I'm 22 and I still have no idea what half of Mathlib is about :sweat_smile:

[Violeta Hernández]

Getting more current or former math competitors to formalize IMO problems might be a way to hook them in, though

[Daniel Weber]

From my discussions with people (including some IMO competitors) about Lean I found that their main point of contention is why formalizing proofs is good, and I'm not sure how to argue for that—I do it because I find it fun

[Paige Thomas]

As a response to why formalizing proofs is good:
One reason I have is because I can be sure the proof is correct, and not rely on trusting or needing an expert to check it for me, other than maybe that the definitions and theorem statements are right. I find it a good way to learn a new subject. And someday I hope to understand it enough to improve my software code with it.

[Paige Thomas]

But I'm definitely past that age range by quite a margin.

[Brandon Harad]

Martin Dvořák said:

I think we completely overlook trends among young people, which is why we don't have almost any people under the age of 15 in our community. For example, this is how the .NET community embraces current trends on TikTok:
https://www.tiktok.com/@dotnetdevelopers
I'm not saying their PR is perfect, but they give it a good try and they stir some reactions.
Overall, I'd say that internet memes are a powerful tool for outreach, and we don't use it enough.

If it is at all helpful, I am simultaneously under 15, hopefully part of the Lean community, and not a part of any competition math teams.

[Brandon Harad]

I got into Lean because of NNG4, and because I was looking for a way to combine joint interests of math and computer science

[Brandon Harad]

In my opinion, social media would reach essentially none of the demographic predisposed to liking Lean

[Brandon Harad]

It certainly wouldn't have reached me

[Violeta Hernández]

Daniel Weber said:

From my discussions with people (including some IMO competitors) about Lean I found that their main point of contention is why formalizing proofs is good, and I'm not sure how to argue for that—I do it because I find it fun

Told my roommate (a former IMO competitor) about how someone had formalized a certain IMO problem on Lean and his response was "why would you do that if they already have official solutions"

[Martin Dvořák]

I'd reply "to make sure I understand the solution fully".

[Kevin Buzzard]

If I wanted to do that I'd just read the official solution. I'd reply "to train the systems so that ultimately they'll help humans do new maths"

[Bulhwi Cha]

Most humans would like to see such systems, but it's hard to persuade these people to participate in training the systems.

[Martin Dvořák]

Violeta Hernández said:

I feel like the prerequisites for entry are just too high to have any sizable young population. I'm 22 and I still have no idea what half of Mathlib is about :sweat_smile:

You know that understanding Mathlib is not a prerequisite to enjoying Lean, right?

A ten-year-old will engage with Lean in a way that's accessible for a ten-year-old.

[Violeta Hernández]

Yeah, I guess "using Lean" and "doing Mathilb PRs" are somewhat different goals.

[Violeta Hernández]

(but the first does often lead to the latter)

[Bulhwi Cha]

I'm teaching Lean to some Koreans and I don't think they're interested in contributing to Mathlib at the moment. When my mentorship program ends, they'll decide whether to continue learning about proof assistants like Lean.

[Luigi Massacci]

Martin Dvořák said:

A ten-year-old will engage with Lean in a way that's accessible for a ten-year-old.

Lean is not a language that is well suited for teaching programming to ten year olds

[Luigi Massacci]

There are Python for Kids books, but I've yet to hear of System Verilog for Kids and lean is closer to the second than the first

[Luigi Massacci]

(if only because of the lack of documentation)

[Ruben Van de Velde]

Let's say that lean can be many things to many different people

[Luigi Massacci]

Yes, but for the topic of children under 15 specifically, it's worth pointing out that in most of the world they are not even allowed to make a Zulip account (according to Zulip's own rules), so given that the current learning process for lean is heavily Zulip based, it would probably not be the best

[Kevin Buzzard]

In mathematics, Lean's strength is proving rather than calculating, and in the UK at least a 15 year old has seen essentially no proving and just lots and lots of calculating, so you'd be better off showing them a CAS than Lean.

[Shreyas Srinivas]

In India, I would say there is a case to be made for lean if you can do Euclidean geometry properly in it. Euclidean geometry is taught from around 13 and by 15, students are supposed to be able to come up with proofs and constructions. By doing euclidean geometry properly, I mean express constructions and see them in the infoview, and visualise angle or length equalities as one proves them.

[Shreyas Srinivas]

That being said, it is far fetched to expect kids to learn a whole PL and program in it

[Shreyas Srinivas]

So this idea is still a castle in a cloud

[Violeta Hernández]

Euclidean geometry in Mathlib is far, far beyond the reach of a 15 year old... I spent quite a bit trying to figure out how angles were even defined just a few hours ago.

[Violeta Hernández]

You'd probably need to build a separate formalization more akin to that of synthetic Euclidean geometry first

[Kevin Buzzard]

Yes I absolutely agree that there is a genuine possibility for a really nice Euclidean geometry game which is accessible to 15 year olds. I give talks at schools and I only ever do NNG material (which can't really be presented to 15 year olds in my country because they've not seen induction, so I just do 2+2=4). I think that one of the possibly several minimum prerequisites for getting 15 year olds to do geometry in lean is to get the infoview displaying lines and triangles and circles etc, and some clickable interface. The toy example I have in mind is a visually comprehensible proof that angle at centre equals twice angle at circumference via the usual argument with isosceles triangles

[Patrick Massot]

Luigi Massacci said:

Yes, but for the topic of children under 15 specifically, it's worth pointing out that in most of the world they are not even allowed to make a Zulip account (according to Zulip's own rules), so given that the current learning process for lean is heavily Zulip based, it would probably not be the best

Of course Zulip is very useful, but there are still people who learn Lean without ever showing up on this Zulip. I would be curious to know what you think is really hard to learn without Zulip. I have some ideas about what you may answer, but I’m still interested in your opinion (and we will be able to discuss it tomorrow).

[mars0i]

I learned from a recent podcast that (iirc) @Sebastian Ullrich got into Haskell when he was a teenager. No doubt he's unusual, but the point of this discussion isn't to figure out how to get all teenagers interested in Lean. (What a world that would be!) Dependently typed languages are harder than Haskell, but Lean may be easier in some respects than Idris or Agda, because of tactics. So maybe other Sebastian Ullrich's could learn Lean to do the sort of programming they're interested in, even if they're not necessarily keen on theorem proving.

[Daniel Weber]

Perhaps we can advertise it to parents who will then teach it to their children

[Martin Dvořák]

Luigi Massacci said:

Yes, but for the topic of children under 15 specifically, it's worth pointing out that in most of the world they are not even allowed to make a Zulip account (according to Zulip's own rules), so given that the current learning process for lean is heavily Zulip based, it would probably not be the best

I didn't know about this restriction. Thanks for pointing out!

[Martin Dvořák]

Kevin Buzzard said:

In mathematics, Lean's strength is proving rather than calculating, and in the UK at least a 15 year old has seen essentially no proving and just lots and lots of calculating, so you'd be better off showing them a CAS than Lean.

There are some ways how a motivated ten-year-old can engage with Lean.
@David Renshaw shows several accessible examples in his video:
https://youtu.be/KuxFWwwlEtc?si=X_Zub9wXRqV6X4EH
From there, anybody can go to interactive theorem proving, even without a prior exposition to mathematical proofs, because the child will have learnt to work with the Infoview, which gives an intuition for "what the rules of the game are" even if the child doesn't know why the game has such rules (e.g. why constructor sometimes opens several goals).

[Martin Dvořák]

That said, a more likely way for a ten-year-old to engage with Lean is to learn some basic programming — first hello world, then a program that asks the user for their name and insults the user, etc — children love this stuff.

[Shreyas Srinivas]

As I recall there used to be a lean 3 Euclidean geometry game. Maybe a lean4 version could augment the game with proof widgets

[Shreyas Srinivas]

@Will Crichton : Would this be of interest for your project for your cognitive engineering lab? Building a nice visual way to understand euclidean geometry proofs?

[Joseph Myers]

Note that accessibility of a sequence of steps in a geometry argument has essentially nothing to do with the axiomatic foundations used. Whatever definitions and lemmas you'd like to use for reasoning could be set up (if correct) based on affine spaces for real inner product spaces just as they could on any other axiomatic basis. (It's very likely that many such lemmas are indeed missing in mathlib at present. Also that in some cases the statements convenient for teaching might be less appropriate for mathlib than some other more general version. Also that tactics would help for the many cases of nondegeneracy conditions that are obvious to humans from looking at a diagram - though we probably don't have enough examples of geometry arguments in Lean yet to identify what such tactics should look like.)

[Kevin Buzzard]

I agree, and the issue right now with me pushing forward with some appropriate lemmas and examples is that I'm not motivated to do it until we have circles and triangles visible in the infoview.

[Bulhwi Cha]

How do we visualize these figures in the infoview?

[Daniel Weber]

We can try to figure out the hypotheses, numerically solve/approximate them to find a generic solution, and then draw it

[Kevin Buzzard]

The example I usually keep in mind is "angle at centre equals twice angle at circumference". I'd like the infoview to have at the very least a picture of the diagram and a statement of what we're trying to prove, and ideally the picture won't "jump around" as we e.g. draw the diameter through the circumference angle point and centre angle point and then do the calc angle chase. Getting it working seems to me to be a nontrivial endeavour (and I wouldn't have a clue how to start with the visualisation stuff), but as I say the motivation is that I can see it working with 15 year olds. In the UK system 15 year olds are shown proofs of the "7 circle theorems" and "x triangle theorems" for some value of x, and if we could do those in Lean and then also flag up the issues between angles and directed angles I think it could be turned into something interesting.

[Daniel Weber]

Daniel Weber said:

We can try to figure out the hypotheses, numerically solve/approximate them to find a generic solution, and then draw it

This shouldn't jump around unless you do case splits, right? And we can also warn if the goal doesn't seem true. One potential problem is having inconsistent hypotheses, but I don't think that's common in geometry

[Patrick Massot]

@Wojciech Nawrocki will probably have comments here.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kevin Buzzard said:

I agree, and the issue right now with me pushing forward with some appropriate lemmas and examples is that I'm not motivated to do it until we have circles and triangles visible in the infoview.

I believe you would have seen the Euclidean demo. It doesn't show triangles (partly because they're not a primitive of the axiomatization) but does show lines which visually form triangles. What is missing from this kind of demo relative to what you'd like? (It does jump around a lot since the randomness is re-seeded every time the hypotheses change, but I'm assuming it's not just that.)

[Kevin Buzzard]

@Wojciech Nawrocki Thanks! I don't remember ever seeing this and am currently trying to work out what this file does. I've cloned proofwidgets4 and I've opened the file; there's a "place your cursor here" on line 189 which displays a line with 3 points on it, and if I move around the proof it keeps printing the same line. There's also a "place your cursor below" on line 316 where I see two points (but have no idea what to do next and not really any idea about what to read to find out). Maybe the idea is that I read the code and try proving the theorem and see what the diagram does? Most of the file is unfortunately incomprehensible to me.

But my conclusion is that instead of whining that I'm not going to prove angle at centre is twice angle at circumference because there are no tools to display what I want to explain, I should just do it anyway (because I was wrong), so it sounds like the ball is back in my court (it might stay there for a while, there is a lot of stuff I want to get off my plate by 1st Oct).

[Patrick Massot]

@Kevin Buzzard you can watch https://www.youtube.com/watch?v=9yG0-CoHDHQ. Skip the first ten minutes if you are really in a hurry.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Thanks for trying it out @Kevin Buzzard! I added some clarifying comments to the demo in this commit. Do these help?

[Kevin Buzzard]

It is ridiculous how forgetful I am. Yes I was at Wojciech's talk. I should try and remember that the ball is now in my court. I need to focus on FLT right now though. If someone else wants to knock up a demo proving the seven circle theorems in Lean (or even just one or two of them!), that would be great! Otherwise I'll get to it at some point.

[Patrick Massot]

Note how I nicely did not point out that you attended that talk, I only suggested that you watch it.

[Kevin Buzzard]

I introduced it :-)