editors for Lean 4

Stream: lean4

[mario jose]

what is the best text editor to use lean 4?
i am gonna start to learn lean 4 as my first proof assistant language

[mario jose]

I mean what text editors have good plugins for lean 4

[Scott Morrison]

Most people are using VS Code, with the Lean 4 plugin.

[Scott Morrison]

There is an emacs mode as well.

[Scott Morrison]

Start reading at https://leanprover.github.io/lean4/doc/setup.html

[Scott Morrison]

(You may find that Lean 3 is an easier place to start: Lean 4 is not particularly beginner friendly yet.)

[mario jose]

is the difference between programming on lean 4 and lean 3 noticeable in regards to syntax?

[Scott Morrison]

Yes.