Formalization of quantum field theory

Stream: Natural sciences

[Michael R Douglas]

We announce OSforGFF, a formalization of the construction of the Gaussian free field (in four dimensions) and the proof that it satisfies the Osterwalder-Schrader axioms. This is the starting point for constructive quantum field theory and an essential prerequisite for (among other things) formalizing the Yang-Mills Millennium problem.
The formalization is complete up to three assumed theorems including Minlos' theorem on construction of measures, and proves many general results in functional analysis along the way.
We made heavy use of coding assistants and the project required just over one man-year of work, for a roughly 10x speed-up over historical coding rates.
Work done in collaboration with Sarah Hoback, Anna Mei and Ron Nissim.

[Joseph Tooby-Smith]

Could you comment on

We made heavy use of coding assistants and the project required just over one man-year of work, for a roughly 10x speed-up over historical coding rates.

Namely, which coding assistants and how extensively they were used and to do what?

[Michael R Douglas]

We're writing a paper explaining our methods. The short answer is that after we planned the project, and wrote many definitions and some theorem statements, the agents (largely Claude code and Copilot/GPT with some help from Gemini 3 Pro) wrote the bulk of the code under our guidance.

[Castedo Ellerman]

Michael R Douglas said:

for a roughly 10x speed-up over historical coding rates.

In the paper it will be nice if you clarify whether the 10x speed-up is based on lines of code (LOC) generated. I suspect it is. LOC generated is not a motivating objective for code and generally speaking less LOC is preferable.

[Michael R Douglas]

Thanks. Yes we will be more precise in the paper. I agree about LOC being inaccurate in comparing code written using different methods, what would you suggest?

[Castedo Ellerman]

It might make sense to create a separate topic on "alternatives to LOC" since the topic of this thread is formalization of quantum field theory.

My short answer is to not attempt quantitative head-to-head overall-task comparison of human vs machine. An alternative, which you might already be putting in the paper, is identifying sub-tasks for which coding assistance were helpful, and where they were not helpful, in qualitative terms. I can't speak for most readers, but the articles I find most useful are the ones that describe specifically in detail what sub-tasks LLMs did well and not well.

[Castedo Ellerman]

Michael R Douglas said:

I agree about LOC being inaccurate in comparing code written using different methods

BTW, I think it's fine to compare LOC written using different methods. For example, I think it's interesting and fine to measure how many LOC a human might golf without an LLM to prove XYZ vs what an LLM found that proved the same XYZ. I can imagine a somewhat precise quantitication that the LLM generated 10x LOC vs golfing without an LLM.

[Kim Morrison]

@Michael R Douglas, @Sarah Hoback, @Anna Mei, @Ron Nissim, might you say anything about your work/future plans to make any of the produced code reusable, whether in the form of upstreaming to Mathlib, or merely doing good library design for the functional analysis material in this project?

It's already a significant problem that projects like this produce non-reusable code, and it is only going to get much worse as people increase the amount of AI they use in these projects without explicit plans for getting past "merely true" all the way up to "useful to others, whether human or AI".

(Context: I think this problem is very solvable, and I do not mean at all to indict AI generated proofs / libraries! But we all collectively have to work hard on this problem, and projects that do not address it are, in my mind, essentially back in 2025 rather than 2026 :-)

[Michael R Douglas]

Happy to work towards bringing this in conformance with library standards.
Are they here? Is there more we should know about?
We will try to get the AI to do that too. Is there a prompt or skill to do it?

[Moritz Doll]

I am travelling, so can't look at the code in detail, but generally I am excited about this and happy to see more applications of Schwarz functions.
As for mathlib upstreaming, for instance there should be a lemma about composition on the right as a continuous linear map and the translation of real to complex valued Schwartz functions should be phrased in terms of that

[Moritz Doll]

I am happy to help with upstreaming, but probably don't have time to look at the code this week

[Michael R Douglas]

@Moritz Doll that would be very good of you, when you find some time let us know.

[Joseph Tooby-Smith]

Kim Morrison said:

It's already a significant problem that projects like this produce non-reusable code, and it is only going to get much worse as people increase the amount of AI they use in these projects without explicit plans for getting past "merely true" all the way up to "useful to others, whether human or AI".

To echo parts of Kim's message here - it would be great to have parts of this added to PhysLean, so that it becomes reusable to the wider community there. Having a single project for results in physics means we are not reproducing things needlessly, for example SpaceTime, and instead can collectively work on making things better, easier to use, and interconnected.

[Joseph Tooby-Smith]

Michael R Douglas said:

Happy to work towards bringing this in conformance with library standards.
Are they here? Is there more we should know about?
We will try to get the AI to do that too. Is there a prompt or skill to do it?

One thing that I think would help is a better organization of the file system. For example, having a folder for SpaceTime, FunctionalAnalysis, GaussianFreeField, etc. Then making sure that e.g. FunctionalAnalysis contains only general results related functional analysis, that could in theory be upstreamed to Mathlib. (One would say, keeping things within their relevant APIs)

[Yoh Tanimoto]

Thanks for the interesting output.

I agree with the other people that it would be necessary to make the code reusable. I am interested in the OS axioms in particular (by the way I think this should be called differently, say the Glimm-Jaffe axioms, to distinguish them from those by Osterwalder and Schrader in 1973/75). For that, we need to make several design decisions.

A substantial part will have an overlap with PhysLean of @Joseph Tooby-Smith, where one would want to define for example the Euclidean group (either as ℝ^n ⋊ O(n) as you did or the (identity component of the) isometry gorup of EuclideanSpace ℝ 4), it should act on ℝ^n just as a function or diffeomorphism....). It's mainly not an AI stuff, but we will have to choose how to formalize them, considering other applications.

[Kelly Davis]

Yoh Tanimoto said:

I agree with the other people that it would be necessary to make the code reusable. I am interested in the OS axioms in particular (by the way I think this should be called differently, say the Glimm-Jaffe axioms, to distinguish them from those by Osterwalder and Schrader in 1973/75). For that, we need to make several design decisions.

I know we'd talked about this before, and I'd mentioned it to @Michael R Douglas too, but are you still interested in formalizing some variant of the Araki-Haag-Kastler axioms too? Maybe reusing some of this work of @Michael R Douglas @Sarah Hoback @Anna Mei and @Ron Nissim as a starting off point?

[Yoh Tanimoto]

the AHK axioms are a bit far, because we need the spectral theorem (I am working on), unitary representations of the Poincaré group and some basics about von Neumann algebras.

The OS (correlation functions)/GJ (measure on the space of distributions) axioms could be doable now with the current status of mathlib.

[Kelly Davis]

Yoh Tanimoto said:

the AHK axioms are a bit far, because we need the spectral theorem (I am working on), unitary representations of the Poincaré group and some basics about von Neumann algebras.

Have you started (public) work on any of these?

[Yoh Tanimoto]

• For the spectral theorem, we will need to define the integral of vector-valued measures, which we are trying to develop now in #26156, #28499 and in this repository https://github.com/oliver-butterley/SpectralThm There was a design question of how to define it, but now we are proceeding and adding basic APIs.
• As for unitary representations of the Poincaré group, the questions that come to my mind immediately are 1. how to define the Poincaré group (the semidirect product vs the group of Lorentz metric preserving transforms) 2. make sure that the representations are SOT continuous (need some type synonym for the the type of unitary operators in B(H)?) I'm sure that one can do it one way or other, but it is a design question.
• I know some work in progress in @Jireh Loreaux 's repository https://github.com/j-loreaux/LeanOA on operator algebras

[Moritz Doll]

As for SOT: docs#PointwiseConvergenceCLM exists and there are characterizations of continuity around here: docs#PointwiseConvergenceCLM.tendsto_nhds

[Patrick Massot]

Did you notice #26160 failed CI?

[Yoh Tanimoto]

@Patrick Massot yes. The PR which #26160 depends on just got merged today, but after a quite bit of design changes. So just merged master. I hope to remove errors shortly.

[Joseph Tooby-Smith]

@Michael R Douglas Would you mind if I started a thread over on the PhysLean channel about what can 'upstream' from your Repo so that the wider physics-lean community can more easily reuse it?

[Michael R Douglas]

Please do. The code is under the Apache 2.0 license.

[Jireh Loreaux]

@Yoh Tanimoto I'm not subscribed to this stream so I didn't see the ping, and only happened upon this thread as a result of another search. Currently, I'm working to develop von Neumann algebra theory from the abstract side, in terms of W⋆-algebras and preduals. One thing which is would be very nice to have is the realization of a H →L[ℂ} H as a W⋆-algebra by realizing the trace-class operators as its predual (note that we don't even have a definition of the ideal of trace-class operators at the moment), let alone the realization of them as a Banach space with the trace norm.

[Joseph Tooby-Smith]

Joseph Tooby-Smith said:

Michael R Douglas Would you mind if I started a thread over on the PhysLean channel about what can 'upstream' from your Repo so that the wider physics-lean community can more easily reuse it?

Done here: #PhysLean > Upstreaming results from OSforGFF

[Yoh Tanimoto]

@Jireh Loreaux yes, I noticed that you are not subscribed to this channel, but I wasn't sure whether I should do it! I agree all about the W*-algebra setting. What is the status of the double commutant theorem?

[Jireh Loreaux]

I have not done anything for that, except for one small thing: docs#LinearEquiv.image_closure_of_convex which effectively says that two locally convex topologies on the same space with the same strong dual have the same closed convex sets.

[Kim Morrison]

Since this is not the main maths threads, I would be happy to have input here from regulars in the Natural Sciences stream. Please DM me, or any moderator, if you have opinions whether posts about like this one (EDIT: since removed, after receiving community feedback) should be junked/suspended. (For context, in the main maths threads someone posting formalizations with : Prop structure fields would probably receive a suspension for AI slop, and the post would be junked.)

[Notification Bot]

4 messages were moved from this topic to #junk > Formalization of quantum field theory by Kim Morrison.

[Joseph Tooby-Smith]

Hi @Michael R Douglas , 

In the conversation above and elsewhere in your private channel a number of different people from the Lean community have being expressing a similar concern with your formalization related to it’s reusability, design, and integration into existing libraries. I have also had private communication with multiple other people that have expressed similar concerns. As has been said elsewhere, this part of formalization is extremely important, and is no small task. A number that I have seen is that it contributes to (at least) 50% of the work, and this is a number that I would agree with. 

I’m not completely convinced that the severity of these points have been fully grasped by your group, or adequately reasoned away. Again multiple others in this community have conveyed a similar message to me privately.  This is fine, and you are under no obligation to do so, as you may have different priorities and interests with formalization. However, due to the prevalence of these dissents within this community, hopefully you will agree with me that, if not addressed before publication, it is academically the correct thing to do to make the physics community aware of them in parallel with your formalisation. I feel this is particularly important because, as you are no doubt aware, your voice and the voice of your group carries a particular weight within the physics community. I would appreciate it if you could let me know here if you plan on doing this, or give the reasons for not? If not I am happy to disseminate something to this effect.

[Michael R Douglas]

Hello @Joseph Tooby-Smith. We are working on integrating those parts which are appropriate for mathlib into mathlib. We received offers of help from the community and we appreciate them and are working with them.

[Michael R Douglas]

You are welcome to use our work in PhysLean with proper attribution. It is under the Apache license which allows this.

[Michael R Douglas]

Personally, I expect the bulk of our QFT work will undergo major rewrites before it reaches final form. It is premature to integrate it into larger works. But if the components are helpful for people now, they are available.

[Joseph Tooby-Smith]

Apologies, but I think I have missed some nuance here in your response. Are you saying that the concerns raised above and elsewhere by this community will be addressed prior to publication? If so this is great, and I thank you for clearing this up.

[Michael R Douglas]

Yes, we will work to address any concerns which are addressed to us. This does not mean that we expect all of this work to go to Mathlib or PhysLean, just certain parts for which that seems appropriate. But good design and reusability are among our goals and we appreciate help with that.

[Moritz Doll]

#35781

[Moritz Doll]

@Michael R Douglas please let me know if the co-authors on the PR need changing

[Matteo Cipollina]

In the hope it helps the integration of this work, I have managed to discharge the three axioms (including the Minlos theorem and uniqueness) in the spacetime Hermite model, here.
https://github.com/or4nge19/OSforGFF

Instead of assuming (or proving) the full Minlos theorem, I implemented a constructive Gaussian measure on the WeakDual of the test function space (WeakDual ℝ TestFunction), relying on the Kolmogorov extension theorem (adapted from the BrownianMotion and KolmogorovExtension libraries by Remy Degenne, both added to the repository), and on the nuclear $L^2$ support theorem.

To discharge the nuclearity assumption (SchwartzNuclearInclusion), I formalized the analytical bounds and steps showing that the Schwartz seminorm sequence is dominated by the Hermite-coefficient seminorms.

All this builds substantially on the above repos and #33329 by Moritz Doll (slightly re-adapted) and re-uses parts of the PhysHermite API from PhysLean (but not yet the distributions API in PhysLean and the SpaceTime API currently under refactor).

While this is partly orthogonal to the discussion about reusability and integration, I think it is motivational to generalize/refactor the results in this repo (or work on the open PhysLean issues) by having a fully proved self-contained model, and useful to see the actual depth of the (minimal) assumptions needed to discharge the formalization.

With regards to reusability, I've sketched some abstractions and potential future TODOs to :
1) refactor the measure-theoretic pipeline through an abstract NuclearGelfandTriple N H abstraction, to decouple the Kolmogorov/Minlos measure construction from the specific geometry of $\mathbb{R}^4$, making the measure theory in theory reusable for spatial kinematics (e.g., $t=0$ Hamiltonian measures);
2) I have started the migration of the 4D spacetime Hermite model to generic d-dimensional Euclidean spaces by parametrizing over a generic [InnerProductSpace ℝ E], defining time translations and reflections via a coordinate-free TimeDirection API;
3) upgrade the test function space to SchwartzMap 𝕜 E V to support vector-valued fields (e.g., gauge fields, Dirac spinors). Global internal symmetries ($V \toL[\mathbb{K}] W$) - not yet local ones - are lifted to the distribution space via WeakDual.comap.

[Michael R Douglas]

@Matteo Cipollina, that is excellent! I look forward to reading it.
I also have a Gaussian measure construction in gaussian-field.
And a version of OS4GFF which uses it to discharge the axioms.
Maybe we can integrate the two.
I am going to wait to do anything to the public OS4GFF until after our preprint comes out,
which should be soon.

[Joseph Tooby-Smith]

Hi @Michael R Douglas , my interpretation your answer to my question above:

Michael R Douglas said:

Yes, we will work to address any concerns which are addressed to us. This does not mean that we expect all of this work to go to Mathlib or PhysLean, just certain parts for which that seems appropriate. But good design and reusability are among our goals and we appreciate help with that.

was that you were going to refactor your repo to take into account principals of good design and reusability before publication.

I now understand that my interpretation was incorrect due to your most recent message in which you have said:

Michael R Douglas said:

I am going to wait to do anything to the public OS4GFF until after our preprint comes out,
which should be soon.

Please can you clarify what you meant in your answer to my question above?

[Michael R Douglas]

I think my message was clear. We will work to address any concerns which are addressed to us. This does not mean that we expect all of this work to go to Mathlib or PhysLean, just certain parts for which that seems appropriate. But good design and reusability are among our goals and we appreciate help with that.
Also, preprint is not publication. Our upcoming preprint is meant primarily for people in our field (theoretical physics, particle physics, string theory) whose background and interests may not be the same as the Lean community at least as of yet. If we publish in a journal of formalization or the like we will of course have to meet their standards.

[Joseph Tooby-Smith]

Ok, thank you for generally being open to discuss publicly and engage in the conversation here. I appreciate the time you have taken to articulate your position, I think there are still points of disagreement, but this is the nature of science.

[Sarah Hoback]

@Joseph Tooby-Smith I think everyone agrees that our formalization needs a huge overhaul to make it "production ready" for others to use. I also think everyone cares that the code eventually is polished, where the parts of the code that are immediately of value to others, are prioritized and refactored such that they are a service to the community. However, there is obviously value in letting users have access to the current state of the code for their own projects to use parts that are of value to their current projects. This includes the fact that the code is of course not ready to be integrated to PhysLean or Mathlib in the current state. Moreover, releasing code that is "merely true" and sharing the result allows others to time their projects w.r.t. our refactor in a way that is highly aligned with the overall incentives of a collaborative physics community. If your concern pertains primarily to publication, our draft states the limitations of our formalization and states that the code will need a major refactor to meet the important standards upheld in PhysLean and Mathlib. We see this as no small task and really appreciate all those who have extended help in significantly improving our formalization.

[Joseph Tooby-Smith]

Hi Sarah, I think this addresses my concerns with regard to the information disseminated to the physics community so thank you