OrgPage (a selfstudy material) for Lean

Stream: new members

[Martin Dvořák]

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]

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]

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

[Martin Dvořák]

Good points, thanks!

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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