Tutorial for the Lean 4 Library physicslib4
Published:
Blog posts
2026
Spectral Theorem for Unbounded, Self-Adjoint Operators
Published:
Here we will state and prove the Spectral Theorem for Unbounded, Self-Adjoint Operators. This theorem extends the Spectral Theorem for Bounded, Self-Adjoint Operators to the small handful of genuinely unbounded self-adjoint operators that do arise in AQFT — the momentum operator on Minkowski space is a standard example — even though the large majority of operators of interest there, local observables in particular, are bounded. It is a prerequisite for handling these unbounded operators within the rest of the AQFT work that motivated this series.
Spectral Theorem for Bounded, Self-Adjoint Operators
Published:
Here we will state and prove the Spectral Theorem for Bounded, Self-Adjoint Operators. This theorem sits at the core of much of AQFT, and extensive use of this theorem will be made in subsequent work.
Local Isometric Invariant States
Published:
This blog post introduces the notion of “isometric invariant states” in Algebraic Quantum Field Theory (AQFT) in Minkowski spacetime (a theory defined in Unpacking the Haag Kastler Axioms) and also does the same for AQFT in Lorentzian spacetime (a theory defined in Haag Kastler Axioms in Curved Spacetime). Such “isometric invariant states” capture the physics of quantum systems that are invariant under isometries of spacetime.
GNS Construction Theorem
Published:
In this blog post we will state and prove the GNS Construction Theorem, which we make extensive use of in subsequent blog posts.
Haag Kastler Axioms in Curved Spacetime
Published:
This blog post presents the axioms governing Algebraic Quantum Field Theory (AQFT) in curved spacetime, generalizing the axioms of AQFT in Minkowski spacetime from the blog post Unpacking the Haag Kastler Axioms.
Unpacking the Haag Kastler Axioms
Published:
The aim of this blog post is to “sharpen” the statement of the Haag Kastler axioms (Haag and Kastler). As originally presented they were revolutionary. However, several small details were left under-specified. This blog post will hopefully clarify some of these details.
Gödel’s Poetry: AI, Lean4 Prover
Published:
Gödel’s Poetry (PDF) is a Lean 4 system that combines specialized language models for proof generation with recursive decomposition of difficult theorems into simpler entailing propositions, coordinated through a multi-agent architecture as in the arXiv manuscript. Proof verification runs through the Kimina Lean Server; when direct proof generation (with verifier-guided self-correction in the style of Goedel-Prover-V2) does not yield a closed proof, the stack falls back to RAG-based theorem retrieval, proof sketching with sorry placeholders in explicit have obligations, AST-based extraction of those subgoals, recursive proof of each proposition, and finally proof reconstruction that substitutes verified sub-proofs back into the parent sketch.