{"id":"90acaca7-12d0-449d-a927-ae09ef5b364c","arxiv_id":"2505.07939","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper announces a machine-checked Lean 4 formalization of Wick's theorem in its static, standard, and normal-ordered versions, as part of PhysLean.","lead":"This paper reports a machine-checked version of Wick's theorem, a standard quantum field theory result, written in the Lean 4 proof assistant. It matters as groundwork for making perturbative quantum field theory and Feynman diagrams formally reliable and reusable.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The formalized theorems are stated only for the quotient WickAlgebra, and the paper's claim that this covers the physical operator algebra O rests on an unproved and apparently unformalized universality assertion in Section 2.","rationale":"The strongest claim is the existence of a machine-checked formalization. The paper's own Section 2 narrows the formalization to WickAlgebra and only asserts, without proof, that O follows via universality. Since the paper's advertised subject is the quantum-field-theoretic Wick theorem, this transfer step is where the central claim could overstate what was digitized. I do not see an internal contradiction in the quotient proof, and the paper gives substantial structural evidence (52 files, 193 definitions, 929 lemmas, release-tagged repository) that the formalization is real. Thus the correct disposition is unchanged from the reader: conditional acceptance pending verification of the transfer/universality theorem, or an explicit scope-lowering to 'Wick's theorems in WickAlgebra'. The proposed build-and-search test would settle whether the transfer is in fact formalized, or whether the claim should be weakened.","tokens_in":7990,"tokens_out":13714,"duration_ms":142877,"concrete_test":"Checkout PhysLean release tag v4.18.0, run `lake build`, and search the code for an explicit lift/universal-property declaration, e.g. a theorem stating that any C-algebra with a `CrAnFieldOp` representation satisfying the four Section 2 supercommutator conditions admits a unique algebra homomorphism from `WickAlgebra` that intertwines the quotient supercommutator and, where defined, the time/normal-ordering maps. If no such theorem exists, verify whether Section 2's 'simple consequence' is only a paper-level claim and request a correction of the claimed scope; if it does exist, record its statement and confirm it matches the four conditions.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 2 defines WickAlgebra as a quotient of FieldOpFreeAlgebra by four supercommutator conditions, and Section 5 states the three Wick theorems only in this quotient. The manuscript then asserts that WickAlgebra 'satisfies the relevant universality conditions to ensure that Wick's theorem in O (however it is defined) is a simple consequence thereof.' No universal property, no map WickAlgebra → O, and no theorem statement to this effect is given; Section 6's proof overview only describes lemmas about WickAlgebra itself. Since physical time-ordering and normal-ordering are not in general well-defined linear maps on an interacting field algebra, the transfer is not a formality. If the claimed transfer theorem is absent from the Lean repository, the digitalization does not cover the ordinary QFT version of Wick's theorem, even though the introduction presents it as the theorem of perturbative QFT. The concern is not that the quotient proof is wrong; it is that its scope is narrower than claimed and the bridge to O is asserted rather than checked.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":8121,"tokens_out":12800,"duration_ms":136723,"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":[{"comment":"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":"Section 2 and Section 5"},{"comment":"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":"Section 1 and footnote 1"},{"comment":"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.","section":"Section 3 and Section 5"}],"minor_comments":[{"comment":"The word \"prominant\" appears twice and should be \"prominent\".","section":"Section 1"},{"comment":"The text contains typos \"supercommuator\" and \"containg\"; these should be \"supercommutator\" and \"containing\".","section":"Section 2"},{"comment":"The phrase \"in the the <WickContraction> directory\" has a duplicated article.","section":"Section 4"},{"comment":"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":"Section 5"},{"comment":"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.","section":"Section 6.2"}],"recommendation":"major_revision","confidential_remarks":"I have not independently inspected the repository at the cited URL; my assessment is based on the manuscript alone. If the repository is complete, the main remaining issue is the unsupported scope claim about the physical operator algebra O. The paper is closer to a research announcement than to a full formalization paper, so the editor may wish to confirm that this format is appropriate for the journal."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nThe 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.\n\nThe 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.\n\nSecond, 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.\n\nMinor: self-citation to the author's own PhysLean/HepLean appears, but it is not the load-bearing part of the argument.\n\nOverall, 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.","headline":"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.","tokens_in":8695,"tokens_out":2092,"would_cite":false,"duration_ms":20379,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B35","68V20","81T15","81T18"],"pacs":[],"model":"deepseek-v4-flash","headline":"Three versions of Wick's theorem now have machine-checked proofs in an interactive theorem prover.","keywords":["Wick's theorem","formal verification","interactive theorem proving","normal ordering","time ordering","supercommutator","quantum field theory","Feynman diagrams"],"falsifier":"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.","tokens_in":7729,"feed_emoji":"✅","tokens_out":8098,"duration_ms":70147,"temperature":0.7,"pith_summary":"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.","feed_headline":"Wick's theorem now has machine-checked proofs","feed_subtitle":"All three versions—static, standard, and normal-ordered—are formalized in an interactive theorem prover.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the original statement of Wick's theorem that the formalization targets.","marker":"[1]"},{"why":"Provides the interactive theorem prover in which the statements and proofs are checked.","marker":"[3]"},{"why":"Supplies the mathematical library that the formalization builds on.","marker":"[4]"},{"why":"Is the project repository where the formalized Wick theorem code lives.","marker":"[5]"}],"fun_headline_variants":["Wick's theorem, now in Lean 4","Machine-checked Wick's theorem","All of Wick's theorem, verified","Lean 4 proves Wick's theorem","Wick's theorem, digitally certified"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Wick's theorem, now in Lean 4","Machine-checked Wick's theorem","All of Wick's theorem, verified","Lean 4 proves Wick's theorem","Wick's theorem, digitally certified"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000221,"raw_usage":{"total_tokens":1361,"prompt_tokens":768,"completion_tokens":593,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":384,"completion_tokens_details":{"reasoning_tokens":530}},"tokens_in":384,"tokens_out":593,"duration_ms":5232,"temperature":1.0,"reasoning_tokens":530,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T22:07:19.893664+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Physlean: Digitalising physics into lean 4","cited_arxiv_id":null,"evidence_quote":"Is the project repository where the formalized Wick theorem code lives."}],"review_version":1}