Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean

🕰 Orloj analysis

Tento článek navrhuje využití interaktivních nástrojů pro ověřování teorémů (Lean 4) k formalizaci a strojové kontrole jinak nerigorózních fyzikálních argumentů, konkrétně Seiberg-Wittenova řešení pro N=2 SU(2) super-Yang-Mills teorii. Metoda spočívá v postulování explicitních fyzikálních axiomů a jejich následném strojově ověřitelném odvození, což má sloužit jako spolehlivý standard pro validaci výsledků generovaných umělou inteligencí v teoretické fyzice.

💡 Jde o vysoce hodnotný metodologický příspěvek, který nabízí novou úroveň důvěryhodnosti pro komplexní fyzikální odvození a je klíčový pro budoucí validaci výsledků AI v teoretické fyzice.

Categories: INF-1 MET-1

✓ code_available, falsifiable, modest_claims

📄 Abstract

Mathematicians have embraced interactive theorem provers with growing enthusiasm -- building large shared libraries and machine-checking a string of landmark results. Theoretical physics is different: most of its results are not theorems but justified by arguments the community trusts without a rigorous proof. For many -- the one we treat here among them -- no rigorous proof is within reach. For 4d Yang--Mills theory, deriving exact rigorous results from first principles would first require constructing the interacting theory nonperturbatively, which is a sizable piece of one of the Clay Millennium prize problems. We argue here that an interactive theorem prover can be used to verify some non-rigorous physics arguments. The method is to postulate a short list of explicit, named physical postulates, which imply the physical results by virtue of a machine-checkable proof. The trust that remains then rests on that short, inspectable list, and the prover can report, for any downstream result, exactly which assumptions it used. We carry this out for the Seiberg--Witten solution of ${N}=2$ $SU(2)$ super-Yang--Mills -- the genus-one case -- formalized in Lean 4; the higher-genus $SU(N)$ generalization is developed in the same repository as an axiomatized skeleton and left to future work. We describe what is proved, what is assumed, how the assumptions are checked -- external review and an independent numerical oracle -- and why this discipline is a sound standard for validating AI-generated results in theoretical physics. What we offer is a discipline, reviewable on its own terms: a reader may take the Seiberg--Witten mathematics on trust and still assess the formalization method.

📄 arXiv abstract page 📥 PDF