Zulip Chat Archive

Stream: new members

Topic: Anatole Dedecker (introduction)


view this post on Zulip Anatole Dedecker (Jun 21 2020 at 10:33):

Hello everyone, I'm a first-year undergraduate in maths and computer science at Universite Paris Saclay (France), and I have been introduced to lean by @Patrick Massot . I am not familiar with Zulip, so let me know if I do anything wrong !

Although the course was more about formalization in general than about Lean itself, I got really interested in the language and I think I start to get used to using it. I'm mostly using it for fun (yes, that's my kind of fun), but that doesn't mean I give up when I'm stuck (it turns out to be the opposite).

Recently I also started to approach a bit more the computer science side of Lean. In particular, I've been trying to encode inside Lean a game we had to code in C++ at the beginning of the year, and it is really interesting (although I've got a lot of performances problem), so I might dive a little bit deeper to this side.

Anyways, I'm really interested in doing more lean. I'm currently playing the Natural Number Game, but if you have any suggestion of other things to do, I'll take it. I can also help to do more "useful" things, for example translating between French and English, so if there are any project where an undergraduate could help, let me know !

TL;DR : Hello everyone !

view this post on Zulip Kevin Buzzard (Jun 21 2020 at 10:43):

I think Patrick and Sebastien have been translating the natural number game into French!

view this post on Zulip Mario Carneiro (Jun 21 2020 at 10:44):

Those all sound like good projects. Feel free to ask about any problems you run into, you will find plenty of folks willing to help

view this post on Zulip Mario Carneiro (Jun 21 2020 at 10:46):

As for performance problems with Lean vs C++, well that's basically to be expected, although it is also possible that you've accidentally done something which has very poor asymptotic complexity like reducing numerals to unary

view this post on Zulip Anatole Dedecker (Jun 21 2020 at 10:46):

Kevin Buzzard said:

I think Patrick and Sebastien have been translating the natural number game into French!

Yes I know, Patrick sent me the repo link so I could help too, I'm a little bit busy right now but I think I'll start soon !

view this post on Zulip Anatole Dedecker (Jun 21 2020 at 10:48):

Mario Carneiro said:

As for performance problems with Lean vs C++, well that's basically to be expected, although it is also possible that you've accidentally done something which has very poor asymptotic complexity like reducing numerals to unary

I was using nat for computing purposes, which, as @Kevin Buzzard told me, doesn't seem to be a good idea :sweat_smile:

view this post on Zulip Mario Carneiro (Jun 21 2020 at 10:53):

Yes and no. nat is the most efficient primitive in the lean VM for doing arithmetic

view this post on Zulip Mario Carneiro (Jun 21 2020 at 10:53):

despite the apparent unary implementation

view this post on Zulip Anatole Dedecker (Jun 21 2020 at 10:55):

Oh. So what is num for then ?

view this post on Zulip Mario Carneiro (Jun 21 2020 at 11:04):

It is not much used. It can be used as a proof that nat can be viewed as an inductive over binary strings, and it can also be used for efficient nat computation in the kernel

view this post on Zulip Mario Carneiro (Jun 21 2020 at 11:04):

However, we generally try to avoid computation in the kernel altogether because lean is better at checking explicit proofs than "heavy refl" proofs

view this post on Zulip Patrick Massot (Jun 21 2020 at 11:10):

Anatole Dedecker said:

Although the course was more about formalization in general than about Lean itself, I got really interested in the language and I think I start to get used to using it.

It was not even about formalization in general, it was about the concept of proof and proof writing.

view this post on Zulip Patrick Massot (Jun 21 2020 at 11:11):

I'm mostly using it for fun (yes, that's my kind of fun), but that doesn't mean I give up when I'm stuck (it turns out to be the opposite).

You don't have to explain that sense of "fun" here...

view this post on Zulip Patrick Massot (Jun 21 2020 at 11:15):

Recently I also started to approach a bit more the computer science side of Lean. In particular, I've been trying to encode inside Lean a game we had to code in C++ at the beginning of the year, and it is really interesting (although I've got a lot of performances problem), so I might dive a little bit deeper to this side.

If you are interested as Lean as a programming language then going straight from C++ to Lean is a very long jump, especially since we have very little documentation on this topic. Do you already know a functional programming language? If no then the more or less canonical next step is to read learnyouahaskell.com. You should do that at some point, even independently of Lean. It's a very good way to broaden your perspective on programming, and it's very interesting, although a lot of it is about solving issues created by the masochistic idea of functional programming (the code name here is monad).

view this post on Zulip Patrick Massot (Jun 21 2020 at 11:16):

Also, if you are serious about using Lean as a programming language, you may want to go directly to Lean 4. It's not yet ready as a proof assistant but it's already a much better programming language if I understand correctly.

view this post on Zulip Anatole Dedecker (Jun 21 2020 at 11:47):

Patrick Massot said:

Recently I also started to approach a bit more the computer science side of Lean. In particular, I've been trying to encode inside Lean a game we had to code in C++ at the beginning of the year, and it is really interesting (although I've got a lot of performances problem), so I might dive a little bit deeper to this side.

If you are interested as Lean as a programming language then going straight from C++ to Lean is a very long jump, especially since we have very little documentation on this topic. Do you already know a functional programming language? If no then the more or less canonical next step is to read learnyouahaskell.com. You should do that at some point, even independently of Lean. It's a very good way to broaden your perspective on programming, and it's very interesting, although a lot of it is about solving issues created by the masochistic idea of functional programming (the code name here is monad).

I do know functional languages (at least in theory, i haven't used them a lot though), and I encoded the game in a way I consider being functional-style, so really different from the C++ approach of course. I was actually quite close of it working (with a lot of sorry though, because proofs are often required when working with {n : nat // n < p}), but it was really inefficient, and I couldn't find why it was. I'll have a look at Haskell anyway, and maybe making the game in Haskell will help me with the lean implementation.

view this post on Zulip Utensil Song (Jun 22 2020 at 07:01):

@Anatole Dedecker What kind of game are you trying to encode in Lean? I'm curious about how far Lean 3 can go in ordinary programming.

view this post on Zulip Johan Commelin (Jun 22 2020 at 07:07):

@Utensil Song Have you seen the "Lean for hackers" tutorial by @James King ?

view this post on Zulip Utensil Song (Jun 22 2020 at 07:11):

Yes, I have ( https://agentultra.github.io/lean-for-hackers/ ), but it seems to be far from complete (compared to an ordinary programming language).

view this post on Zulip Utensil Song (Jun 22 2020 at 07:17):

I've read some source code of Lean 4, that opens a whole lot of possibilities. For example, maybe we could have a standard library via FFI to Rust's std library.

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 13:05):

Utensil Song said:

Anatole Dedecker What kind of game are you trying to encode in Lean? I'm curious about how far Lean 3 can go in ordinary programming.

It's a game called "Squadro". I might have chosen too difficult for a first approach :D


Last updated: May 10 2021 at 00:31 UTC