5 ms·
Lean has the largest existing math library, but you're kind of stuck in a microsoft ecosystem.
by mathgradthrow 2y ago
Lean has the largest existing math library, but you're kind of stuck in a microsoft ecosystem.
- mkehrt 2y agoI'm not sure what you mean. I've been playing around with Lean and it works fine on a Mac. I am using VSCode, though.
- ykonstant 2y agoIf you mean dependence on VS Code, there are emacs and neovim packages for Lean; some of the core devs use those exclusively. Also note that de Moura is no longer at Microsoft and Lean is not an MS product.