Zulip Chat Archive

Stream: new members

Topic: introduction ilmu


view this post on Zulip ilmu (Apr 02 2020 at 20:27):

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 :)

view this post on Zulip Mario Carneiro (Apr 02 2020 at 20:32):

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

view this post on Zulip ilmu (Apr 02 2020 at 20:34):

Cool, I'll start with this.

view this post on Zulip Mario Carneiro (Apr 02 2020 at 20:36):

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)

view this post on Zulip Mario Carneiro (Apr 02 2020 at 20:36):

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

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 21:21):

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

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 21:21):

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

view this post on Zulip ilmu (Apr 03 2020 at 00:23):

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?

view this post on Zulip ilmu (Apr 03 2020 at 00:24):

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

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

view this post on Zulip ilmu (Apr 03 2020 at 00:26):

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).

view this post on Zulip ilmu (Apr 03 2020 at 00:59):

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) :

view this post on Zulip ilmu (Apr 03 2020 at 01:10):

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

view this post on Zulip ilmu (Apr 03 2020 at 01:10):

Good enough, you guys are awesome (y)

view this post on Zulip Andrew Ashworth (Apr 03 2020 at 01:25):

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

view this post on Zulip ilmu (Apr 03 2020 at 01:31):

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

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

view this post on Zulip Andrew Ashworth (Apr 03 2020 at 01:47):

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

view this post on Zulip Donald Sebastian Leung (Apr 03 2020 at 03:45):

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.

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 07:21):

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

view this post on Zulip Marc Huisinga (Apr 03 2020 at 10:40):

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.

view this post on Zulip ilmu (Apr 03 2020 at 21:04):

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


Last updated: May 13 2021 at 21:12 UTC