Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
mathgradthrow
on June 12, 2024
|
parent
|
context
|
favorite
| on:
Terence Tao on proof checkers and AI programs
Lean has the largest existing math library, but you're kind of stuck in a microsoft ecosystem.
ykonstant
on June 12, 2024
|
next
[–]
If 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.
mkehrt
on June 12, 2024
|
prev
[–]
I'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.
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search:
