Add About, Roadmap and Get Involved pages; simplify the README

CHANGELOG.md

@@ -8,6 +8,8 @@ file is where its history lives.
 
 The first release, 1.0, is in preparation.
 
+- The website has About, Roadmap and Get Involved pages, and the header on every page links to them.
+
 - The Jekyll home page is retired: the Verso website is served at the root, with redirects from the
   old page URLs, and the Lean and Mathlib versions are stated in `README.md` alone. The blueprint's
   text column and the API docs' welcome page are centred as in the books, and the web blueprint's

README.md

@@ -1,49 +1,29 @@
 # physicslib4
 
-**A Lean 4 formalisation of the mathematical foundations of physics**
+A Lean 4 library for axiomatic physics.
 
-## Goal
-
-This project works towards a formal resolution of **Hilbert's 6th problem** — the axiomatisation of the mathematical foundations of physics — in the [Lean 4 theorem prover](https://leanprover-community.github.io).
-
-Hilbert's 6th problem calls for a rigorous mathematical treatment of the axioms underlying physical theories, analogous to what Euclidean geometry received from Hilbert's own *Grundlagen der Geometrie*. Modern physics has produced candidate axiom systems — operator-algebraic frameworks for quantum mechanics and quantum field theory chief among them — but these have never been subjected to the kind of machine-checked formal scrutiny that Lean makes possible. This project aims to change that.
-
-## AQFT in Minkowski and Lorentzian Spacetime
+Official website at <https://physicslib.github.io/physicslib4/>.
 
-physicslib4 formalises **Algebraic Quantum Field Theory (AQFT)**, specifically a sharpened version of the [Haag–Kastler axioms (1964)](https://doi.org/10.1063/1.1704187), in both Minkowski and curved (Lorentzian) spacetime. This covers:
+<p align="center">
+  <picture>
+    <source media="(prefers-color-scheme: dark)" srcset="web/static_files/axiom3-diagram-dark.svg">
+    <img src="web/static_files/axiom3-diagram-light.svg" width="320" alt="A causal diamond B containing two smaller diamonds B₁ and B₂. Dashed light-cone lines from B₁ bound its causal future and past, and B₂ lies outside them.">
+  </picture>
+</p>
 
-- The GNS construction and its role in representing states on C\*-algebras.
-- Causal structure: Minkowski and Lorentzian spacetimes, timelike/spacelike/null vectors, chronological and causal futures and pasts, the Alexandrov topology.
-- The sharpened Haag–Kastler axioms (Local Algebras, Isotony, Local Commutativity, Quasilocal Algebra, Lorentz/Isometric Covariance) and their curved-spacetime generalisations.
-- Local von Neumann algebras, irreducibility, and the equivalence of purity, irreducibility of the GNS representation, and extremality in the state space.
-- KMS states, Killing-flow automorphism groups, and thermal representations in curved spacetime.
+<p align="center"><em>Axiom 3 in one picture: the diamonds B₁ and B₂ are spacelike separated inside B, so their observables commute.</em></p>
 
-The blueprint gives full mathematical detail; see the links below.
+# What's physicslib4?
 
-## Scope
+physicslib4 aims to formalise axiomatic physical theories in the [Lean 4 theorem prover](https://leanprover-community.github.io). The library covers algebraic quantum field theory: the [Haag–Kastler axioms](https://doi.org/10.1063/1.1704187) in Minkowski and curved spacetime, the GNS construction, spectral theory and Stone's theorem.
 
-AQFT on fixed Minkowski or Lorentzian spacetime is a significant milestone, but not the end goal. Both settings treat spacetime as a fixed background and do not account for backreaction — the mutual influence between matter and geometry that is central to general relativity. A complete answer to Hilbert's 6th problem will ultimately require going further.
-
-The repository is therefore designed to grow. Future work may include, for example:
-
-- An axiomatisation of quantum mechanics (which would fall squarely within the project's scope).
-- Quantum field theory on dynamical spacetimes.
-- Connections to semiclassical gravity and beyond.
-
-Contributions in any of these directions are welcome.
+## Goal
 
-## Links
+This project works towards a formal resolution of **Hilbert's 6th problem**: a rigorous mathematical treatment of the axioms underlying physical theories.
 
-| Resource | Link |
-|---|---|
-| Landing page | https://physicslib.github.io/physicslib4/ |
-| Blueprint (web) | https://physicslib.github.io/physicslib4/blueprint/ |
-| Blueprint (PDF) | https://physicslib.github.io/physicslib4/blueprint.pdf |
-| Dependency graph | https://physicslib.github.io/physicslib4/blueprint/dep_graph_document.html |
-| API documentation | https://physicslib.github.io/physicslib4/docs/ |
-| Original Haag–Kastler paper | https://doi.org/10.1063/1.1704187 |
+Hilbert asked for a treatment analogous to what Euclidean geometry received from his own *Grundlagen der Geometrie*. Modern physics has produced candidate axiom systems — operator-algebraic frameworks for quantum mechanics and quantum field theory chief among them — but these have never been subjected to the kind of machine-checked formal scrutiny that Lean makes possible. This project aims to change that.
 
-## Getting Started
+# Getting Started
 
 Requires [Lean 4](https://leanprover-community.github.io/get_started.html) and [Mathlib4](https://github.com/leanprover-community/mathlib4), both at v4.35.0, as pinned by `lean-toolchain` and `lakefile.toml`.
 
@@ -54,13 +34,13 @@ lake exe cache get    # download prebuilt dependencies
 lake build            # build the project
 ```
 
-## Contributing
+# Contributing
 
-Contributions are welcome. The blueprint is the canonical guide to what is stated and what is proved. The tutorial's chapter ["Doing it yourself"](https://physicslib.github.io/physicslib4/tutorial/Doing-it-yourself/) explains how to set up Lean, add a result to the blueprint and the library, and run the checks; a pull request against `main` is merged once it passes all status checks, has no conflicts with `main`, and is approved by a reviewer.
+Contributions are welcome; see [Get Involved](https://physicslib.github.io/physicslib4/get-involved/). The [blueprint](https://physicslib.github.io/physicslib4/blueprint/) is the canonical guide to what is stated and what is proved. The tutorial's chapter ["Doing it yourself"](https://physicslib.github.io/physicslib4/tutorial/Doing-it-yourself/) explains how to set up Lean, add a result to the blueprint and the library, and run the checks; a pull request against `main` is merged once it passes all status checks, has no conflicts with `main`, and is approved by a reviewer.
 
-## Acknowledgements
+# Acknowledgements
 
-We are grateful to Rudolf Haag and Daniel Kastler for their foundational work, and to the authors of [Entanglement in Algebraic Quantum Field Theories](https://arxiv.org/abs/2410.16599) for their clear presentation of the GNS construction that this blueprint in part follows. We thank the Mathlib maintainers and the broader Lean community for their support, and Project Numina for partially supporting this research.
+We are grateful to Rudolf Haag and Daniel Kastler for their foundational work, and to the authors of [Entanglement in Algebraic Quantum Field Theories](https://arxiv.org/abs/2410.16599) for their clear presentation of the GNS construction that the blueprint in part follows. We thank the Mathlib maintainers and the broader Lean community for their support, and Project Numina for partially supporting this research.
 
 ---
 

blueprint/src/extra_styles.css

@@ -152,6 +152,8 @@ header.site-header .mobile-nav .nav-list { display: flex; flex-direction: column
 header.site-header .mobile-nav .nav-item { margin: var(--space-1) 0; width: 100%; }
 header.site-header .mobile-nav .nav-link { width: 100%; justify-content: flex-start; padding: var(--space-2) var(--space-4); }
 
+header.site-header .desktop-menu .nav-link { padding-left: var(--space-2); padding-right: var(--space-2); }
+@media (max-width: 1150px) { header.site-header .navbar { padding: 0 var(--space-2); } }
 @media (max-width: 1024px) {
   body > header.site-header { background-color: var(--color-bg); }
   header.site-header .desktop-menu { display: none; }

blueprint/src/webtheme/site-header.html

@@ -12,7 +12,10 @@
       <menu class="desktop-menu">
         <ul class="desktop-menu-part"></ul>
         <ul class="desktop-menu-part">
+          <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/about/">About</a></li>
           <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/tutorial/">Tutorial</a></li>
+          <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/roadmap/">Roadmap</a></li>
+          <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/get-involved/">Get involved</a></li>
           <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/manual/">Reference manual</a></li>
           <li class="nav-item active"><a class="nav-link" href="index.html" aria-current="page">Blueprint</a></li>
           <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/docs/">API docs</a></li>
@@ -23,7 +26,10 @@
     </div>
     <menu class="mobile-nav">
       <ul class="nav-list">
+        <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/about/">About</a></li>
         <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/tutorial/">Tutorial</a></li>
+        <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/roadmap/">Roadmap</a></li>
+        <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/get-involved/">Get involved</a></li>
         <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/manual/">Reference manual</a></li>
         <li class="nav-item active"><a class="nav-link" href="index.html" aria-current="page">Blueprint</a></li>
         <li class="nav-item"><a class="nav-link" href="https://physicslib.github.io/physicslib4/docs/">API docs</a></li>

web/Main.lean

@@ -4,11 +4,14 @@ import Site
 open Verso Genre Blog Site Syntax
 
 /--
-The physicslib4 website: the landing page. The tutorial and the reference manual are separate books
+The physicslib4 website: the landing page and the About, Roadmap and Get Involved pages. The tutorial and the reference manual are separate books
 (`TutorialMain.lean`, `ManualMain.lean`).
 The wordmark icons in `static_files/` are copied to the site root.
 -/
 def physicslib4Site : Verso.Genre.Blog.Site := site Site.FrontPage /
+  "about" Site.About
+  "roadmap" Site.Roadmap
+  "get-involved" Site.GetInvolved
   static "apple-touch-icon.png" ← "static_files/apple-touch-icon.png"
   static "favicon.png" ← "static_files/favicon.png"
 

web/README.md

@@ -10,8 +10,8 @@ Three documents written with [Verso](https://github.com/leanprover/verso):
   the blueprint.
 
 All three share one look: the verso-web-components design tokens with a deep-teal accent, and the
-same header with the "physicslib4" wordmark and the navigation Tutorial, Reference manual,
-Blueprint, API docs.
+same header with the "physicslib4" wordmark and the navigation About, Tutorial, Roadmap, Get involved,
+Reference manual, Blueprint, API docs.
 
 This directory is a Lake package of its own. It requires physicslib4 from `..`, so the Lean
 examples on the page are elaborated against the library itself.
@@ -24,10 +24,14 @@ examples on the page are elaborated against the library itself.
   of the blueprint and API docs (`apiDocsUrl` for one declaration).
 - `Site/Theme.lean`: the website theme (header, footer, design tokens, accent colour, code colours).
   The header, the design tokens and the stylesheet are also used by the books.
-- `Site/Components.lean`: the landing-page directives (hero, sections, code gallery, feature cards),
+- `Site/Components.lean`: the page directives (hero, sections, code gallery, feature cards, `pageToc`,
+  `anchoredHeading`, and the Get Involved page's `sideFigure`, `contributeSteps`, `contributeCards` and
+  `callout`),
   built on verso-web-components.
 - `Site/Diagram.lean`: the causal-diamond diagram, as inline SVG.
 - `Site/FrontPage.lean`: the landing page.
+- `Site/About.lean`, `Site/Roadmap.lean`, `Site/GetInvolved.lean`: the About, Roadmap and Get Involved
+  pages, at `about/`, `roadmap/` and `get-involved/`.
 - `Book/Theme.lean`: what the two books share: their stylesheet (the website's, plus `bookCss`, which
   restyles the manual genre), their HTML configuration `Book.config` and `Book.replaceHeader`,
   which puts the website header on every page.

web/Site.lean

@@ -3,3 +3,6 @@ import Site.Theme
 import Site.Diagram
 import Site.Components
 import Site.FrontPage
+import Site.About
+import Site.Roadmap
+import Site.GetInvolved

web/Site/About.lean

@@ -0,0 +1,51 @@
+import VersoBlog
+import Site.Components
+
+open Verso Genre Blog
+open Site
+
+#doc (Page) "About" =>
+
+:::pageToc
+- [What This Enables](about/#what-this-enables)
+- [With Openness and Intent](about/#with-openness-and-intent)
+:::
+
+Physics rests on mathematics, yet few of its theories are stated with the precision of a mathematical
+theory. In 1900 David Hilbert asked, as the sixth of his problems, for the axioms of physics to be
+treated mathematically, in the manner of the axioms of geometry. Proof assistants give that question
+a new kind of answer: an axiom system written in a proof assistant is unambiguous, every definition
+is explicit, and every theorem drawn from it is checked by machine. They are also a natural setting
+for AI systems that reason about physics.
+
+At the heart of this effort is *physicslib4*, an open-source library in the
+[Lean proof assistant](https://lean-lang.org/). Its aim is to solve Hilbert's sixth problem in Lean 4
+by presenting physical theories axiomatically: algebraic quantum field theory (AQFT), locally
+covariant quantum field theory (LCQFT), topological quantum field theory (TQFT), axiomatic quantum
+mechanics and others. It aims to be for physics what [Mathlib](https://leanprover-community.github.io/)
+is for mathematics. The library's foundation is AQFT: the Haag–Kastler axioms in Minkowski and curved
+spacetime, with the GNS construction, spectral theory and Stone's theorem beneath them, and no `sorry`.
+The other theories are the directions in which the library grows.
+
+::::anchoredHeading "what-this-enables" "What This Enables"
+::::
+
+A library of axiomatic physics in Lean means researchers and students can build on verified
+foundations rather than reinvent them: causal structure, nets of local algebras, states and their
+representations, and the spectral theory of operators, all mechanically verified. It means a
+standardization of axioms: each axiom system has one precise statement that anyone can read and cite,
+so a result says exactly what it assumes, and competing formulations can be compared definition by
+definition. And it means a foundation for AI-assisted proofs: formal physics for AI systems to train on
+and reason over, and a proof checker that accepts a machine-generated proof only if it is correct.
+
+::::anchoredHeading "with-openness-and-intent" "With Openness and Intent"
+::::
+
+physicslib4 is a global effort. It is open source under the Apache 2.0 licence, developed in public on
+[GitHub](https://github.com/physicslib/physicslib4), and open to contributions from anyone, anywhere:
+physicists, mathematicians, Lean users and students alike. Every statement is written down first in
+a public [blueprint](https://physicslib.github.io/physicslib4/blueprint/), so that what the library
+claims can be read and questioned without knowing Lean.
+
+To see where the project is heading, read the [roadmap](roadmap/). To take part, see
+[how to get involved](get-involved/). To learn the library, start with the [tutorial](tutorial/).