Nate Glenn

Stream: new members

[Nathan Glenn]

Hi, total noob here. I'm a software engineer, not a mathematician, but I enjoy some recreational math and I thought Lean looked like a really fun avenue to explore. I'm from the US, but I live in Düsseldorf, Germany.

[Patrick Massot]

Welcome!

[Jalex Stark]

If the goal is exactly recreation,
I think the funnest part of Lean for a new user is filling in sorries. So I recommend the "game"s, tutorials, and Codewars :)

[Nathan Glenn]

Thanks for the suggestion! I've done most of the natural number game, and I'm just starting the tutorial now. I think the Codewars katas are maybe more intermediate? The very first kata is about finding a syntax error, and the errors shown on the website are not helpful for finding it.

[Patrick Massot]

I certainly hope the tutorials are much easier and much more interesting than codewars

[Jalex Stark]

which kata is about finding a syntax error? afaik they don't have a canonical order.
also, you should write code locally. It's not hard to install Lean and VSCode, and the experience of writing locally is significantly better than writing code on codewars. (and at least a little bit better than writing code in the community web editor, which is what e.g. the natural number game runs on.)

[Donald Sebastian Leung]

The very first kata is about finding a syntax error, and the errors shown on the website are not helpful for finding it.

Yeah, the entry kata to the site is rather designed for ordinary programming languages and doesn't fit Lean (or other theorem proving languages) so well. IMHO a more suitable introductory Lean kata would be Theorem proving hello world.

[Reid Barton]

I thought it was fine, but it is true that it tests a skill (basically, do you know how to write a definition) that won't come up again until you get to the point where you want to write auxiliary definitions in your kata solutions.

[Nathan Glenn]

@Jalex Stark this one: image.png . I guess it might not be about finding a syntax error, but that's what I thought when I read the instructions. Copying and pasting the code into VS code and solving it locally makes sense I guess, but I think it defeats the purpose of having katas on the CodeWars site, doesn't it? At that point, it seems like it would be better to migrate all of the katas into the tutorials.

[Jalex Stark]

ah yeah that first kata is not particularly friendly.
the thing that codewars did for me was to give me a list of problems that I'm supposed to solve mostly without help, as though i were an undergrad doing problem sets.

[Nathan Glenn]

Ah, makes sense

[Donald Sebastian Leung]

@Nathan Glenn About the lack of an interactive environment for Lean, Codewars currently supports over 50 different programming languages, probably more than any other recreational/educational/competitive OJ site you could find, so it is infeasible to support a full-fledged IDE for every language. As Jalex mentioned, you may wish to think of Codewars as a repository of Lean exercises of varying difficulty, contributed by the community, as opposed to a dedicated online tutorial. For getting up to speed with Lean as a complete beginner, I would still recommend proper tutorials and/or textbooks such as the NNG, TPIL and/or Patrick's tutorial.

[Nathan Glenn]

Thanks! I'm working on the tutorial now.

[Carl Friedrich Bolz-Tereick]

@Nathan Glenn heh, I'm a Lean newb from Duisburg, waving from one city over ;-)

[Pedro Minicz]

@Nathan Glenn hey there, welcome!

[Pedro Minicz]

Well, fun you will certainly have. Know that rush you get when things compile? Completing proofs is much better, because Lean is much more annoying than any compiler out there (I'd love to see someone argue for Rust's).

[Patrick Massot]

There are several Rust people here, maybe you'll be lucky.

[Nathan Glenn]

I learned Rust for my last project and thought I'd move onto Lean, actually :D I was going to learn Haskell, but someone on HN said that learning Lean did a much better job of teaching them how to think differently, and then I came down this rabbit hole...

[Kevin Buzzard]

You can learn Haskell using Lean, just write meta in front of every definition and don't prove anything.

[Nathan Glenn]

:joy: sounds easy! Yeah my first impression is that Lean is a superset of Haskell. Haskell didn't seem super production-applicable to me at first glance, so I thought I'd go for something that provided the mind-bending language learning benefit but also had a niche application that I couldn't easily get elsewhere.