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 plugin I had to find a Lua alternative. Once I had that, I updated my Ansible playbooks for the Neovim installation. This took about a week. Once I had a repeatable process, I tested it on my other machines and, once satisfied, archived Vim from my Ansible playbooks. The plugins I ended up with are:
| Name | Description |
|---|---|
| bufferline | Buffer display |
| conjure | Lisp and Clojure support |
| devicons | File icons |
| dokuwiki | DokuWiki syntax |
| git | Git integration |
| lean | Lean language support |
| lsp | LSP configuration |
| lualine | Status line display |
| miniicons | Mini icons |
| sexp | Precision editing for S-expressions |
| sexp-mappings | Sexp key mappings for regular people |
| tree | File explorer |
| windsurf | Codeium code completion |
However, plugins were only part of the migration. Lean uses an extended font set, enabling mathematicians to use familiar symbols in code and proofs. My default terminal font did not support those characters. Neovim offers a solution via Nerd Fonts. That meant updating my terminal emulator and reviewing other UI tools such as Gitk, Git GUI, and Mousepad. Resetting the system font would be the obvious thing to do, but the fonts need to be installed early in the site's playbook, otherwise trouble might ensue.
| Name | Description |
|---|---|
| adwaita | Adwaita Mono Nerd Font |
| cousine | Cousine Nerd Font |
| firacode | FiraCode Nerd Font |
| lua-ls | Lua language server |
| marksman | Marksman markdown LSP |
| texlab | TexLab LaTeX LSP |
Once the plugins, fonts, and LSP servers were in place, the next step was syntax highlighting. Neovim v0.12 would have made that easier, but I still found syntax files for my most commonly used languages, including Lean.
After a week, I had a native Neovim environment. One unforeseen benefit of the transition was that I ended up with less Ansible code. I dropped a few plugins, but overall the configuration was simpler for Neovim.
VS Code
I also use VS Code. To support Lean, I installed the following extensions:
| Name | Description |
|---|---|
| Lean 4 | Lean 4 language support for VS Code |
| Loogle Lean | Loogle Lean search for VS Code (like Hoogle) |
This was straightforward. VS Code's default font supports the mathematical characters needed for Lean 4. The extensions are available through the official marketplace.
That left the main task: installing Lean, which was the whole point of the Neovim exercise…
Lean 4
The first thing I discovered was that Debian does not package Lean.
That was disappointing. However, after some reading, I found a package
called elan. Elan works
as a toolchain manager similar to Rust's rustup or
Haskell's ghcup. Elan is Lean's official version manager,
which handles downloads and updates. Once installed, it manages Lean
versions. I now have all the tools ready to start learning Lean 4.
This will be covered in the next blog post. The following introduction was generated from my Lean 4 NotebookLM: Software as Absolute Mathematical Proof.
Comments