Is lean 3 still more suited for mathematical proving?

Stream: general

[Joseph O]

Is lean 3 still more suited for mathematical proving? I am doing nng, and I'm wondering if I should continue theorem proving in lean 3 or lean 4. Is mathlib4 at a good enough state to migrate also?

[Arthur Paulino]

It depends on the level of mathematics you're aiming at. mathlib for Lean 3 already has a big stack of abstractions to support rather advanced mathematics (from what I recall Kevin saying that it's no longer limited to undergrad level math). But if you want to stick to the basics and build an API for the natural numbers (which is likely to already exist for Lean 3), then you should be fine with Lean 4. I'd also post such questions in the #new members stream

[Joseph O]

Like I plan on mainly proving algebraic stuff, with natural numbers.

[Kevin Buzzard]

Basically the situation is that if you use Lean 4 then you don't have access to Lean 3's maths library so you are missing probably tens of thousands of lines of code here https://github.com/leanprover-community/mathlib/tree/master/src/data/nat which corresponds to many many results and definitions about the naturals (stuff like Fibonacci sequence, a theory of digits, a theory of congruences modulo N etc). However if you're happy to make these definitions yourself (i.e. basically do the natural number game in Lean 4) then Lean 4 is fine.

[Yaël Dillies]

I would still advise you to use Lean 3. mathlib4 is still an experiment at this point and you won't get nearly as much community suppport if you stumble upon a problem.

[Joseph O]

Kevin Buzzard said:

Basically the situation is that if you use Lean 4 then you don't have access to Lean 3's maths library so you are missing probably tens of thousands of lines of code here https://github.com/leanprover-community/mathlib/tree/master/src/data/nat which corresponds to many many results and definitions about the naturals (stuff like Fibonacci sequence, a theory of digits, a theory of congruences modulo N etc). However if you're happy to make these definitions yourself (i.e. basically do the natural number game in Lean 4) then Lean 4 is fine.

I mean I would probably try and prove these lemmas myself, but they are definitely fun to play around with and use. Though on the other hand, lean 4 seems interesting too. But for now, I think I will probably use lean 3 for proving, and lean 4 for more general programming.

[Joseph O]

I’m also curious as to how Lean 4 differs from Lean 3 in terms of proving, both semantically and syntactically.

[Jason Rute]

Re Lean 3 vs Lean 4: here are some key differences, mostly syntax changes. https://leanprover.github.io/lean4/doc/lean3changes.html Also glance through this page to see what Lean 4 tactic proofs now look like: https://leanprover.github.io/theorem_proving_in_lean4/tactics.html