Digitalizing Wick's theorem
High Energy Physics - Theory
2025-05-14 v1 Logic in Computer Science
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.
Cite
@article{arxiv.2505.07939,
title = {Digitalizing Wick's theorem},
author = {Joseph Tooby-Smith},
journal= {arXiv preprint arXiv:2505.07939},
year = {2025}
}
Comments
10 pages. Associated code at https://github.com/HEPLean/PhysLean