Breaking changes in Lean 4 vs 3?

Stream: lean4

[Jorge Fernandez-de-Cossio-Diaz]

Hello, I am a new user thinking about learning more about Lean. Should I learn Lean 3 or Lean 4? More precisely, if I learn Lean 3 now, are there any breaking changes coming in Lean 4 that I will have to unlearn / relearn? Thanks!

[Johan Commelin]

Welcome! What is your background / what do you want to do? More on the CS side of things or the maths side?

[Johan Commelin]

For CS stuff, just start with Lean 4. For maths, stick with Lean 3 for now.
There are plenty of breaking changes, though.

[Jorge Fernandez-de-Cossio-Diaz]

Thanks! Well I am just interested in Lean for curiosity really, I want to understand what it can do. So no CS or math specific. I just want to follow some tutorials.

[Huỳnh Trần Khanh]

(deleted)

[Arthur Paulino]

Very very broadly speaking, Lean 4 allows you to state and prove theorems like in Coq and write functional programs like in Haskell. You can even write programs and prove theorems about them.

It also allows you to expand its own syntax via metaprogramming such that you can even define your own language within it.

There's also a powerful infoview which shows you the precise context of wherever you place your cursor at.

If you're just curious about what it can do, I'd suggest picking up Lean 4 because it can do even more than Lean 3.

[Jorge Fernandez-de-Cossio-Diaz]

Ok thanks! I'll try Lean 4 then.