From 18386e18619c03283e7f74590c09c51ac1062f66 Mon Sep 17 00:00:00 2001 From: KellyJDavis Date: Sat, 31 Oct 2026 11:09:44 +0100 Subject: [PATCH] Add About, Roadmap and Get Involved pages; simplify the README - The website has About, Roadmap and Get Involved pages, and the header on every page (website, books, blueprint, API docs, 404) links to them. - Header links are spaced more tightly so that seven entries fit. - The footer separates documentation links from project links. - The README is simplified and shows the Axiom 3 diagram, in light and dark versions. Co-Authored-By: Claude Opus 5.5 --- CHANGELOG.md | 2 + README.md | 58 +++++--------- blueprint/src/extra_styles.css | 2 + blueprint/src/webtheme/site-header.html | 6 ++ web/Main.lean | 5 +- web/README.md | 10 ++- web/Site.lean | 3 + web/Site/About.lean | 51 ++++++++++++ web/Site/Components.lean | 94 +++++++++++++++++++++++ web/Site/Diagram.lean | 5 +- web/Site/GetInvolved.lean | 30 ++++++++ web/Site/Links.lean | 38 ++++++--- web/Site/Roadmap.lean | 39 ++++++++++ web/Site/Theme.lean | 65 ++++++++++++++-- web/docs-theme/physicslib4-docs.css | 3 + web/docs-theme/site-header.html | 6 ++ web/redirects/404.html | 8 ++ web/static_files/axiom3-diagram-dark.svg | 29 +++++++ web/static_files/axiom3-diagram-light.svg | 29 +++++++ 19 files changed, 423 insertions(+), 60 deletions(-) create mode 100644 web/Site/About.lean create mode 100644 web/Site/GetInvolved.lean create mode 100644 web/Site/Roadmap.lean create mode 100644 web/static_files/axiom3-diagram-dark.svg create mode 100644 web/static_files/axiom3-diagram-light.svg diff --git a/CHANGELOG.md b/CHANGELOG.md index bf0515b..54df7f7 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/README.md b/README.md index fd6a12b..7d4424b 100644 --- a/README.md +++ b/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 . -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: +

+ + + 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. + +

-- 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. +

Axiom 3 in one picture: the diamonds B₁ and B₂ are spacelike separated inside B, so their observables commute.

-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. --- diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css index 6c2114f..a2920d2 100644 --- a/blueprint/src/extra_styles.css +++ b/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; } diff --git a/blueprint/src/webtheme/site-header.html b/blueprint/src/webtheme/site-header.html index a6311e2..0da1a79 100644 --- a/blueprint/src/webtheme/site-header.html +++ b/blueprint/src/webtheme/site-header.html @@ -12,7 +12,10 @@
      +
    • About
    • Tutorial
      • +
    • Roadmap
      • +
    • Get involved
    • Reference manual
    • Blueprint
    • API docs
      • @@ -23,7 +26,10 @@
        +
      • About
      • Tutorial
        • +
      • Roadmap
        • +
      • Get involved
      • Reference manual
      • Blueprint
      • API docs
        • diff --git a/web/Main.lean b/web/Main.lean index 77c36cf..09906d5 100644 --- a/web/Main.lean +++ b/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" diff --git a/web/README.md b/web/README.md index ae5c07a..d8881d2 100644 --- a/web/README.md +++ b/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. diff --git a/web/Site.lean b/web/Site.lean index cc9adc1..3468b1a 100644 --- a/web/Site.lean +++ b/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 diff --git a/web/Site/About.lean b/web/Site/About.lean new file mode 100644 index 0000000..d1433ce --- /dev/null +++ b/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/). diff --git a/web/Site/Components.lean b/web/Site/Components.lean index 75180af..717a2ec 100644 --- a/web/Site/Components.lean +++ b/web/Site/Components.lean @@ -19,6 +19,100 @@ open Verso.Web Components namespace Site +/-- The list of a page's sections, beside the text; the contents of the directive are a list of links. -/ +block_component +directive pageToc where + toHtml _ _ _ goB contents := do + return {{ }} + +/-- +A section heading with a fixed anchor, the target of a `pageToc` link. The directive has no contents; +the text of the section follows it. +-/ +block_component +directive anchoredHeading (anchor : String) (heading : String) where + toHtml _ _ _ _ _ := do + return {{

        {{ heading }}

        }} + +/-- Text beside the causal-diamond diagram; the argument is the diagram's caption. -/ +block_component +directive sideFigure (caption : String) where + toHtml _ _ _ goB contents := do + return {{ +
        +
        {{ ← contents.mapM goB }}
        +
        + {{ diamondDiagram }} +
        {{ caption }}
        +
        +
        + }} + +/-- The steps of a contribution, as a numbered row. -/ +def contributeStepList : Array (String × String) := #[ + ("Set up Lean", "Install Lean, clone the repository and build the library."), + ("Write it in the blueprint", "State the result and its informal proof, with its dependencies."), + ("Prove it in Lean", "Add the declaration to the library and link it to its blueprint entry."), + ("Open a pull request", "It is merged once it passes all status checks, has no conflicts with main, and is approved by a reviewer.") +] + +/-- The row of numbered contribution steps. -/ +block_component +directive contributeSteps where + toHtml _ _ _ _ _ := do + let items : Array Html := contributeStepList.mapIdx fun i (title, desc) => {{ +
      • + + {{ title }} + {{ desc }} +
        • + }} + return {{
          {{ items }}
        }} + +/-- A line icon of the Get Involved cards, from its SVG path data. -/ +def cardIcon (path : String) : Html := {{ + +}} + +/-- The cards of the Get Involved page: icon path, title, description, link text and link. -/ +def contributeCardList : Array (String × String × String × String × String) := #[ + ("M4 5a2 2 0 0 1 2-2h14v16H6a2 2 0 0 0-2 2zM4 21a2 2 0 0 1 2-2h14v2", + "Learn the library", "The tutorial introduces AQFT and Lean, with worked examples and exercises.", + "Read the tutorial", tutorialPath), + ("M6 2h9l5 5v15H6zM15 2v5h5M9 12h8M9 16h8", + "See what is stated", "The blueprint gives every definition and theorem in mathematical prose, linked to its Lean.", + "Open the blueprint", blueprintUrl), + ("M8 6a3 3 0 1 1-3-3 3 3 0 0 1 3 3zM8 18a3 3 0 1 1-3-3 3 3 0 0 1 3 3zM22 18a3 3 0 1 1-3-3 3 3 0 0 1 3 3zM5 9v6M19 15V9a3 3 0 0 0-3-3h-4", + "Contribute on GitHub", "The source of the library, the blueprint and this website, developed in public.", + "Go to the repository", githubUrl) +] + +/-- The grid of cards of the Get Involved page, in the style of the landing page's feature cards. -/ +block_component +directive contributeCards where + toHtml _ _ _ _ _ := do + let cards : Array Html := contributeCardList.map fun (icon, title, desc, label, url) => {{ + +
        + {{ cardIcon icon }} +

        {{ title }}

        +

        {{ desc }}

        +
        +
        {{ label }}" →"
        +         + }} + return {{
        {{ cards }}
        }} + +/-- A coloured band with a heading, the contents of the directive and a button. -/ +block_component +directive callout (heading : String) (label : String) (url : String) where + toHtml _ _ _ goB contents := do + return {{ + + }} + /-- The hero: wordmark, tagline, the contents of the directive (one sentence), the three call-to-action buttons, and the causal-diamond diagram. diff --git a/web/Site/Diagram.lean b/web/Site/Diagram.lean index 8b2f580..88baed0 100644 --- a/web/Site/Diagram.lean +++ b/web/Site/Diagram.lean @@ -9,7 +9,10 @@ used in the tutorial only. Both are 1+1-dimensional (time up, space to the right The landing-page diagram shows the setting of Axiom 3, local commutativity: a causal diamond `B` containing two smaller, spacelike-separated diamonds `B₁` and `B₂`. The dashed lines are the light cones of `B₁`: its causal future and past, which `B₂` avoids. Colours come from CSS classes in -`Site.Theme.siteCss`, so the diagrams follow light and dark mode. +`Site.Theme.siteCss`, so the diagrams follow light and dark mode. The repository's `README.md` cannot use +inline SVG or these classes, so it shows standalone copies of `diamondDiagram`, +`static_files/axiom3-diagram-light.svg` and `static_files/axiom3-diagram-dark.svg`; a change to the +diagram is made in those files too. -/ open Verso Output Html diff --git a/web/Site/GetInvolved.lean b/web/Site/GetInvolved.lean new file mode 100644 index 0000000..d184cf6 --- /dev/null +++ b/web/Site/GetInvolved.lean @@ -0,0 +1,30 @@ +import VersoBlog +import Site.Components + +open Verso Genre Blog +open Site + +#doc (Page) "Get Involved" => + +:::sideFigure "A result in the library: local commutativity on causal diamonds, Axiom 3 of the Haag–Kastler axioms." +Contributions are welcome. 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](tutorial/Doing-it-yourself/) explains how to set up Lean, add +a result to the blueprint and the library, and run the checks. +::: + +# From an idea to a pull request + +:::contributeSteps +::: + +# Where to start + +:::contributeCards +::: + +:::callout "Questions are welcome" "Visit the Lean Zulip" "https://leanprover.zulipchat.com/" +Ask on the Lean Zulip chat, or open an [issue](https://github.com/physicslib/physicslib4/issues) in the +repository. +::: diff --git a/web/Site/Links.lean b/web/Site/Links.lean index 588ea76..1f6c1ca 100644 --- a/web/Site/Links.lean +++ b/web/Site/Links.lean @@ -4,8 +4,8 @@ The website is published at the root of the project site, `/physicslib4/`, with the tutorial and the reference manual beneath it, at `/physicslib4/tutorial/` and `/physicslib4/manual/`. Every page of each carries a `` pointing at its own root, so the relative paths below resolve to the -same place from every page: `tutorial/` and `manual/` from the website, `../` (the website) and -`../tutorial/` or `../manual/` (the other book) from the books. +same place from every page: `tutorial/`, `manual/` and `about/` from the website, `../` (the website), +`../about/` and `../tutorial/` or `../manual/` (the other book) from the books. -/ namespace Site @@ -59,25 +59,45 @@ def manualChapterUrl (slug : String) : String := manualPath ++ slug ++ "/" /-- The website root, relative to the root of a book. -/ def siteFromBook : String := "../" +/-- The About page, relative to the root of the website. -/ +def aboutPath : String := "about/" + +/-- The Roadmap page, relative to the root of the website. -/ +def roadmapPath : String := "roadmap/" + +/-- The Get Involved page, relative to the root of the website. -/ +def getInvolvedPath : String := "get-involved/" + +/-- The documentation links of the footer, given the roots of the tutorial and the reference manual. -/ +def docLinksFrom (tutorialRoot manualRoot : String) : Array (String × String) := #[ + ("Tutorial", tutorialRoot), + ("Reference manual", manualRoot), + ("Blueprint", blueprintUrl), + ("API docs", docsUrl) +] + /-- -The navigation links, in order, given the paths of the roots of the tutorial and the reference -manual relative to the current root. Used by the header and the footer of the website and the -books. +The navigation links, in order, given the path of the website's root and the paths of the roots of +the tutorial and the reference manual, all relative to the current root. Used by the header of the +website and the books. -/ -def navLinksFrom (tutorialRoot manualRoot : String) : Array (String × String) := #[ +def navLinksFrom (siteRoot tutorialRoot manualRoot : String) : Array (String × String) := #[ + ("About", siteRoot ++ aboutPath), ("Tutorial", tutorialRoot), + ("Roadmap", siteRoot ++ roadmapPath), + ("Get involved", siteRoot ++ getInvolvedPath), ("Reference manual", manualRoot), ("Blueprint", blueprintUrl), ("API docs", docsUrl) ] /-- The navigation links of the website. -/ -def navLinks : Array (String × String) := navLinksFrom tutorialPath manualPath +def navLinks : Array (String × String) := navLinksFrom "" tutorialPath manualPath /-- The navigation links of the tutorial. -/ -def tutorialNavLinks : Array (String × String) := navLinksFrom "./" manualFromBook +def tutorialNavLinks : Array (String × String) := navLinksFrom siteFromBook "./" manualFromBook /-- The navigation links of the reference manual. -/ -def manualNavLinks : Array (String × String) := navLinksFrom tutorialFromBook "./" +def manualNavLinks : Array (String × String) := navLinksFrom siteFromBook tutorialFromBook "./" end Site diff --git a/web/Site/Roadmap.lean b/web/Site/Roadmap.lean new file mode 100644 index 0000000..3eb8ecb --- /dev/null +++ b/web/Site/Roadmap.lean @@ -0,0 +1,39 @@ +import VersoBlog +import Site.Components + +open Verso Genre Blog +open Site + +#doc (Page) "Roadmap" => + +# Two pillars + +physicslib4 is built around two pillars. + +*Pillar 1: Formalizing physics in Lean.* The first pillar is to solve Hilbert's sixth problem in +Lean 4, presenting physical theories axiomatically: algebraic quantum field theory, locally covariant +quantum field theory, topological quantum field theory, axiomatic quantum mechanics and others. The +goal is one library in which each theory has precise axioms and machine-checked consequences. + +*Pillar 2: Using AI to discover new physics.* A cycle of proof and revision that treats an axiom system +as a physical hypothesis to be tested and changed, centered on the theories of Pillar 1, such as AQFT and +LCQFT. Because every derivation is checked by machine, a conflict with observation cannot be put down to +a slip in the proof: it points at the axioms. The cycle has four steps: + +- *Derive.* AI systems prove theorems from a theory's axioms at a scale that hand derivation cannot match, + and Lean checks every one. The PCT and spin–statistics theorems of axiomatic quantum field theory show + the kind of consequence an axiom system can yield. + +- *Compare.* Each consequence is set against experiment. Some theorems reflect observation, and some do + not. Those that have not been tested are predictions. + +- *Revise.* A theorem that does not reflect observation implies that the axioms used to derive it are in + error. A formal proof names the hypotheses it depends on, which narrows the search for the axiom at + fault. AI proposes a weakened, strengthened or replaced axiom, and Lean reports every proof that the + change breaks. + +- *Re-derive.* AI repairs the broken proofs and derives the consequences of the revised axioms, and the + cycle begins again. + +Each pass through the cycle yields candidates for new physical foundations, the axioms, and new +consequences, their theorems. diff --git a/web/Site/Theme.lean b/web/Site/Theme.lean index 7e1426a..186e33e 100644 --- a/web/Site/Theme.lean +++ b/web/Site/Theme.lean @@ -228,6 +228,42 @@ a.feature-card:hover { border-color: var(--color-primary); box-shadow: 0 6px 18p .feature-card-more { color: var(--color-primary); font-size: var(--fs-sm); font-weight: 600; white-space: nowrap; transition: transform var(--transition-base); } a.feature-card:hover .feature-card-more { transform: translateX(3px); } +.post-content:has(.page-toc) { position: relative; } +.post-content h2[id] { scroll-margin-top: calc(var(--site-header-height) + var(--space-4)); } +.page-toc { position: absolute; left: calc(100% + var(--space-8)); top: 6rem; width: 12rem; } +@media (max-width: 1279px) { .page-toc { display: none; } } +.page-toc ul { list-style: none; margin: 0; padding: 0; } +.page-toc li { margin: 0 0 var(--space-4); } +.post-content .page-toc a { color: var(--color-text) !important; background: none !important; text-decoration: none; font-size: var(--fs-sm); } +.post-content .page-toc a:hover { color: var(--color-primary) !important; } + +.side-figure { display: grid; grid-template-columns: 1.5fr 1fr; gap: var(--space-8); align-items: center; } +.side-figure-image { margin: 0; } +.side-figure-image figcaption { font-size: var(--fs-sm); line-height: 1.45; color: var(--color-text-light); text-align: center; margin-top: var(--space-2); } + +.post-content ol.steps { list-style: none; margin: var(--space-6) 0 0; padding: 0; display: grid; grid-template-columns: repeat(4, 1fr); gap: var(--space-5); position: relative; } +.steps::before { content: ''; position: absolute; top: 1.2rem; left: 1.2rem; right: 25%; border-top: 2px solid var(--color-border-light); } +.post-content .steps li.step { display: flex; flex-direction: column; gap: var(--space-2); margin: 0; padding: 0; position: relative; } +.step-number { display: flex; align-items: center; justify-content: center; width: 2.4rem; height: 2.4rem; border-radius: 50%; + background: var(--testimonial-bg); color: var(--testimonial-text); font-weight: 700; } +.step-title { line-height: 1.3; margin-top: var(--space-2); } +.step-text { font-size: var(--fs-sm); line-height: 1.5; color: var(--color-text-light); } + +.contribute-grid { margin-top: var(--space-6); } +.post-content a.contribute-card { padding: var(--space-6); color: var(--color-text) !important; background: var(--card-bg) !important; } +.contribute-card .feature-card-text { margin: 0 0 var(--space-2); font-size: var(--fs-sm); } +.contribute-card .feature-card-text strong { font-size: var(--fs-base); } +.card-icon { display: block; width: 2rem; height: 2rem; margin-bottom: var(--space-3); fill: none; stroke: var(--color-primary); stroke-width: 1.6; stroke-linecap: round; stroke-linejoin: round; } +.dark-theme .card-icon { stroke: #5eead4; } + +.callout { display: flex; align-items: center; justify-content: space-between; gap: var(--space-6); margin-top: var(--space-12); + padding: var(--space-8); border-radius: var(--radius-lg); background: var(--testimonial-bg); color: var(--testimonial-text); } +.post-content .callout h3.callout-heading { margin: 0 0 var(--space-2); font-size: var(--fs-lg); color: inherit; } +.post-content .callout p { margin: 0; color: inherit; } +.post-content .callout-text a { color: inherit !important; text-decoration: underline; background: none !important; } +.post-content a.callout-button { flex: none; padding: var(--space-3) var(--space-6); border-radius: var(--radius-md); background: #fff !important; color: #0f766e !important; font-weight: 600; text-decoration: none; } +.post-content a.callout-button:hover { background: #ccfbf1 !important; } + .nav-item.active .nav-link { background-color: rgba(15, 118, 110, 0.12); color: var(--color-primary); } .dark-theme .nav-item.active .nav-link { background-color: rgba(45, 212, 191, 0.16); color: #5eead4; } .dark-theme .nav-link:hover { color: #5eead4; } @@ -236,6 +272,11 @@ a.feature-card:hover .feature-card-more { transform: translateX(3px); } @media (max-width: 900px) { .landing-hero { grid-template-columns: 1fr; padding-top: var(--space-10); } .feature-grid { grid-template-columns: 1fr; } + .side-figure { grid-template-columns: 1fr; } + .side-figure-image { max-width: 280px; justify-self: center; } + .post-content ol.steps { grid-template-columns: 1fr; } + .steps::before { display: none; } + .callout { flex-direction: column; align-items: flex-start; } } " @@ -266,6 +307,8 @@ header.site-header .nav-link { font-family: var(--font-primary); font-size: 0.9r padding: var(--space-3) var(--space-4); margin: 0; } header.site-header .nav-link svg { width: 20px; height: 20px; } header.site-header .nav-toggle-label { font-size: var(--fs-xl); line-height: 1.2; padding: var(--space-3); } +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) { header.site-header { background-color: var(--color-bg); } } @media (max-width: 768px) { header.site-header .navbar { padding: 0 var(--space-2); } } " @@ -311,13 +354,18 @@ def headerWith (home : String) (links : Array (String × String)) (isActive : St }} -/-- The website header. No navigation entry is active: each one leads out of the website. -/ -def header : Html := - headerWith "./" navLinks fun _ => false +/-- +The website header on the page at `path`. The entry of the current page is active; the entries of +the books, the blueprint and the API docs lead out of the website. +-/ +def header (path : Array String) : Html := + let current := path[0]?.map (· ++ "/") + headerWith "./" navLinks fun title => + navLinks.any fun (t, u) => t == title && some u == current /-- -The footer shared by the website and the books, using the `verso-web-components` footer classes. -`home` and `links` are as in `headerWith`. +The footer of the website, using the `verso-web-components` footer classes. `home` is as in +`headerWith`; `links` are the documentation links. -/ def footerWith (home : String) (links : Array (String × String)) : Html := let link (title url : String) : Html := @@ -337,6 +385,9 @@ def footerWith (home : String) (links : Array (String × String)) : Html :=