Glitnir: A simple notebook format for Lean

Glitnir is a simple notebook format that makes it easier for a standard human mathematician to follow agent-generated proofs in Lean.

A notebook is an ordinary .lean file: the prose lives in a specific Markdown format inside its /-! … -/ comment blocks, so it builds with Lean like any other file.

Glitnir is also this VS Code extension, which renders and checks notebooks beside their source, and an authoring skill that teaches coding agents such as Claude Code or Codex to write Lean in this style.

See example notebooks.

The Origin

I built Glitnir to fit how I work with Lean and coding agents.

My usual setup is VS Code, split into three panes: one for the Lean code itself, one for the Glitnir rendering and one for the coding agents. As the agents work, the Glitnir window updates live and highlights the newest changes, so I can follow their reasoning, intervene when they go the wrong way, or, more often, ask them to explain something better in the notebook or dig deeper into something.

Generally I am not a believer in new agent harnesses for math. I think coding agents, with the right skills and tools, are the perfect agents for mathematical research. So that is what I am trying to improve with Glitnir.

The VS Code extension

The extension opens any .lean file as a rendered notebook beside your editor. Names written Glitnir: … are Command Palette commands; other bold names are buttons in the preview.

• Reading: prose, typeset mathematics, images and collapsible sections, with each claim's statement, proof and check status in its own card.
• Live updates: every save, from VS Code or a coding agent, refreshes the preview and briefly highlights the changed sections.
• Source navigation: Edit in VS Code jumps from a cell to its source, and Glitnir: Reveal in Glitnir jumps back from the cursor to the notebook.
• Claim review: Next and Previous step through the claims that need attention: out of date, not rechecked, containing sorry, resting on additional assumptions, or where checking stopped.
• Checking: Check saved file replays the saved file in Lean's kernel, independently of the project's compiled files, and marks each claim checked, admitted (it uses sorry) or assumptions (it uses extra axioms). Results are saved beside the notebook in <Notebook>.glitnir.json.
• Proof steps: Explore Proof Steps records a proof's tactic tree once, then lets you walk it with the goals before and after each step.
• Evidence and decisions: -- @evidence directives show simulations as cards that run on click; -- @decide directives ask a provider for a Lean block, which Glitnir kernel-checks before Accept inserts it into the notebook.
• History and export: recent Git commits of the notebook with their diffs, and Export HTML for an offline snapshot.

Checking, proof-step recording and evidence runs happen only when you ask. Lean always runs in the sandbox; an evidence provider computes from its output.

Install

Glitnir runs in local VS Code windows on macOS and Linux (see Limits). You need:

• VS Code 1.96 or newer, with the notebook's folder open as a trusted workspace.
• uv and Python 3.12 or newer, for the Python backend. Without uv, setup offers Install uv, which shows its command before running it: Homebrew, or the official installer https://astral.sh/uv/0.12.23/install.sh.
• Lean 4.32.1, for checking, proof steps, views, evidence and decisions; reading needs only the backend. Checking needs the notebook's project to be on that toolchain (elan toolchain install leanprover/lean4:v4.32.1): a project on another Lean version renders but cannot be checked. Build the project yourself first (lake build, after lake exe cache get for Mathlib).
• On Linux, bubblewrap with unprivileged user namespaces, which Lean runs in; the setup guide has the Ubuntu commands. macOS uses its built-in sandbox.

Then:

1. Install Glitnir — Lean Notebooks from the Extensions view once it is on the Visual Studio Marketplace, or download glitnir-VERSION.vsix from a release and run Extensions: Install from VSIX….
2. Open a Lean file in a trusted workspace and run Glitnir: Set Up Environment → Set Up (also offered when you first open a notebook). It downloads the backend wheel of the extension's own release, verifies its checksum and installs it with uv into its own environment.
3. Run Glitnir: Open in Glitnir.

Views, evidence and decisions come from the optional Forseti plugin, an extension package (a Python package installed into Glitnir's backend, not a VS Code extension) for projects built on the Forseti and Asgard Lean libraries. Ordinary Lean and Mathlib notebooks do not need it. To install it, run Glitnir: Install Extension Package… → Forseti → Download from this release.

The setup guide (INSTALL.md in each release) covers manual installation, existing environments, upgrading and troubleshooting.

Try it

Save this as Hello.lean in a new, empty folder. A loose file needs no Lake project, but it should not sit inside an existing Lean project.

/-! # A first notebook -/
theorem hello : True := by
  trivial

1. Open that folder in VS Code and run Glitnir: Open in Glitnir. Click Edit in VS Code on a cell to jump to its source, save an edit and watch the preview refresh.
2. Click Check saved file (needs Lean 4.32.1). The hello card shows checked, and the result is saved beside the notebook.
3. Run Glitnir: Set Up Coding Agent, then ask your agent to extend Hello.lean with the glitnir-notebooks skill and follow its work in the preview.

The Forseti examples repository has notebooks on circuits, dynamical systems and PDEs; they are Forseti projects and need the plugin.

Coding agents

Glitnir: Set Up Coding Agent installs the bundled authoring skill into your workspace: .claude/skills/glitnir-notebooks for Claude Code, .agents/skills/glitnir-notebooks for Codex, or a folder you choose for another agent. Start a new agent session and ask it to use glitnir-notebooks. The skill gives the agent the notebook syntax and the checking rules, and agents check a notebook with the command from Glitnir: Copy Validation Command.

Writing a notebook

A notebook is a .lean file that builds with standard Lean. Glitnir reads it as cells:

• Prose cells are column-zero /-! … -/ comment blocks, written in Markdown with $…$ and $$…$$ for mathematics.
• Lean cells are everything between prose cells: imports, namespaces, definitions and claims, shown as source.
• Claims are named theorem or lemma declarations, rendered with the statement and proof shown separately and the check status alongside. A docstring (/-- … -/) right above a definition or claim becomes its description. sorry marks unfinished work and is never reported as a success.
• Sections come from Markdown headings of level 2 to 6 in prose cells. Add {fold} at the end of a heading to make its section collapsible, with the first paragraph as the summary.
• Images and links: a prose line that is only ![caption](https://github.com/arnovich/glitnir/raw/HEAD/assets/figure.png) shows that file from the assets/ folder beside the notebook, and [Basics](https://github.com/arnovich/glitnir/blob/HEAD/Basics.lean) links to a sibling notebook.
• Directives are standalone comment lines: -- @view circuit myCircuit draws a view, -- @evidence simulate dissipative (h := 1/100) (steps := 400) shows a simulation that runs on click, and -- @decide disk : entailment x, y : x^2 + y^2 <= 1 |- x^2 <= 1 and y^2 <= 1 asks a decision provider for a proof. They need an extension package such as the Forseti plugin.

The authoring skill has the full rules, and the user guide describes sections, images, links and each directive in detail.

Using the preview

• Contents lists the sections; s switches between the rendered document and the Lean source.
• Follow edits scrolls to the sections each save changed.
• Claims (c) steps through the claims with j and k; i opens the claim inspector; n and p go to the next and previous claim that needs attention.
• Check through here (r) checks only through the selected claim. A result goes out of date when anything above its claim changes. Glitnir: Copy Validation Command gives the same check for a terminal or a coding agent.
• Explore Proof Steps (t) walks the selected proof's goals.
• Run on an evidence or decision card runs it, one at a time. Accept on a checked decision inserts its block after the directive and saves the file.
• ⌘K G on macOS and Ctrl+K G on Linux run Glitnir: Reveal in Glitnir from the editor. Press ? in the preview for every shortcut.

The user guide covers the preview and checking in detail: statuses, what a check accepts, import replay and caches, linked notebooks and the claim graph.

Settings

Limits

• Lean 4.32.1 only. Checking, proof steps, views, evidence and decisions use that toolchain; a project on another Lean version can be read but not checked.
• Local macOS and Linux only. Windows, remote windows (SSH, WSL, containers) and virtual or untrusted workspaces are unsupported. On Linux, the sandbox needs an x86-64 or ARM64 machine.
• Lean always runs in the platform sandbox. Lake configuration that needs subprocesses is unavailable on macOS.
• Glitnir does not prepare projects. It never builds or downloads dependencies; run lake build yourself. Views, evidence, decisions and imports of other notebooks need the notebook inside a built Lake project; a loose .lean file has no prepared imports.
• Simulation is evidence, never proof. Evidence never changes a claim's status or the check's exit code, and a decision provider only proposes a Lean block that the kernel check must accept.

Where next

• Something wrong? Start with Output → Glitnir, then the troubleshooting list, then report an issue.
• User guide: the notebook format, the preview, checking, settings, keyboard shortcuts and extension packages in full.
• Setup guide: requirements, manual installation, existing environments, upgrading and troubleshooting.
• Forseti plugin: views, evidence and decisions, with every option and goal form.
• DEVELOPMENT.md: building, testing and releasing Glitnir, and the static export for galleries.
• SECURITY.md: report vulnerabilities privately.
• MIT licensed, with third-party notices. Pull requests are limited to invited collaborators.