Papers With

← All papers
First page of Digitalizing Wick's theorem

Digitalizing Wick's theorem

Joseph Tooby-Smith

hep-th May 12, 2025 · v1
formalization verification physics quantum
Read PDF arXiv abstract Code
TL;DR
Formalizes Wick's theorem and its normal-ordered and static variants in Lean 4 as part of the PhysLean project.
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.
Problem

Wick's theorem is a cornerstone of perturbative quantum field theory relating time-ordered and normal-ordered products of field operators, but it has not been formally verified in a proof assistant.

Approach

The authors digitalize Wick's theorem and its proof in Lean 4 as part of the PhysLean project. The formalization covers the operator algebra (FieldOpFreeAlgebra, WickAlgebra), time-ordering and normal-ordering maps, and the combinatorial structure of Wick contractions. Both the static and normal-ordered versions of Wick's theorem are formalized.

Results

The formalization provides machine-checked proofs of three versions of Wick's theorem (standard, static, and normal-ordered) in Lean 4. The type-theoretic representation of Wick contractions and the algebraic infrastructure are part of the PhysLean library.