Tools for Functional Programming in Lean 4
I've been busy this month learning about the success of LLMs in the Mathematical Olympiad . What interested me was not the result itself, but the tools used by the AI teams. They used the proof assistant called Lean . Lean is an interactive theorem prover and functional programming language. It also has dependent types. That opened up a rabbit hole that has consumed me for the past three weeks. So the yak shaving began… Neovim My editor of choice, Vim , did not support Lean . That meant retooling from Vim to Neovim . Instead of keeping my old Vim configuration, I decided to go fully Neovim-native with Lua configuration. That meant reviewing my Vim plugins and syntax files. The move was made a little harder because the version of Neovim available on Debian testing is v0.11.6. Many useful features landed in Neovim v0.12 and later, but those are not yet available on Debian testing. They are, however, available on Debian unstable . I just have to be patient. So, for each Vim plu...