# Digitalizing Wick's theorem

arXiv: https://arxiv.org/abs/2505.07939 · HTML: https://mlsanity.com/paper/2505.07939/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 May 2025.

## Built on by (most cited first, 1 of 1)

- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)

## Abstract (arXiv)

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.