Undergraduate advanced math Linux workstation setup

Configuring LaTeX

LaTeX is a document preparation and typesetting system.

Installing LaTeX

OpenSUSE provides packages from the TeX Live project. There are a lot of packages, so I'll sometimes still need to install something. This list captures everything I've had to deliberately install for some aspect of my setup and does not explicitly include any dependencies.

sudo zypper install \
        # Foundational LaTeX packages
        texlive-latexmk \
        texlive-xetex \
        texlive-chktex \
        texlive-synctex \
        texlive-dvips \
        texlive-latexindent \
        \
        # Secondary document tools
        texlive-bibtex \
        texlive-biber \
        texlive-titlesec \
        \
        # Math formatting packages
        texlive-amsmath \
        texlive-mathtools \
        texlive-pgfplots \
        texlive-nicematrix \
        texlive-wasysym
  

Configuring LaTeX editor integration

VSCodium

Install LaTeX Workshop. If you've installed the requisite LaTeX packages already, nothing else is required.

Configuring Lean

Lean is a functional programming language and proof assistant.

Installing Lean

Lean's installation instructions go over a lot of quick installation steps that are suitable for people with standard setups. I run Linux as my primary operating system, so of course I will do things a bit more manually.

elan: the lean version manager

Installing lean starts by installing elan. Start by heading to the elan releases page and downloading an archive of the latest release.

curl -sLo $HOME/Downloads/elan-x86_64-unknown-linux-gnu.tar.gz https://github.com/leanprover/elan/releases/download/v4.2.4/elan-x86_64-unknown-linux-gnu.tar.gz
tar -C $HOME/Downloads -xf $HOME/Downloads/elan-x86_64-unknown-linux-gnu.tar.gz
  

Then execute elan-init. It's an interactive setup program and will prompt you for several options.

1. Proceed, customize or cancel the installation

   Customize.

2. Default toolchain? (stable/beta/nightly/<specific version>/none)

   Stable is the way to go.

3. Modify PATH variable? (y/n)

   n.

   The installer adds to PATH variable by modifying $HOME/.profile but I prefer to make lean's binaries accessible via somewhere already in PATH.

It then dumps an elan installation to $HOME/.elan. I don't love this so I moved it to $HOME/.local/opt/elan and symlinked the binaries to $HOME/.local/bin. You don't have to do this—it's just something I did.

mv -v $HOME/.elan $HOME/.local/opt/elan

# symlink the default ELAN_HOME to the updated path
ln -sv $HOME/.local/opt/elan $HOME/.elan

# symlink the lean binaries to a PATH directory
cd $HOME/.local/opt/elan
ln -sv ../opt/elan/bin/lake ../../bin/lake
ln -sv ../opt/elan/bin/lean ../../bin/lean
ln -sv ../opt/elan/bin/leanc ../../bin/leanc
ln -sv ../opt/elan/bin/leanchecker ../../bin/leanchecker
ln -sv ../opt/elan/bin/leanmake ../../bin/leanmake
ln -sv ../opt/elan/bin/leanpkg ../../bin/leanpkg
ln -sv ../opt/elan/bin/elan ../../bin/elan

# Alternatively, if you have stow installed
stow -t $HOME/.local/bin bin
  

This will create symbolic links in a local binary directory, which most people already have in their PATH. I can then execute them to verify that they work as expected.

↪ command -v elan lean; elan --version; lean --version
/home/sofia/.local/bin/elan
/home/sofia/.local/bin/lean
elan 4.2.4 (227caca13 2026-08-25)
Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)
  

Installing mathlib

Lean's mathlib library makes it much more usable for the documented forms of mathematics. Installing mathlib will require:

• Using lake, Lean's build tool
• A project defining a lakefile.toml.

The easiest way to obtain a lakefile.toml is to use lake to initialize a new Lean project.

# Create a new project based on mathlib
lake +leanprover-community/mathlib4:lean-toolchain new NewMathlibProject math

# Change directory into the project you just created
cd NewMathlibProject

# Retrieve the project dependency's (i.e. mathlib) cached binaries
lake exe cache get

# Build the project
lake build
  

Configuring AppArmor to allow lean toolchain to use bundled libraries

OpenSUSE ships with AppArmor which can result in interference with lake when it attempts to download library files. Evidence of interference can be found in the AppArmor audit log and can look like

type=AVC msg=audit(1791329627.259:4695): apparmor="DENIED" operation="file_mmap" class="file" profile="curl" name="/home/sofia/.elan/toolchains/leanprover--lean4---v4.35.0-rc3/lib/libz.so.1.2.11" pid=719290 comm="curl" requested_mask="m" denied_mask="m" fsuid=1000 ouid=1000

To solve this, you will need to create an additional AppArmor rule that allows curl to load library files from within the home directory.

This text should be placed in /etc/apparmor.d/local/curl.

# Allow curl to load Lean's bundled zlib when run via `lake` (which sets
# LD_LIBRARY_PATH to the toolchain's lib directory).
owner @{HOME}/.elan/toolchains/*/lib/libz.so* mr,
owner @{HOME}/.local/opt/elan/toolchains/*/lib/libz.so* mr,
  

OpenSUSE's default AppArmor configuration in /etc/apparmor.d/curl will load and merge the corresponding configuration from the local subdirectory. Run apparmor_parser -r /etc/apparmor.d/curl to reload curl's AppArmor profile.

Configuring Lean editor integration

neovim

The Lean project sponsors the lean.nvim plugin for neovim.

From the official documentation, you can install lean.nvim by adding a line of text to your neovim configuration. The default path is $HOME/.config/nvim/init.lua.

vim.pack.add { {src = "https://github.com/Julian/lean.nvim", version = "v2026.4.1" } }
          

VSCodium

I prefer to use VSCodium—a libre build of Microsoft's VSCode. Usage-wise, it's mostly identical to VSCode.

The lean extension or VSCodium can be found in the Open VSX Registry at https://open-vsx.org/extension/leanprover/lean4. The extension can be installed directly to VSCodium from this page.

I found that the extension "just worked" since I'd already installed the lean toolchain, thus did not require any additional configuration.