There’s a new paper out on the Formalization of QFT, purporting to formalize a QFT using Lean/Mathlib. I’ve been trying to avoid spending time on the hot topics of AI and theorem proving, but in this case there’s a lot of overlap with what I have been thinking about recently (and written about here, see this blog posting).
The authors have been working at this since last July, and you can consult section 5 of the their paper to see the methods they used. The theorem they prove is that if you start with the usual two-point Schwinger function of a free scalar field
$$K(x,y)=\int_{\mathbf R^4}e^{ip(x-y)}\frac{1}{p^2+ m^2}d^4p$$
then you get a Euclidean quantum field theory that satisfies a certain set of axioms.
A basic problem with any claim to have “formalized QFT” is that we don’t actually have an accepted definition of what a QFT is. The authors take a definition from the book by Glimm and Jaffe: a probability measure on distributions satisfying five axioms labeled OS0-OS4. They need to do a lot of work to formalize the proof that you can construct a measure with these properties from $K(x,y)$. Such a proof though is quite standard and well-understood long ago. This is not a topic where there’s any concern that it might have some sort of subtle problem.
An obvious question is, why use this Glimm/Jaffe definition of what a QFT is? The use of “OS” refers to the original work on characterizing Euclidean QFTs of Osterwalder-Schrader. If you look at their paper, they characterize a Euclidean QFT as a set of Schwinger functions satisfying a set of axioms E0-E4 (they intended to show that these imply, after Wick rotation, the usual Wightman axioms). The OS paper doesn’t have anything to say about measures and while their axioms correspond to the Glimm/Jaffe ones, they are different.
Why not formalize the free scalar QFT using the Osterwalder-Schrader definition of a Euclidean QFT? The reason I think is that this would be too easy: the only axiom that the free Schwinger functions don’t obviously satisfy is the positivity one (recognizing the significance of this was the great contribution of OS). The argument for OS positivity of the free theory is straight-forward, but shows that something quite interesting is going on (I spent quite a bit of time trying to understand this in terms of hyperfunctions).
Just about all of the work in this particular formalization goes into putting the free field QFT into a specific measure-theoretical straight-jacket. This straight-jacket only fits the real scalar field QFT, possibly with self-interactions, doesn’t apply to the QFTs of relevance to fundamental physics (gauge fields, fermionic spinor fields, gauge interactions). The interesting thing about this class of QFTs is that they are basically statistical mechanical systems and can be studied with the techniques of probability theory. The problem is that they not only don’t correspond to any fundamental real world QFT, but that the only non-trivial examples are in two and three spacetime dimensions. We now have proofs that if you try and do this in four or more spacetime dimensions, you can only get free field theory.
The authors are aware of this, claim as one motivation formalizing Yang-Mills theory. By now there’s a 50 year history of people trying to follow this program of constructing a measure of some sort on gauge fields, showing a mass gap and getting a million dollars, but I don’t see any evidence this is going anywhere. New, very different ideas are surely needed. They also claim as motivation producing a measure on metrics that would give quantum gravity, but again fifty years of people trying to do this indicates that this is not at all a good starting point.
What’s most likely needed for further progress is the same thing that almost always ends up being needed for a big breakthrough when a field has been stuck for decades: a change in the question. In this case, one needs a different definition of QFT than as a measure on a space of distributions. Finding that new definition is the interesting problem, not reproving well-known implications of the definition that you know is not the right one.
The AI and formalization program that is being sold to us as the future of fundamental physics seems to me to come with a big danger. It may turn this field into nothing but an endless investigation of the blind alleys that are what we know about now and have been stuck at for decades. This particular “formalization of QFT” is an expedition headed down such a blind alley.
