Lean 4

Lean 4 is a pure functional programming language and an interactive theorem prover base on dependent type theory.

Building Lean 4 projects

Use the following

leanPackages.buildLakePackage {
  pname = "my-project";
  version = "0.1.0";
  src = ./.;
  leanDeps = with leanPackages; [ mathlib ];
  lakeHash = null; # all deps nix-managed; set to lib.fakeHash for Lake-managed deps
}

Installing Lean 4

Lean4 is available as a package, both on the packages 26.05 channel and the unstable channel, and they may be installed according to their provided instructions. Below is an example of a minimal Lean 4 flake.

{
  description = "Minimal Lean 4 flake.";

  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05";
  };

  outputs = { self, nixpkgs }@inputs:
    let
      system = "x86_64-linux";
      pkgs   = nixpkgs.legacyPackages.${system};
    in
      {
        devShells.${system}.default = pkgs.mkShell {
          packages = with pkgs; [
            lean4
          ];
        };
      };
}

Text Editors

Lean provides an official extension for VS Code, but community extensions can also be found for other editors such as emacs, neovim, cursor and so on. Please note, that Lean FRO recommends installing Lean through the officially supported VS Code extension.

Lean4-mode - major mode for Emacs

leanprover-community provides a lean major mode for emacs called "lean4-mode". However, the provided major mode seems to not be receiving updates, and according to community discussions, it has split up into a number of different forks, with different features and support. While the version provided by leanprover-community supports lsp-mode, the fork by GitHub user bustercopley supports eglot instead.