Digitalizing Wick's theorem
arXiv:2505.07939
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.
10 pages. Associated code at https://github.com/HEPLean/PhysLean