Get Involved

Contributions are welcome. The blueprint is the canonical guide to what is stated and what is proved.

The tutorial's chapter Doing it yourself explains how to set up Lean, add a result to the blueprint and the library, and run the checks.

Two spacelike-separated diamonds inside a causal diamondA large causal diamond B contains two smaller diamonds B1 and B2 side by side. Dashed light-cone lines at 45 degrees from B1 bound its causal future and past; B2 lies outside them, so B1 and B2 are spacelike separated.BB₁B₂tx
A result in the library: local commutativity on causal diamonds, Axiom 3 of the Haag–Kastler axioms.

From an idea to a pull request

  1. Set up LeanInstall Lean, clone the repository and build the library.
  2. Write it in the blueprintState the result and its informal proof, with its dependencies.
  3. Prove it in LeanAdd the declaration to the library and link it to its blueprint entry.
  4. Open a pull requestIt is merged once it passes all status checks, has no conflicts with main, and is approved by a reviewer.

Where to start

Learn the library

The tutorial introduces AQFT and Lean, with worked examples and exercises.

Read the tutorial →

See what is stated

The blueprint gives every definition and theorem in mathematical prose, linked to its Lean.

Open the blueprint →

Contribute on GitHub

The source of the library, the blueprint and this website, developed in public.

Go to the repository →