introduction ilmu

Stream: new members

[ilmu]

Hi, I'm new here, I'm Ilmu. I've got a BS in math and am currently applying for a MS.

I'm sorry to ask before I finish reading the resources that you already point to (like the mathlib paper) but what would be the recommended way to read the library / try to reimplement parts of it / use it to solve exercises (like a munkres topology course).

Part of the reason I ask is an analogy with haskell; if Lean is to Mathematics what Haskell is to Programming then mathlib is like prelude, and the best haskell tutorial I ever did was to reimplement prelude (fp-course from data61). Has anyone tried to make some exercises or introductory material along these lines?

Thank you in advance :)

[Mario Carneiro]

The Natural Number Game sounds pretty similar to this, although it is in a controlled environment so that the proving is more game-like

[ilmu]

Cool, I'll start with this.

[Mario Carneiro]

If you want to learn how to read mathlib itself, you could pick a simple file like data.list.basic and try to follow the definitions and proofs. If you don't know enough syntax for that yet consult TPIL (theorem proving in lean)

[Mario Carneiro]

it's a steeper learning curve but worth it especially if you intend to eventually contribute to mathlib

[Kevin Buzzard]

I aim to get some tutorials up within the next week or two implementing the basics of eg group theory or equivalence relations

[Kevin Buzzard]

I still don't know whether I should put them in the tutorial project or just post them here in #new members

[ilmu]

Hey so I was almost finished with the natural number game (level 6 of advanced addition and I'd finished the other side as well) when the lean guy froze and it looks like I'll have to refresh but if I do I think I'll lose my state.. is there a cheatcode to open all the worlds?

[ilmu]

is this "the tutorial project" https://github.com/ImperialCollegeLondon/M40001_lean ?

or is it the natural number game or something completely different?

[ilmu]

anyway, also wanted to say: thank you Kevin for these great resources! and for resolving my analysis paralysis w.r.t. which of these tools was most suitable to invest my time in (Edward Kmett had already told me that Lean was the best but at the time they were in the middle of rewriting it and Coq was the only thing that had any learning resources so I ended up just procrastinating).

[ilmu]

Oh and btw, while the natural number game is simple enough to kind of just steamroll (but it is very educational nevertheless, perfect introduction!), anyway, I think the left column would be a super useful resource if it had wider scope and was independent (i.e. tactic cheatsheet).

The thing I needed to be able to do the exercise sheets in the M40001 repo was basically this kind of api reference for tactics ..and in general I think this is the most useful thing to have in any kind of programming ecosystem.

I ran into this problem when attempting to do some Coq exercises in the past, the author of the exercises had shown a few tactics which worked for the first few problems but then I got stuck and when I finally gave up and looked at the solutions, it turned out that suddenly you needed to know tactics that had never appeared before... this completely blew my morale and I pretty much decided Coq is stupid (which it is most definitely is not, but you know what I mean).

Lean is already miles easier to get started with (although agda is probably still easier than lean) but I foresee some difficulties, once I become intermediate, with keeping track of all the different tactics and finding out which options I have in a context.

I think these are especially good (but obviously it'll be somewhat differently organized in the lean context) :

• https://cljs.info/cheatsheet/
• https://hoogle.haskell.org/

[ilmu]

I guess this is it: https://leanprover-community.github.io/mathlib_docs/

[ilmu]

Good enough, you guys are awesome (y)

[Andrew Ashworth]

I feel like the most important thing, even more than tactics, is knowing how to understand Lean terms? Give a man a tactic, and you'll feed him for a day. Teach a man to understand the terms tactics construct, and you've avoided weeks of angst in the debugger

[ilmu]

aren't the terms just like normal functional programming though?

also wow the manual is superb, I'm more and more impressed!

[Andrew Ashworth]

Yes, they are. Ignore what I wrote : ) I did not see your background with functional programming

[Donald Sebastian Leung]

I ran into this problem when attempting to do some Coq exercises in the past, the author of the exercises had shown a few tactics which worked for the first few problems but then I got stuck and when I finally gave up and looked at the solutions, it turned out that suddenly you needed to know tactics that had never appeared before... this completely blew my morale and I pretty much decided Coq is stupid (which it is most definitely is not, but you know what I mean).

I'm sorry you had this experience with Coq. Which tutorial(s) were you following back then? For me, I was following Software Foundations and only encountered this problem once in the first 3 books of the series (never got around to trying the 4th). But even then, an online friend of mine later told me that (s)he was able to solve that particular problem using only the tactics taught up to that point, albeit in a slightly convoluted way.

[Kevin Buzzard]

There is an entire #teaching stream and any comments about resources that are missing or could be better would be definitely of interest there

[Marc Huisinga]

i'm sure you've seen it already, but https://leanprover.github.io/theorem_proving_in_lean/ is also a good introduction for those who are already somewhat familiar with functional programming. if you know a bit of coq or agda, much of it may not be new to you, so perhaps it can also serve as a reference manual for a good portion of the lean language itself.

[ilmu]

@Donald Sebastian Leung it was a (remote) summer school, I don't have the exercise sheet anymore, sorry.