Skip to content

Polish the homepage wording #54

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
KellyJDavis merged 2 commits into from
Oct 31, 2026
Merged

Polish the homepage wording #54

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
12719db
Polish the homepage wording
KellyJDavis Oct 31, 2026
241fa92
Reword the README's diagram caption and opening
KellyJDavis Oct 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,13 @@ Official website at <https://physicslib.github.io/physicslib4/>.
</picture>
</p>

<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>
<p align="center"><em>Algebraic quantum field theory's axiom 3 in one picture: the diamonds B₁ and B₂ are spacelike separated inside B, so their observables commute.</em></p>

# 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

Expand Down
20 changes: 6 additions & 14 deletions web/Site/FrontPage.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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`.

::::::
2 changes: 1 addition & 1 deletion web/Site/Links.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
Loading