4. Doing it yourself🔗

4.1.1. Installing Lean and building the library🔗

Lean is installed through elan, which downloads and manages Lean versions. Each project names the version it needs in a file lean-toolchain at its root, and elan fetches that version when you first build the project, so you never install a Lean version by hand. The Lean community's installation guide covers each operating system; on Linux and macOS it comes down to

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

and a new terminal. With git installed, fetch the library and build it:

git clone https://github.com/physicslib/physicslib4.git
cd physicslib4
lake exe cache get
lake build

Lake is Lean's build tool, installed with elan. lakefile.toml names the project's dependencies, Mathlib among them, and lake-manifest.json pins each to an exact commit.

• lake exe cache get downloads Mathlib's compiled files, several gigabytes: minutes on a fast connection, longer on a slow one. Without it, lake build would compile Mathlib itself, which takes hours. (lake exe cache get! downloads everything again, if a download was interrupted.)

• lake build then compiles the library's hundred-odd files. The first time takes a while (tens of minutes on a laptop is normal); later builds recompile only the files that changed and those that import them.

A build that ends without errors has checked every proof in the library.

4.1.2. The editor🔗

The standard editor is VS Code with the Lean 4 extension. Open the folder physicslib4 itself, so that the extension finds lean-toolchain, and then a library file, say Physicslib4/AQFT/HaagKastler/Net.lean, the home of chapter 3's trivial net. A Lean server starts, loads the file's imports (seconds, once lake build has run) and checks the file as you type. Three things are then at hand.

• The infoview, a panel beside the file (the ∀ menu, "Toggle Infoview"). With the cursor in a tactic proof it shows the goal at that point, as the goals blocks of chapters 2 and 3 do for a whole proof. Step through trivialLocalNet_localCommutativity and watch the goal change.

• Hovers, as on these pages: the type and docstring of a name. Ctrl-click (Cmd-click on macOS) jumps to its definition, in the library or in Mathlib.

• Errors and warnings, underlined in the file and listed in the infoview. Lean checks past an error, so one mistake does not hide the next.

A file sees changes to the files it imports once they are saved and its server is restarted ("Lean 4: Server: Restart File").

4.1.3. Running the tutorial's exercises🔗

Create a file at the root of the repository, say Playground.lean, and start it with

import Physicslib4

open Physicslib4 Spacetime AQFT.HaagKastler
open scoped ComplexOrder InnerProductSpace

import Physicslib4 loads the whole library, and Mathlib with it. Below, paste an exercise from chapter 2 or 3, together with any definition from the text it uses, such as chapter 3's identityState, and replace the sorry by a proof. The file is yours; do not commit it.

The tutorial itself is the Lean package in web/, one file per chapter: this one is web/Tutorial/DoingItYourself.lean. Its Lean examples are checked when the package is built:

cd web
lake exe cache get
lake build
lake exe generate-tutorial --output _out/tutorial

The first lake build in web/ compiles Verso, the tool that renders these pages, and the native code of the modules it links, and takes a while. The last command writes the HTML to web/_out/tutorial/html-multi/, and web/README.md explains how to view it. Change an example so that it fails to check, and the build stops there.

example : identityState.IsFaithful := by
  intro a ha
  exact star_mul_self_pos_iff.mpr ha

4.2.1. The blueprint is the specification🔗

As you will recall from chapter 1, the project's starting point is the blueprint, a document in ordinary mathematics that sharpens the 1964 axioms of Haag and Kastler (1964)Marginal noteShow marginal noteRudolf Haag and Daniel Kastler (1964). “An algebraic approach to quantum field theory”. Journal of Mathematical Physics. 5(7), pp. 848–861. where they are under-specified. Its chapters 1 to 9 analyse the original axioms one by one and give the context; only chapter 10 is formalised. Every definition and theorem of chapter 10 carries a label, such as def:state, and names the Lean declarations that formalise it. A Lean statement is correct when it says what its blueprint entry says, so it is checked against the blueprint, and not against the 1964 paper or a textbook. If you think the blueprint is wrong or imprecise, the fix starts there.

4.2.2. Where things are🔗

The repository has four parts.

• Physicslib4/: the library, by subject. Spacetime/ and Geometry/ hold spacetimes, their causal structure and the Alexandrov topology; GNS/ states and the GNS construction; Spectral/ and Operators/ the spectral theorems, Stone's theorem and operator algebra; Analysis/ supporting analysis; AQFT/HaagKastler/ and AQFT/HaagKastlerCurved/ the axioms in Minkowski and in curved spacetime. The file Physicslib4.lean imports every file of the library.

• blueprint/src/: the blueprint's LaTeX source; chapter 10 is in sections/sec10/, one file per section.

• web/: the project's website, this tutorial and the reference manual, which follows the sections of chapter 10 and collects the library's conventions.

The published versions are linked from the header of this page: the blueprint, with its dependency graph, and the API documentation, generated from the docstrings.

4.2.3. Conventions🔗

A few rules keep the library and the blueprint in agreement.

• Definitions are design decisions. The topology on Minkowski space, the class of regions, and the fields of structures such as LocalNet, Isotony and HaagKastlerNet fix what the library means by a net. A change to them changes what every theorem says, so it is proposed and discussed in an issue before it is made. Theorems, lemmas and proofs can be added freely.

• Restrictions are recorded. When a declaration is deliberately less general than the blueprint intends, its docstring says so on a line starting **Restriction:**, naming the intended general form and what it is waiting on, in the form **Restriction:** <restriction>; the intended form <general form>, and is waiting on <result>. The line is removed when the general form is formalised.

• Documentation is in the present tense. Docstrings, comments, the blueprint and the home page describe what the project is, not how it came to be: no "previously" or "now". The history goes in CHANGELOG.md.

• No sorry. A sorry is useful while you work, as you will see, but the library contains none, and a contribution adds none.

4.3.1. Start from the blueprint🔗

A new result begins as a blueprint entry. In blueprint/src/sections/sec10/haag-kastler-axioms.tex, next to the entries it depends on, it would read:

\begin{proposition}[The State of the Trivial Net]
    \label{prpstn:trivial-net-state}
    \uses{def:state, def:quasilocal-algebra}
    Let $\mathfrak{U}$ be the quasilocal algebra of the net that
    assigns $\mathbb{C}$ to every diamond. Every element of
    $\mathfrak{U}$ is a multiple $\lambda\mathbf{1}$ of the unit,
    and $\lambda\mathbf{1} \mapsto \lambda$ is the only state
    on $\mathfrak{U}$.
\end{proposition}
\begin{proof}
    \uses{def:quasilocal-algebra}
    Each local algebra is $\mathbb{C}$, so its image in $\mathfrak{U}$
    lies in $\mathbb{C}\mathbf{1}$. This subspace is finite-dimensional,
    hence closed, and the union of the images is dense, so
    $\mathfrak{U} = \mathbb{C}\mathbf{1}$. ...
\end{proof}

\label gives the entry its name. \uses lists the entries the statement, or the proof, depends on; they become the edges of the dependency graph. Two more commands come later, once the Lean exists: \lean{…}, with the full names of the declarations that formalise the entry (and \leanfile{…}, this project's own addition, with their file), and \leanok, which marks the statement as formalised when it is in the statement and the proof as formalised when it is in the proof. The graph colours each node accordingly. Writing the proof on paper first is not a formality: it tells you which lemmas the Lean proof needs.

4.3.2. Translate it into Lean🔗

The statement goes in the library next to what it uses. Here that is a new file, Physicslib4/AQFT/HaagKastler/TrivialState.lean, which imports the files that define the trivial net and GNS.State.comp, opens namespace Physicslib4.AQFT.HaagKastler like its neighbours, and is added to Physicslib4.lean. The two claims, with sorry for their proofs:

algebraMap ℂ A is Mathlib's name for the map \lambda \mapsto \lambda\mathbf{1} of a complex algebra A, and the underscore lets Lean fill in A from the type of x. The first statement says that every element is a multiple of the unit; the second that every state takes the value \lambda on \lambda\mathbf{1}, which, with the first, is uniqueness. Existence is a construction, a term of type GNS.State trivialHaagKastlerNet.quasilocal.carrier, and section 6 builds it.

A sorry lets everything else be checked: Lean reports a warning, "declaration uses sorry", and otherwise accepts the file. You can state all the lemmas of a proof this way, check that they fit together, and fill them in one at a time.

4.3.3. Check what the statement says🔗

A Lean statement can fail to mean what you intend, and a proof of the wrong statement is worth nothing. Before proving, check it.

• Read it back. Hover over each name, or #check the statement, and read the result as mathematics. Is trivialHaagKastlerNet.quasilocal.carrier the algebra the blueprint means? It is: the quasilocal algebra that every predicate of the library, such as IsVacuumState, refers to.

• Beware of statements that are too easy. The library's trivialQuasilocalAlgebra is also a quasilocal algebra of the trivial net, with carrier ℂ, and a state on it is just identityState. Stated for it, the project would be a one-liner, and would say nothing about the algebra that matters.

• Beware of hypotheses that cannot hold. A theorem with contradictory hypotheses is true and useless. If you suspect this, try to prove False from them.

• Test special cases. Specialise the statement to a case you can check by hand, or try to prove a slightly stronger one and see where it fails.

4.4.1. Guessing a name, and #check🔗

Mathlib's naming convention suggests where to look. A *-homomorphism is in particular an algebra homomorphism, and for these the property "commutes with algebraMap" is called commutes. #check confirms the guess:

AlgHomClass.commutes
  (trivialHaagKastlerNet.quasilocal.ι
    isAlexandrovBasisSet_trivialBasisSet) : ∀ (r : ℂ),
  (trivialHaagKastlerNet.quasilocal.ι isAlexandrovBasisSet_trivialBasisSet)
      ((algebraMap ℂ (trivialHaagKastlerNet.U.algebra trivialBasisSet)) r) =
    (algebraMap ℂ trivialHaagKastlerNet.quasilocal.carrier) r

AlgHomClass.commutes f r holds for any algebra homomorphism f, *-homomorphisms included, and applying it to the embedding ι of one diamond (trivialBasisSet, the library's sample diamond) shows what it says there: ι sends r\mathbf{1} to r\mathbf{1}. Applying a lemma to the objects at hand is often the quickest way to read it.

4.4.2. exact?, apply? and rw?🔗

When the goal is a standard fact, let Lean search. exact? looks for a single lemma, applied to hypotheses in context, that closes the goal:

Try this:
  [apply] exact (IsClosed.closure_subset_iff ht).mpr h

Replace exact? by the suggestion, which in the editor is one click. apply? lists lemmas whose conclusion matches the goal, leaving their hypotheses as new goals, and rw? lists equations that can rewrite it. These searches work well for small, general facts. They fail, or time out, when the goal is large or the lemma needs an argument that is not in context, and they see the goal as written: a goal phrased with the library's own definitions may need change or unfold first.

4.4.3. Loogle🔗

Loogle searches Mathlib by the constants and patterns a statement contains. The query IsClosed, Submodule, FiniteDimensional asks for statements that mention all three, and among the first results is

Submodule.closed_of_finiteDimensional (s : Submodule 𝕜 E)
  [FiniteDimensional 𝕜 ↥s] : IsClosed ↑s

(with the hypotheses on the field 𝕜 and the space E omitted): a finite-dimensional subspace of a Hausdorff topological vector space over a complete field is closed. Patterns with ?x for unknown terms, such as closure ?s ⊆ ?t, narrow the search further.

4.4.4. Documentation and sources🔗

The API documentation lists each declaration of the library, and Mathlib's lists each of Mathlib's, with its docstring and a link to its source. From the blueprint, each entry links to the documentation of its Lean declarations, so a concept you know in mathematics leads to its Lean name. Finally, the sources are on your disk: Mathlib is in .lake/packages/mathlib/Mathlib/, and a text search such as

grep -rn "closed_of_finiteDimensional" .lake/packages/mathlib/Mathlib

finds the declaration first, and its file, where the lemmas around it are often the ones you need next.

4.5.1. Working interactively🔗

A Lean proof is written in a loop: read the goal in the infoview, take one step, read the new goal. Each step should correspond to a sentence of the paper proof; if you cannot say which sentence, stop and write it on paper first. Two habits help.

• Keep the file checking. Write sorry for whatever you have not done yet, so that Lean checks the rest and the infoview shows the goals that remain.

• State intermediate facts. have h : P := by sorry records a fact you will need, and you prove it once the main argument goes through. If the main argument does not go through, you have lost nothing.

4.5.2. Breaking a proof into lemmas🔗

A long proof is a sequence of lemmas, each a short statement with a short proof. The paper proof of section 3 has four steps, and the Lean has four lemmas: local elements are scalars; the scalars form a closed set; therefore every element is a scalar; and therefore \lambda \mapsto \lambda\mathbf{1} is a bijection. Small lemmas are easier to prove, easier to read, and often useful elsewhere. A rule of thumb: if a proof does not fit on a screen, or a have is used twice, make it a lemma.

4.5.3. Common errors🔗

Three kinds of error account for most of the time a beginner spends stuck. Each appeared, in a mild form, in chapters 2 and 3.

Type class problems. Lean finds structure, such as a norm or a commutative multiplication, by type class search (chapter 2, section 5). When the search fails, the message says failed to synthesize; when Lean does not yet know the type to search on, it says typeclass instance problem is stuck, as in the first exercise of section 1. Another case: a GNS.State can be applied to an element, like a function, but it is not registered as a linear map, so Mathlib's map_smul does not apply to it:

failed to synthesize instance of type class
  MulActionHomClass (GNS.State ℂ) ℂ ℂ ℂ

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

MulActionHomClass is the class of maps that commute with scalar multiplication, and Lean finds no instance saying that states are such maps. (The second error, an unsolved goal of the same type, is a consequence of the first.) The fix is to apply the lemma to the state's underlying continuous linear map, ω.toContinuousLinearMap, as in the exercise below.

Universe mismatches. Recall the aside on universes in chapter 2, section 5: a structure such as HaagKastlerNet.{u} is a family of types, one for each universe level. The trivial net has its algebras in Type, so nonempty_haagKastlerNet is about level 0, and it cannot be used at level 1:

Type mismatch
  nonempty_haagKastlerNet
has type
  Nonempty.{2} HaagKastlerNet
but is expected to have type
  Nonempty.{3} HaagKastlerNet

The levels in the message are those of Nonempty, which records where its argument lives: HaagKastlerNet.{0} is a type in Sort 2, HaagKastlerNet.{1} one in Sort 3. Different levels, different types. Lean's display omits the level of HaagKastlerNet itself, so a mismatch in which two types print identically is often a universe mismatch; set_option pp.universes true shows the levels. The fix is to state the result at the level where it holds, or to generalise the construction.

Coercions. A state ω is applied to a through a coercion to a function, displayed ω a; its field ω.toContinuousLinearMap is applied through another. The two are equal by definition, but rw looks for a term as written, not up to definitions:

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ω 1
in the target expression
  ω.toContinuousLinearMap 1 = 1

ω:GNS.State ℂ⊢ ω.toContinuousLinearMap 1 = 1

The fix is change ω 1 = 1, which replaces the goal by one equal to it by definition, followed by the rewrite; or simply exact ω.apply_one, since exact does unfold definitions. Hover over the terms in the infoview to see which coercion each uses.

4.6.1. Local elements are scalars🔗

The algebra of every diamond is ℂ, so an element a of it is a number, and ι sends it to a\mathbf{1}. This is AlgHomClass.commutes applied to ι:

The lemma's left side is ι (algebraMap ℂ ℂ a), which is ι a by definition; on the right, Lean accepts a as a complex number, although its type is the algebra of B, because the two types are equal by definition.

4.6.2. The scalars are closed🔗

The multiples of the unit form the range of Algebra.linearMap ℂ A, the map \lambda \mapsto \lambda\mathbf{1} as a linear map. Its range is a finite-dimensional subspace, so Submodule.closed_of_finiteDimensional applies:

h says that the range, as a subspace, is closed. LinearMap.coe_range turns the subspace into the set Set.range (Algebra.linearMap ℂ A), which is the goal up to definitions, and rwa closes it. The finite-dimensionality is found by type class search: the range of a linear map out of a finite-dimensional space is finite-dimensional. The lemma holds in every C*-algebra, so it is stated for every C*-algebra.

4.6.3. Every element is a scalar🔗

Now the paper argument: the union of the local images lies in the closed set of scalars, so its closure does too, and the closure is everything.

• have hsub : … := by … states the inclusion of the union of the images in the scalars. Its proof: simp only [Set.iUnion_subset_iff] turns "a union is contained in a set" into "each member is", and rintro introduces a diamond B, its proof hB, and an element of the range of ι, written ι a by the pattern ⟨a, rfl⟩. Then a itself is the scalar.

• have hcl := … applies IsClosed.closure_subset_iff, found by exact? in section 4, to get the closure of the union inside the scalars.

• exact hcl (Q₀.dense_range x): the field dense_range of a quasilocal algebra says that the union is dense, so x is in its closure, and hence a scalar.

4.6.4. The isomorphism, and the state🔗

The map \lambda \mapsto \lambda\mathbf{1} is Mathlib's StarAlgHom.ofId ℂ Q₀.carrier. It is surjective by the last lemma, and injective because the algebra is nonzero: ι is injective and 1 \neq 0 in ℂ.

• refine ⟨?_, trivial_exists_scalar⟩: a bijection is a pair, injective and surjective. The second is the last lemma; ?_ leaves the first as the goal.

• h10 proves 1 \neq 0 in Q₀.carrier: if 1 = 0, then ι 1 = ι 0 in the sample diamond, and injectivity of ι gives 1 = 0 in its algebra, which is ℂ. Note (α := ℂ), which names the type as in chapter 3: the algebra of the diamond is ℂ only by definition.

• have : Nontrivial Q₀.carrier puts the instance in context, and the lemma of the section 4 exercise finishes.

A bijective *-homomorphism is a *-isomorphism (StarAlgEquiv.ofBijective). Its inverse is the *-homomorphism to ℂ the project needs, and the state is chapter 3's identityState pulled back along it with GNS.State.comp:

The check confirms that the state is \lambda\mathbf{1} \mapsto \lambda: change writes \lambda\mathbf{1} as the image of \lambda under the isomorphism, the isomorphism and its inverse cancel, and identityState z = z by definition.

4.6.5. Recording it🔗

In the library the four lemmas and the definition go into the file of section 3, each with a docstring giving the blueprint label. The blueprint entry then gets its links and its marks:

\begin{proposition}[The State of the Trivial Net]
    \label{prpstn:trivial-net-state}
    \lean{Physicslib4.AQFT.HaagKastler.trivial_exists_scalar,
      Physicslib4.AQFT.HaagKastler.trivialNetState}
    \leanfile{Physicslib4/AQFT/HaagKastler/TrivialState.lean}
    \uses{def:state, def:quasilocal-algebra}
    \leanok
    ...
\end{proposition}
\begin{proof}
    \uses{def:quasilocal-algebra}
    \leanok
    ...
\end{proof}

The \leanok in the proof belongs there only once the whole proposition is proved in Lean, uniqueness included, which is the exercise below; until then the proof carries none, and the dependency graph shows the gap.

4.7.1. What CI checks🔗

Every push and every pull request runs the workflow .github/workflows/lean_action_ci.yml on GitHub. It checks, in order:

• that the library builds (lake build);

• that it passes the linters of Mathlib's companion library Batteries (lake lint): every definition has a docstring, no argument is unused, simp lemmas are in the right form, and so on;

• that Physicslib4.lean imports every file of the library (lake exe mk_all --check), so a new file must be added there;

• that every Lean name in a blueprint \lean{…} exists (checkdecls, from the package of the same name);

• that the documentation is in the present tense (scripts/check_temporal_wording.py), as section 2 asked;

• when web/, the library or the toolchain changes, that the website and this tutorial build, and that their pages use no root-relative links.

A second workflow, .github/workflows/blueprint.yml, runs on the main branch only. It builds the blueprint's web and PDF versions, the API documentation, the website and the tutorial, and publishes them.

4.7.2. Running the checks yourself🔗

Run the checks before you push; it is faster than waiting for CI. From the root of the repository:

lake build
lake lint
lake exe mk_all --check
python3 scripts/check_temporal_wording.py

The blueprint needs leanblueprint, a Python package (pip install leanblueprint; it needs Graphviz for the dependency graph and a LaTeX installation for the PDF; its README gives the details per system). After a successful lake build,

leanblueprint web
leanblueprint pdf
leanblueprint checkdecls

build the blueprint into blueprint/web/ and blueprint/print/, and then check the \lean{…} names against the build (checkdecls reads the list of names that leanblueprint web writes). Open blueprint/web/index.html and the dependency graph, and check that your entry and its edges look as intended. For changes to the tutorial or the website, build them as in section 1.

4.7.3. Pull requests🔗

Contributions follow the usual GitHub process. Create a branch, commit your work to it, and open a pull request against main. A pull request is merged when it passes all the checks above, has no conflicts with main, and is approved by a reviewer. A notable change, such as a new result, a changed definition or a new section of the blueprint, also gets a line in CHANGELOG.md, under "Unreleased"; that file, not the documentation, is where the project's history is recorded. Keep a pull request to one topic: a reviewer can check one new result with its blueprint entry far more easily than five.

When you are stuck, ask. The Lean Zulip chat, in particular its "new members" and "Is there code for X?" channels, answers questions about Lean and Mathlib, usually within hours; a question with a short complete example that shows the problem gets the best answers. Questions and proposals about this project, including proposed changes to its definitions, go to the repository's issues.