Anatole Dedecker (introduction)

Stream: new members

[Anatole Dedecker]

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 !

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Anatole Dedecker]

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 !

[Anatole Dedecker]

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:

[Mario Carneiro]

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

[Mario Carneiro]

despite the apparent unary implementation

[Anatole Dedecker]

Oh. So what is num for then ?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Anatole Dedecker]

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.

[Utensil Song]

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

[Johan Commelin]

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

[Utensil Song]

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

[Utensil Song]

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.

[Anatole Dedecker]

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