Digitalizing Wick's theorem

TL;DR

This work presents the digitalization of the three forms of Wick's theorem into Lean 4 as part of the PhysLean project, enabling machine-checked proofs of perturbative quantum field theory results. It constructs a computable algebraic framework, WickAlgebra, and a WickContraction data structure to capture contractions and their signs, supporting explicit, verifiable formulations of the static, standard, and normal-ordered theorems. The authors outline the core proof strategy and key lemmas that underlie the Lean formalizations, and point to a public codebase for interactive exploration. The formalization promises reliable reuse and integration with broader physics formalizations, potentially facilitating future formalizations of Feynman diagrams and related perturbative techniques.

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.

Figures (1)

• Figure 1: The types and algebras involved in the formalization of Wick's theorem.