Title: Progress towards Algebraic Quantum Field Theory in Isabelle/HOL
Speakers: Richard Schmoetten
Abstract:

Algebraic Quantum Field Theory (AQFT) is a topic in mathematical physics that aims to put the theories underlying modern particle physics on a solid axiomatic footing. This demand for rigour finds its natural continuation in the programme of formalisation of mathematics, gaining computer-checked certainty of correctness. The aim of my work is to conduct an investigation into a formalised theory of AQFT in Isabelle/HOL. Yet much of the mathematical context required for a meaningful definition of AQFT is missing from Isabelle’s libraries. During this talk, I report on progress we have made towards remedying this lack, and present formalisations in the theories of manifolds, Lie groups, and involutive algebras. I will then outline a plan to quickly obtain a minimal formalisation of AQFT, so that the study of theorems with physical interpretation can begin.