lean 3 or lean 4

Stream: lean4

[tica]

Hello,
I'm sure this question has been asked before but I can't find an answer.

Would you advise a beginner to use lean 3 or lean 4?
Thanks

[Henrik Böving]

That depends on your topic of interest. Are you a computer scientists that wants to do functional programming and a bit of proving? Or are you a mathematician that is exclusively interested in proving.

If you fall in the first category definitely Lean 4. If you fall in the second category Lean 3 is probably the better choice due to the already available mathlib with tons of formalized mathematics already done for you. There is however ongoing work to port it to Lean 4 and sooner or later everyone will switch to Lean 4 so if you're content with not doing too advanced things for now you can also stay with Lean 4 already while the team is busy porting.

[tica]

It is mainly for doing algorithm proofs or verifying implementations and doing math.

I program mainly in C and I do not intend to write my programs in lean.

[Mario Carneiro]

doing algorithm proofs in lean generally involves writing the code in lean, since you can't prove properties about an extern function

[tica]

Yes I know.
I mean my final code will be written in another language but I will use lean to verify that the math and logic of my algorithms are correct.

[Kevin Buzzard]

It will only be a few months until mathlib has been ported to Lean 4 and then Lean 3 will be end of life.

[tica]

Ok thanks you :smile:

[Tomáš Jakl]

Kevin Buzzard said:

It will only be a few months until mathlib has been ported to Lean 4 and then Lean 3 will be end of life.

Oh, great, good to know.

I'm in a similar situation and want to start learning now. I'm comfortable with Haskell other standard programming languages so getting used to that side of things will not be an issue.

But I intend to use Lean for mathematics, mostly for logic, basic category theory, and a study of relational structures. Would you say that that part of Lean 4 is ready already?

[Johan Commelin]

@Tomáš Jakl I think it's almost ready. In a couple of weeks, those basics should be ported.