Zulip Chat Archive

Stream: new members

Topic: OrgPage (a selfstudy material) for Lean


Martin Dvořák (Dec 09 2021 at 09:53):

Hello!

I am a new Lean user. In order to learn Lean more effectively, I use OrgPad. I gradually create this OrgPage (a selfstudy material):
https://orgpad.com/s/ZBGjrzoGIBb

I am posting it here for two reasons:
1) If you spot any mistake, please, let me know! I will be thankful if you help me correct mistakes I made.
2) Feel free to use my OrgPage for your selfstudy as well.

Huỳnh Trần Khanh (Dec 09 2021 at 11:49):

well, I'm pretty sure mathlib contributors have done an immense amount of work as well... probably unfair to list only 3 people as VIPs :stuck_out_tongue:

Huỳnh Trần Khanh (Dec 09 2021 at 11:50):

I'd say the whole Lean "movement" is a large scale collaboration effort and it doesn't have any "leaders" :joy:

Martin Dvořák (Dec 09 2021 at 11:50):

Good points, thanks!

Kevin Buzzard (Dec 09 2021 at 11:51):

I think that I am often mistaken as some kind of leader, because I go around doing a lot of promotion of the software; however I am not even a maintainer of the maths library!

Kevin Buzzard (Dec 09 2021 at 11:58):

I think that there are even some people in the community who are uncomfortable with the fact that I am somehow deemed a "leader" -- mathlib is even occasionally referred to "my library", something which couldn't be further from the truth and which we're doing our best to stamp out. Massot in particular is often quick to guide me to such inaccuracies and I do my best to fix them.

Kevin Buzzard (Dec 09 2021 at 12:01):

It is undoubtedly true that some of the projects I've been involved in have resulted in media coverage, and I've given a lot of talks in mathematics departments about mathlib so I am inevitably associated with the library by many mathematicians. But I have certainly never wanted to be a leader, not least because I couldn't organise myself out of a paper bag.

Martin Dvořák (Dec 09 2021 at 13:07):

OK. If I delete the small section called "Community", will you then pay attention to the rest of the document instead?

Huỳnh Trần Khanh (Dec 09 2021 at 13:25):

i think aside from that issue your document is pretty solid lol but like there are quite a few ??? in your document, so maybe it's a good idea to post them as questions here?

Martin Dvořák (Dec 09 2021 at 13:45):

I felt like I hadn't put enough effort into figuring it out myself. I will ask these questions later if those question marks stay there.

Martin Dvořák (Dec 09 2021 at 13:46):

I am more worried about mistakes in places where I don't think I have a mistake.


Last updated: Dec 20 2023 at 11:08 UTC