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