A Lean 4 library for axiomatic physics.
Official website at https://physicslib.github.io/physicslib4/.
Algebraic quantum field theory's axiom 3 in one picture: the diamonds B₁ and B₂ are spacelike separated inside B, so their observables commute.
physicslib4 aims to formalise axiomatic physical theories in the Lean 4 theorem prover.
The library currently covers algebraic quantum field theory: the Haag–Kastler axioms in Minkowski and curved spacetime, the GNS construction, spectral theory and Stone's theorem.
This project works towards a formal resolution of Hilbert's 6th problem: a rigorous mathematical treatment of the axioms underlying physical theories.
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.
Requires Lean 4 and Mathlib4, both at v4.35.0, as pinned by lean-toolchain and lakefile.toml.
git clone https://github.com/physicslib/physicslib4.git
cd physicslib4
lake exe cache get # download prebuilt dependencies
lake build # build the projectContributions are welcome; see Get Involved. 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; a pull request against main is merged once it passes all status checks, has no conflicts with main, and is approved by a reviewer.
We are grateful to Rudolf Haag and Daniel Kastler for their foundational work, and to the authors of Entanglement in Algebraic Quantum Field Theories 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.
Maintained by Kelly J Davis.