OpenAI Result in Theoretical Physics

Stream: Machine Learning for Theorem Proving

[Franz Huschenbeth]

There has been a article (and paper) by Open AI in which they show GPT-5.2 "solving" (rather solving a subproblem, but I dont want to discuss this particular result here) a Research Problem in Theoretical Phsyics. What I find interesting about that blog post is the following excerpt:

"An internal scaffolded version of GPT‑5.2 then spent roughly 12 hours reasoning through the problem, coming up with the same formula and producing a formal proof of its validity"

They do not explain what that "formal proof" is or in what language it is, altough I suspect it might be Lean. Does anyone know more? The preprint only explains the theoretical physics result and does not explain, how that internal scaffolded version of GPT-5.2 works.

[David Michael Roberts]

If it's Lean then I suspect it would have to be with a bunch more than what's in mathlib. From the paper:

The key formula (39) for the amplitude in this region
was first conjectured by GPT-5.2 Pro and then proved by
a new internal OpenAI model. The solution was checked
by hand using the Berends–Giele recursion and was more-
over shown to nontrivially obey the soft theorem, cyclic-
ity, Kleiss–Kuijf, and U(1) decoupling identities—none of
which are evident from direct inspection.

leading up to this is a lot of particle physics jargon. Since the authors are physicists, they will probably say "formal proof" for what people here would call "informal proof" (aka pen and paper proof). The paper also says

The rest of this work is devoted to proving that the
conjecture (39) is correct. The proof uses ideas from
time-ordered perturbation theory

so for doing this in Lean, that theory would need to be developed, and that is not exactly trivial. If that was done, I think it would also be announced ("we have formalised particle physics in Lean!!!1!")

[David Michael Roberts]

I don't think an AI company would want to pass up mentioning using Lean like the cool kids are

[David Michael Roberts]

From the press release:

The equation was subsequently verified analytically to solve the Berends-Giele recursion relation,

"solving analytically" is a term of art in physics, meaning an actual mathematical derivation rather than a hand-wavy argument based on physical principles being imposed on formulae to simplify or massage them. So I'm very confident that whoever wrote this was using terminology as the way physicists would, and not how the formalisation community would.

[Franz Huschenbeth]

Good points. But OpenAI has connections to Lean (or atleast had through Jesse Han), but your arguments do make sense and I am more convinced its a natural language proof than a formalized proof now.