356 karma · joined September 1, 2012
It may destroy many foundational assumptions that humans have had for thousands of years.
- Emacs: https://github.com/leanprover-community/lean4-mode
- Neovim: https://github.com/Julian/lean.nvim
I'm using the Emacs lean4-mode and it's pretty good.
But what most of them do is not to be more efficient but to be shown to be more efficient. The main reason they are so obsessed with AI is because they want to send the signal that they are pursuing to be more efficient, whether they succeed or not.
I remember that the company behind it was called "280 South". They seem to have opensourced it before they shut down.