From 12719db4e8f012ed8533295c89a3a8dffcd81be8 Mon Sep 17 00:00:00 2001 From: KellyJDavis Date: Sat, 31 Oct 2026 19:00:59 +0100 Subject: [PATCH 1/2] Polish the homepage wording - The tagline and the line beneath it state the project's wider aim. - "Checked by Lean" describes what each tab of examples proves. - The formalised-content section is titled "What is currently formalised". - The landing page's "About" section is removed; the About page covers it. Co-Authored-By: Claude Opus 5.5 --- web/Site/FrontPage.lean | 20 ++++++-------------- web/Site/Links.lean | 2 +- 2 files changed, 7 insertions(+), 15 deletions(-) diff --git a/web/Site/FrontPage.lean b/web/Site/FrontPage.lean index 449c971..d029f34 100644 --- a/web/Site/FrontPage.lean +++ b/web/Site/FrontPage.lean @@ -14,7 +14,7 @@ htmlId := some "frontpage" %%% :::hero -physicslib4 formalises algebraic quantum field theory in Lean 4. +A Lean 4 formalisation of axiomatic physical theories. ::: ```leanInit physicslib4 @@ -33,9 +33,10 @@ local notation:50 p:51 " ≺ " q:51 => ::::::centeredSection "example" "Checked by Lean" -As you will recall, a Poincaré transformation maps causal curves to causal curves, so it cannot change -which events can influence which. In the library this is a theorem, and the code below is elaborated -against it when the page is built. Hover over a name to see its type. +A Poincaré transformation maps causal curves to causal curves, so it cannot change which events can +influence which. In the library this is a theorem, proved in the first tab. The second tab proves +that a Haag–Kastler net exists, so the axioms are consistent. (Hover over a name to see its +type.) :::::gallery @@ -70,18 +71,9 @@ manual/Haag-Kastler-axioms-in-Minkowski-spacetime/ :::::: -::::::centeredSection "contents" "What is formalised" +::::::centeredSection "contents" "What is currently formalised" :::features ::: :::::: - -::::::centeredSection "about" "About" - -The blueprint is the specification of the project. It sharpens the 1964 Haag–Kastler axioms where the -original paper leaves details open, and states every definition and theorem in ordinary mathematical -prose, linked to the Lean declarations that realise it. Every formal statement is checked against the -blueprint, not against the 1964 paper, and the Lean contains no `sorry`. - -:::::: diff --git a/web/Site/Links.lean b/web/Site/Links.lean index 1f6c1ca..7f49fcf 100644 --- a/web/Site/Links.lean +++ b/web/Site/Links.lean @@ -11,7 +11,7 @@ same place from every page: `tutorial/`, `manual/` and `about/` from the website namespace Site /-- The tagline, shown under the wordmark and in the page metadata. -/ -def tagline : String := "A Lean 4 formalisation of the mathematical foundations of physics" +def tagline : String := "Solving Hilbert's 6th problem in Lean 4" /-- The project's GitHub repository. -/ def githubUrl : String := "https://github.com/physicslib/physicslib4" From 241fa92fc9cc608ae38be6811ea3d6792eb9945c Mon Sep 17 00:00:00 2001 From: KellyJDavis Date: Sat, 31 Oct 2026 19:02:03 +0100 Subject: [PATCH 2/2] Reword the README's diagram caption and opening Co-Authored-By: Claude Opus 5.5 --- README.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 7d4424b..3bf58cb 100644 --- a/README.md +++ b/README.md @@ -11,11 +11,13 @@ Official website at .

-

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

+

Algebraic quantum field theory's axiom 3 in one picture: the diamonds B₁ and B₂ are spacelike separated inside B, so their observables commute.

# What's physicslib4? -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. +physicslib4 aims to formalise axiomatic physical theories in the [Lean 4 theorem prover](https://leanprover-community.github.io). + +The library currently 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. ## Goal