I love the emacs experience with lean

Stream: Emacs

[EstebanMarin]

I use eglot and everything work out of the box. I had to install elean rather than lean as a dependency to get mathlib working. But awesome experience

[Tomas Skrivan]

Would you share your config?

[Malvin Gattinger]

I am also curious, what is elean? Oh, maybe you meant elan?

[EstebanMarin]

Sorry I mean elan https://search.nixos.org/packages?channel=25.11&query=elan&show=elan
https://github.com/leanprover/elan