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.
Published:
In this blog post we will state and prove the GNS Construction Theorem, which we make extensive use of in subsequent blog posts.
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.
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.
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.