Fwiw there's also an Emacs plugin which is what I use and it works really well. For using Lean as a theorem prover, this book is pretty good: https://github.co

Fwiw there's also an Emacs plugin which is what I use and it works really well. For using Lean as a theorem prover, this book is pretty good: https://github.com/lean-forward/logical_verification_2024 https://github.com/lean-forward/logical_verification_2024 Also, Lean is also remarkably usable as a programming language itself, which might give an easier onboarding ramp: https://lean-lang.org/functional_programming_in_lean/ https://lean-lang.org/functional_programming_in_lean/