Hi from Alex Mackay

Stream: new members

[Alex Mackay]

Hi, I'm a maths student hoping to eventually do research related to computer proofs. I've completed the natural number game and the tutorials project, and started working through the lftcm20 exercises.

[Jeremy Tan]

At this time you should probably be learning Lean 4, not Lean 3

[Jeremy Tan]

We're currently porting the whole mathlib library to lean 4

[Eric Wieser]

We have a lot more tutorial content for maths in Lean3; so I think "you should use Lean 4 instead" is advice probably better suited until Alex is through that content. The lessons are certainly transferrable!

[Alex Mackay]

Yep I was just about to say, there still seems to be better documentation/tutorials for Lean 3, so I figured I'd start with that.

[Moritz Doll]

what kind of mathematics are you interested in?

[Alex Mackay]

I briefly confused myself by simultaneously reading the Lean 3 and Lean 4 versions of Theorem Proving in Lean at the same time (on different devices). :P

[Alex Mackay]

Moritz Doll said:

what kind of mathematics are you interested in?

Hmm tough question. Pure maths in general. Combinatorics. Theoretical comp sci.

[Moritz Doll]

ah, then you will probably be able to move to Lean 4 earlier if you wish. It seems that quite a lot of combinatorics (if not all) has been ported already.

[Yaël Dillies]

Interesting! Feel free to ping to me if you have combinatorics questions. I've contributed a good deal of what's under combinatorics in mathlib.