Digitalizing Wick's theorem

TL;DR

This paper presents the digitalization of Wick's theorem and its variants into the Lean 4 theorem prover, enhancing formal verification in quantum field theory.

Contribution

It introduces a formal proof of Wick's theorem and its versions within Lean 4, advancing the integration of quantum physics into interactive theorem proving.

Findings

Successful formalization of Wick's theorem in Lean 4

Implementation of static and normal-ordered versions

Enhanced tools for quantum field theory verification

Abstract

Wick's theorem is a cornerstone of perturbative quantum field theory. In this paper we announce and discuss the digitalization of Wick's theorem and its proof into the interactive theorem prover Lean 4 as part of the project PhysLean. We do the same for the static and normal-ordered versions of Wick's theorem.