5. The LLM🔗

In this chapter, we are going to install Codex inside VS Code, configure it so as to make writing Lean code easy, and explain the workflow we have designed to work on the library using Codex. (We could certainly work with other LLMs like Claude Code; the setup process should be very similar.)

5.1. Installation and first usage🔗

Click here. It should open VS Code and show you the Codex extension in the marketplace. If it doesn't, just go to VS Code, click on Extensions in the left bar, and search for the Codex extension.

Codex extension

After you install it, you’ll find Codex in your editor sidebar. Codex opens in the right sidebar by default; restart the editor if you don’t see Codex right away. The first time you use it, it will ask you to log in. After that, you will be able to start using Codex.

Codex sidebar

5.2. Skills🔗

We are now going to install the official Lean4 skills for Codex.

What are skills?

Skills are small packages of instructions that tell Codex how to do a particular kind of work. They do not modify the Lean project by themselves, and they are not extensions in the VS Code sense. They are more like a manual that Codex reads before acting: which commands to run, which files to inspect, what conventions to follow, and which mistakes to avoid.

The Lean4 skills we install here teach Codex how to work inside Lean projects. In particular, they explain how to use the Lean language server, how to inspect proof states and error messages, how to search mathlib, and how to fill sorrys while keeping the file compiling. This makes Codex much more useful than a generic code assistant when we ask it to write Lean.

Learn more about skills in the official Codex documentation.

Make sure you have the banlat library open (as a project or folder) in VS Code. Open Codex on your right and send it the following:

$skill-installer install https://github.com/leanprover/skills/tree/main/skills/*

When prompted for permission to fetch the skills and install them, say yes. After that, restart Codex and the new Lean skills will be available.

5.3. MCP🔗

Next we are going to install the Lean MCP.

What is an MCP?

MCP stands for Model Context Protocol. It is a standard way for an AI assistant to talk to external programs. The assistant itself does not know how to inspect every possible database, website, editor, or program on your computer. Instead, an MCP server exposes a small set of tools, and the assistant can call those tools when it needs them.

The Lean MCP is one of those servers. It connects Codex with the Lean language server, the same piece of infrastructure that powers the Lean information you see in the Lean Infoview of VS Code. This lets Codex ask precise questions such as: what are the current diagnostics? what is the proof state at this line? what is the type of this term? where is this definition declared? It also gives Codex access to Lean-specific search tools such as LeanSearch, Loogle, and Lean Finder.

This is important because Lean code is very hard to write just by guessing from the text of the file. With the Lean MCP, Codex can see the feedback that Lean itself is giving, and can use that feedback to iterate much more reliably.

In order to do this, open Codex in VS Code and prompt:

Install the Lean MCP.

Authorize Codex whenever needed and, once it is done, restart VS Code. Now you can go to Codex, prompt /mcp, and you should see the Lean MCP in the list. You can also ask Codex if it has access to the Lean MCP tools.

Lean MCP in Codex

5.4. AGENTS.md🔗

Now that Codex has all the tools needed to write Lean code efficiently, you should have a look at the file AGENTS.md.

Within, you will find something like this:

**State mode** — activated when asked to state (but not prove) a result.
- Fill every proof body with `sorry`.
- The file must compile modulo `sorry` (no other errors).
- Do not write any proof content; the signatures are what will be reviewed.
- Before editing any file, first show the proposed diff/patch and ask for
  permission. Do not apply the edit until explicitly approved.

**Prove mode** — activated when asked to prove a result.
- The file must compile with no `sorry` whatsoever.
- If the proof needs an auxiliary result, introduce it as a `private lemma`
  with its own proof; do not touch public declarations.
- The file must compile with no style or suggested `warning`.

These are the two main modes in which we work with Codex. We first enter state mode, and ask Codex to state some definitions and theorems we want to incorporate (at this stage, the proof of the theorems will be sorries, which are nothing but placeholders for actual proofs). Then, we check very carefully that the formal Lean statements Codex produced correspond to the informal statements we wanted to formalize (Codex is instructed to ask for confirmation before applying the changes). Once we are happy with the definition and theorem signatures (i.e., statements), we let Codex apply the patch. We now have the scaffolding ready. Start a new Codex session in prove mode and ask it to fill in the sorries. As you can see above, in this mode Codex will try to make the file compile with no warnings (and, in particular, with no sorries), splitting the proofs into private lemmas where needed. (For Lean, a lemma is the same as a theorem; a private lemma is a lemma that does not appear in the documentation and that cannot be used outside the current file. This is useful to organize big proofs into small intermediate results that won't be reused.)

The LLM will write Lean code for us, but it still needs careful supervision to make sure it is formalizing what we want to formalize and in the way we want to formalize it. In order to do this, we need to know some Lean basics.