One by one, artificial intelligence (AI) is felling some of the biggest trees in the mathematical forest. In September, OpenAI announced it had cracked the notoriously difficult Navier-Stokes fluid dynamics problem, one of math’s seven Millennium Prize challenges. A month later, the company released more than 700 math papers, including a major advance on the Riemann hypothesis, another famous unsolved Millennium Prize Problem involving prime numbers. Its latest release, on 28 October, included a refutation of a decades-old conjecture in computer science —as well as a proof that one of physics’ most successful theories is on firm mathematical footing.

Controversially, OpenAI did not release the 1147-page proof of the physics result, known as the 4D Yang-Mills existence problem. Instead, it appointed a committee of physicists and mathematicians headed by Nobel laureate David Gross to “shepherd” the result. On 10 November, the group released a validation of a formalized version of the proof in Lean, a computer language that can check mathematical arguments against a set of axioms. Although it doesn’t mean the still-unreleased proof is correct, it’s a sign of its logical consistency.

For physicists, the result is unlikely to change their day-to-day work: The Yang-Mills theory has already been remarkably successful at explaining the behavior of particles at accelerators such as the Large Hadron Collider. But important mysteries still remain, including how most of the mass of protons and neutrons arises, and why the quarks that make them up can never be found alone. A rigorous proof could offer fresh insights into these phenomena. “Maybe there’s something we’re missing,” says David Tong, a physicist at the University of Cambridge.