Digitalizing Wick's theorem

Joseph Tooby-Smith

REVIEW 3 major objections 5 minor 1 cited by

Digitalizing Wick's theorem

T0 review · 3 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Three versions of Wick's theorem now have machine-checked proofs in an interactive theorem prover.

desk verdict Credible Lean 4 formalization of Wick's theorem in an abstract quotient algebra, but the advertised bridge to the physical operator algebra O is asserted, not formalized. read the letter →

arxiv 2505.07939 v1 pith:ASRBKQQM submitted 2025-05-12 hep-th cs.LO

Joseph Tooby-Smith This is my paper · ORCID

classification hep-thcs.LO MSC 03B3568V2081T1581T18

keywords Wick'stheoremformalverificationinteractiveprovingnormalorderingtimesupercommutatorquantumfieldtheoryFeynmandiagrams

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper announces that the static, standard, and normal-ordered versions of Wick's theorem have been stated and proved inside an interactive theorem prover, as part of an open-source library of formalized physics. The author's aim is to show that a cornerstone of perturbative quantum field theory can be turned into a fully formal, machine-checked mathematical result, and that the formalization can serve as a reusable foundation for future work on Feynman diagrams. The mathematical insight is a formulation of the theorem adapted to theorem proving: a quotient algebra built from creation and annihilation operators, governed by four supercommutator conditions, together with a computable data structure for Wick contractions. If the claims are correct, this is the first time the Wick theorems have been checked by any theorem prover.

What carries the argument

The central object is the Wick algebra: the free complex algebra on creation and annihilation field operators quotiented by four supercommutator conditions. The argument is carried by the data structure of a Wick contraction, defined as a finite set of disjoint unordered pairs of positions in a list of field operators, together with its sign, its static contraction, and its time contraction. The proof of the standard version proceeds by induction on the list length: pull out the operator with the latest time, expand the remaining time-ordered product by the induction hypothesis, and reassemble the two resulting sums into a single sum over all Wick contractions using an insertion constructor. The normal-ordered version follows from the standard version combined with a split of equal-time contractions and a lemma that rewrites time-ordered normal-ordered products using the static theorem.

What would settle it

Inspect the published code for a proven transfer statement: if no lemma connects the abstract quotient algebra to a concrete operator algebra, then the digitalized theorem has not been shown to cover ordinary quantum field theory. Alternatively, exhibit a standard field theory whose operator algebra satisfies the four conditions but fails one of the three Wick identities, which would show the conditions are insufficient to force the theorem.

Watch

Extended reading notes

Core claim

The central discovery is that all three versions of Wick's theorem can be expressed and proved in one quotient algebra, called the Wick algebra, generated by creation and annihilation parts of field operators and quotiented by four supercommutator conditions: two creations supercommute to zero, two annihilations supercommute to zero, mixed boson-fermion pairs supercommute, and supercommutators lie in the center. In this algebra the paper proves, with machine-checked proofs, that any product of field operators equals a signed sum over Wick contractions of static contractions times normal-ordered uncontracted products; that the time-ordered product equals the analogous sum using time contractions; and that the time-ordered normal-ordered product equals the same sum restricted to contractions in which no contracted pair has equal time. The paper claims these four conditions are the minimal assumptions needed for Wick's theorem, and that universality conditions make the theorem in any physical operator algebra a consequence of the quotient-algebra statement.

Load-bearing premise

The load-bearing premise is that the abstract algebra defined by the paper's four supercommutator conditions captures exactly the algebraic structure of a physical field-operator algebra, so that a proof in that quotient algebra transfers to the operators used in quantum field theory.

Editorial extensions

If this is right

Physicists and mathematicians can build on a machine-checked statement of Wick's theorem, so derivations that use it inherit a guarantee of correctness rather than relying on manual sign bookkeeping.
The three versions of the theorem are proved in a single framework, allowing calculations that mix static, standard, and normal-ordered identities to be combined without re-proving their relationship.
Wick contractions are defined as a computable data structure, so the theorem is not only a statement but also an algorithm that can be run on lists of operators.
The surrounding library of definitions and lemmas provides a reusable foundation for the formalization of Feynman diagrams, which the paper identifies as the next step.
Because the proof isolates the minimal algebraic assumptions, the same formal infrastructure can be applied to other ordering identities in quantum field theory.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural test is to apply the same quotient-algebra strategy to other ordering identities, such as the operator product expansion or the Dyson series, and see whether the same four supercommutator conditions suffice.
If the transfer assumption holds generally, then any identity that follows purely from supercommutator relations and ordering rules could in principle be formalized without choosing a concrete Hilbert-space representation.
The equal-time restriction in the normal-ordered version appears to mirror the diagrammatic rule that equal-time contractions in time-ordered normal products drop out; the formal proof's sign handling may clarify edge cases in textbook treatments.
The paper argues for universality but does not display the transfer proof here; a reader intending to use the result in an ordinary QFT calculation should verify that the concrete operator algebra satisfies the four conditions.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

You should know this paper is not a new physics result; it is a machine-checked formalization announcement. The theorems themselves are classical (Wick 1950). What is new is the Lean 4 formalization, which is substantial on its face: 52 files, 193 definitions, 929 lemmas, covering three versions of Wick's theorem and a computable contraction API. If the code checks out, it is a genuine infrastructure contribution to PhysLean and a plausible foundation for future formalization of Feynman diagrams.

The paper does several things well. It is explicit about the design choice to work in an abstract algebra, WickAlgebra, defined as a quotient of a free algebra by four supercommutator conditions. That is a sensible way to isolate the minimal assumptions. The proof overview in Section 6 is coherent and tracks the standard recursive argument; the sign handling is described carefully. The code is pinned to a release tag, so the artifact is at least findable.

The main soft spot is the transfer claim. Section 2 says WickAlgebra "satisfies the relevant universality conditions to ensure that Wick's theorem in O (however it is defined) is a simple consequence thereof," but no universal property, no map WickAlgebra → O, and no theorem statement to that effect are given. Section 6's proof overview only discusses lemmas about WickAlgebra itself. For interacting QFT, time-ordering and normal-ordering are not in general well-defined linear maps on the field operator algebra, so the transfer is not a formality. The stress-test note is right: the digitalization covers the quotient algebra, not necessarily the ordinary QFT version of Wick's theorem, despite the introduction's framing. The paper should either formalize the transfer or explicitly state that the O-version is future work.

Second, no Lean code appears in the manuscript, no compile log, and no commit hash. A release tag is better than nothing, but readers cannot verify the central claim from the paper alone. That matters because the selling point is machine-checked correctness.

Minor: self-citation to the author's own PhysLean/HepLean appears, but it is not the load-bearing part of the argument.

Overall, the formalization is real and likely correct, but the paper overreaches in its universality claim. It will be useful to people working on formal verification of physics, less to physicists who want a proof of Wick's theorem as used in QFT. I would send it to peer review, but with a clear request for either a formalized transfer theorem or an explicit scope limitation, plus a buildable artifact. It deserves a serious referee.

Referee Report

3 major / 5 minor

Summary. The paper announces the formalization in Lean 4 of three versions of Wick's theorem — static, standard, and normal-ordered — within the author's PhysLean library. It introduces a quotient algebra WickAlgebra generated by creation/annihilation field operators modulo four supercommutator conditions, defines algebraic time-ordering and normal-ordering maps on this quotient, defines Wick contractions and their associated signs and contraction terms, states the three theorem statements, and provides a proof overview. The paper does not reproduce the formal proof; instead it points to a release tag of the PhysLean repository and to interactive notes. All three theorem statements are made in WickAlgebra, not in a general physical operator algebra.

Significance. If the Lean repository at the cited release contains the claimed declarations and proofs, this is a useful and credible step toward machine-checked perturbative quantum field theory. The design of Wick contractions as a computable data structure, the 929-lemma API, and the public availability of the code are concrete strengths, and the formalization is not fitted to data. The significance is currently conditional, however, because the paper's bridge from WickAlgebra to the ordinary operator algebra O is only asserted, and because the manuscript itself does not include the formal theorem statements. As written, the result is narrower than the abstract: it establishes Wick's theorem for the quotient WickAlgebra, not for a general physical operator algebra. With the scope clarified, the paper would be a valuable announcement for the formalization community and for physicists using Lean.

major comments (3)

[Section 2 and Section 5] The claim that WickAlgebra "satisfies the relevant universality conditions to ensure that Wick's theorem in O (however it is defined) is a simple consequence thereof" is load-bearing but unsupported: no universal property, no map from WickAlgebra to O, and no transfer theorem are stated or referenced, and the three theorem statements in Section 5 are all explicitly "in the algebra WickAlgebra". Because physical time-ordering and normal-ordering are not automatically well-defined linear maps on an arbitrary field algebra, this transfer is not a routine corollary. Please either formalize and report the transfer theorem, or revise the abstract and introduction to state that the digitalization covers Wick's theorem in WickAlgebra and that passage to O is future work.
[Section 1 and footnote 1] The paper's central claim is that the three theorems and their proofs have been checked by Lean, but the manuscript includes no Lean code, no quoted declarations, and no compile log; it only gives a release-tag URL. Since the paper explicitly says it will not give the full details of the formalization, the reader cannot verify the main claim from the manuscript. Please include the exact Lean statements of the three theorems, and ideally a build log or commit hash, so that the announcement is self-contained enough to be checked.
[Section 3 and Section 5] The definition of the time-ordering relation is a preorder rather than a linear order: for two position operators with equal time, timeOrderRel holds in both directions, and the normal-ordering relation similarly leaves multiple creation-creation or annihilation-annihilation pairs unordered. The paper says the map is obtained by insertion sort, but it does not specify the tie-breaking rule; the statement of the normal-ordered version in Section 5, which restricts contractions using HaveEqTime, depends on this convention. Please state the exact ordering relation, or the exact algorithm, used in the formalization, including equal-time cases.

minor comments (5)

[Section 1] The word "prominant" appears twice and should be "prominent".
[Section 2] The text contains typos "supercommuator" and "containg"; these should be "supercommutator" and "containing".
[Section 4] The phrase "in the the <WickContraction> directory" has a duplicated article.
[Section 5] The predicate HaveEqTime is only explained parenthetically; please give its formal definition in a displayed equation or provide a precise reference to its definition in the code.
[Section 6.2] The first displayed equation for timeOrder_haveEqTime_split has a stray "ϕssucΛ" at the end of the first line, and the notation is hard to parse; please reformat it cleanly.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the Lean-formalized Wick theorems are proved in a quotient algebra under explicit axioms, with no fitted inputs and no load-bearing self-citation chain.

full rationale

The paper's derivation chain is self-contained against an external proof kernel. The three Wick theorems are stated as Lean propositions in WickAlgebra, defined as a quotient of FieldOpFreeAlgebra by four explicit supercommutator conditions (Section 2), and the proof overview in Section 6 derives them from properties of ordering maps, Wick contractions, and constructors such as insertAndContract and join, not from the theorem statements themselves. No fitted parameter is renamed as a prediction, and no uniqueness theorem is imported from the author's prior work to force a choice. The citations to [5] PhysLean and [6] HepLean are contextual references to the repository and predecessor project, not load-bearing evidence for the mathematical content, which is machine-checked. The only notable gap is a scope assertion rather than a circular step: Section 2 states that WickAlgebra 'satisfies the relevant universality conditions to ensure that Wick's theorem in O (however it is defined) is a simple consequence thereof,' but no universal map or formalized transfer theorem is exhibited. That is an unsupported breadth claim about physical applicability, not a reduction of the formalized result to its own input, and therefore does not raise the circularity score. The static, standard, and normal-ordered theorems in the quotient retain independent combinatorial content; defining timeContract as T(phi*psi) - N(phi*psi) makes the single-pair case a definitional identity, but the multi-field identities are proved rather than assumed.

Assumptions & free parameters 0 free parameters · 5 assumptions · 1 invented entities

The formalization introduces a new quotient algebra, WickAlgebra, based on four supercommutator axioms, plus a specific decomposition of fields into creation and annihilation parts. These are domain assumptions rather than fitted parameters. The reliability of the central claim depends on the transfer from WickAlgebra to physical operator algebras and on the soundness of Lean and Mathlib. There are no free parameters fitted to data.

assumptions (5)

standard math Lean 4 type theory and Mathlib are sound enough for the formalized statements to mean what the paper claims.
Every Lean proof depends on the kernel; the paper does not justify the foundation, and no formalization can rule out kernel bugs.
domain assumption The four supercommutator conditions in Section 2 define the correct minimal algebraic setting for Wick's theorem.
WickAlgebra is the quotient by these conditions; Wick's theorem is proved in this algebra, so any physics application inherits this assumption.
domain assumption CrAnFieldOp splits position operators into exactly one creation and one annihilation part, with the stated asymptotic behavior.
This decomposition is hard-wired into the normal-ordering map and static contractions; physical fields that do not split this way are not covered.
domain assumption The claimed universality transfer from WickAlgebra to any operator algebra O is valid.
The paper asserts universality in Section 2 but does not include the formal transfer proof in the manuscript; it is essential for the physical interpretation.
domain assumption The normal-ordered version's restriction to contractions with no equal-time contracted pair exactly matches the intended physical statement.
The paper defines the restriction with HaveEqTime and asserts this is the normal-ordered Wick theorem; the equivalence to textbook statements is not fully demonstrated in the text.

invented entities (1)

WickAlgebra
purpose: A quotient algebra used as the minimal setting in which the three Wick theorems are stated and proved in Lean.
This is a new mathematical object introduced by the paper, not a physical particle or force. It is constructive and computable in Lean, but the paper provides no empirical falsifiable prediction associated with it.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Digitalizing Wick's theorem." pith.science (2026). https://pith.science/paper/ASRBKQQM

@misc{pith2026250507939,
  author       = {Pith},
  title        = {Pith review of: Digitalizing Wick's theorem},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ASRBKQQM}},
  note         = {Machine review of arXiv:2505.07939}
}

read the original 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

Figures reproduced from arXiv: 2505.07939 by the authors.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Algebraic versus physical uniqueness of MHV gravity numerators
hep-th 2026-08 conditional novelty 7.0 of 10 partial

Pair-zero and degree conditions admit extra six-dimensional hook solutions at seven points and a two-dimensional plane at eight; Bose symmetry and one normalized physical boundary condition single out the Hodges numerator.

Reference graph

Works this paper leans on

11 extracted references · 4 canonical work pages · cited by 1 Pith paper

[1]

G. C. Wick. The evaluation of the collision matrix. Phys. Rev., 80:268–272, Oct 1950. URL: https://link.aps.org/doi/10.1103/PhysRev.80.268, doi:10.1103/PhysRev.80.268. 10

doi:10.1103/physrev.80.268 1950
[2]

Notes on Wick’s theorem in many-body theory, 2023

Luca Guido Molinari. Notes on Wick’s theorem in many-body theory, 2023. URL: https:// arxiv.org/abs/1710.09248, arXiv:1710.09248

arXiv 2023
[3]

The Lean theorem prover (system description)

Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th Interna- tional Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015 , pages 378–388. Springer, 2015. doi:10.1007/978-3-319-21401-6_26

doi:10.1007/978-3-319-21401-6_26 2015
[4]

The Lean mathematical library

The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIG- PLAN International Conference on Certified Programs and Proofs , CPP 2020, pages 367–381. Association for Computing Machinery, 2020. doi:10.1145/3372885.3373824

arXiv 2020
[5]

Physlean: Digitalising physics into lean 4

The PhysLean Community. Physlean: Digitalising physics into lean 4. GitHub repository. URL: https://github.com/HEPLean/PhysLean

work page
[6]

HepLean: Digitalising high energy physics

Joseph Tooby-Smith. HepLean: Digitalising high energy physics. Comput. Phys. Commun. , 308:109457, 2025. arXiv:2405.08863, doi:10.1016/j.cpc.2024.109457

arXiv 2025
[7]

Formalizing chemical physics using the lean theorem prover

Maxwell P Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M Wraback, and Tyler R Josephson. Formalizing chemical physics using the lean theorem prover. Digital Discovery, 3(2):264–280, 2024. doi:/10.1039/D3DD00077J

doi:10.1039/d3dd00077j 2024
[8]

Scilean: Scientific computing assistant

Tomáš Sk ˇrivan. Scilean: Scientific computing assistant. GitHub repository. URL: https:// github.com/lecopivo/SciLean

work page

Show all 11 references

[9]

Joachim Breitner. loogle. GitHub repository. URL: https://github.com/nomeata/loogle
[10]

Ai achieves silver-medal standard solving international mathe- matical olympiad problems, 2024

Google DeepMind. Ai achieves silver-medal standard solving international mathe- matical olympiad problems, 2024. URL: https://deepmind.google/discover/blog/ ai-solves-imo-problems-at-silver-medal-level/

2024
[11]

Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. 2023. arXiv:2306.15626

2023 arXiv

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.

[1] [1]

G. C. Wick. The evaluation of the collision matrix. Phys. Rev., 80:268–272, Oct 1950. URL: https://link.aps.org/doi/10.1103/PhysRev.80.268, doi:10.1103/PhysRev.80.268. 10

doi:10.1103/physrev.80.268 1950

[2] [2]

Notes on Wick’s theorem in many-body theory, 2023

Luca Guido Molinari. Notes on Wick’s theorem in many-body theory, 2023. URL: https:// arxiv.org/abs/1710.09248, arXiv:1710.09248

arXiv 2023

[3] [3]

The Lean theorem prover (system description)

Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th Interna- tional Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015 , pages 378–388. Springer, 2015. doi:10.1007/978-3-319-21401-6_26

doi:10.1007/978-3-319-21401-6_26 2015

[4] [4]

The Lean mathematical library

The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIG- PLAN International Conference on Certified Programs and Proofs , CPP 2020, pages 367–381. Association for Computing Machinery, 2020. doi:10.1145/3372885.3373824

arXiv 2020

[5] [5]

Physlean: Digitalising physics into lean 4

The PhysLean Community. Physlean: Digitalising physics into lean 4. GitHub repository. URL: https://github.com/HEPLean/PhysLean

work page

[6] [6]

HepLean: Digitalising high energy physics

Joseph Tooby-Smith. HepLean: Digitalising high energy physics. Comput. Phys. Commun. , 308:109457, 2025. arXiv:2405.08863, doi:10.1016/j.cpc.2024.109457

arXiv 2025

[7] [7]

Formalizing chemical physics using the lean theorem prover

Maxwell P Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M Wraback, and Tyler R Josephson. Formalizing chemical physics using the lean theorem prover. Digital Discovery, 3(2):264–280, 2024. doi:/10.1039/D3DD00077J

doi:10.1039/d3dd00077j 2024

[8] [8]

Scilean: Scientific computing assistant

Tomáš Sk ˇrivan. Scilean: Scientific computing assistant. GitHub repository. URL: https:// github.com/lecopivo/SciLean

work page