This project attempts to formalise in Lean Algebraic Quantum Field Theory (AQFT) in Minkowski and curved spacetime. Important links:
- Landing Page
- GitHub Project Page
- Blueprint (web version)
- Dependency Graph (web version)
- Blueprint (PDF version)
- API Documentation
This project was started by Kelly Davis in June 2026. It is currently being maintained by Kelly Davis. Contributions welcome: see below for more details.
Should you wish to make any contributions to the content of the project, please add them to a new branch and make a pull request. Your PR will need to satisfy certain status checks, be approved by a reviewer and have no conflicts with the base branch before it can be merged.
We are grateful to all contributors for their effort. We would also like to thank the Mathlib maintainers and the Lean community for their support. Finally, we would like to thank Project Numina for their generosity in partially supporting this research.