The Seiberg–Witten SU(2) solution is formalized in Lean 4 with physical assumptions as named predicates and mathematical consequences as sorry-free theorems, demonstrating a method for auditing non-rigorous physics arguments.
Instanton counting on blowup. I. 4-dimensional pure gauge theory
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
abstract
We give a mathematically rigorous proof of Nekrasov's conjecture: the integration in the equivariant cohomology over the moduli spaces of instantons on $\mathbb R^4$ gives a deformation of the Seiberg-Witten prepotential for N=2 SUSY Yang-Mills theory. Through a study of moduli spaces on the blowup of $\mathbb R^4$, we derive a differential equation for the Nekrasov's partition function. It is a deformation of the equation for the Seiberg-Witten prepotential, found by Losev et al., and further studied by Gorsky et al.
fields
hep-th 2years
2026 2verdicts
CONDITIONAL 2representative citing papers
Blow-up equation prefactors encode cubic 1-form self-anomalies and mixed anomalies of 5d N=1 SCFTs, deciding 2-group vs mixed anomaly structure.
citing papers explorer
-
Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean
The Seiberg–Witten SU(2) solution is formalized in Lean 4 with physical assumptions as named predicates and mathematical consequences as sorry-free theorems, demonstrating a method for auditing non-rigorous physics arguments.
-
Generalised global symmetries in 5d $\mathcal{N}=1$ theories from the blow-up equations
Blow-up equation prefactors encode cubic 1-form self-anomalies and mixed anomalies of 5d N=1 SCFTs, deciding 2-group vs mixed anomaly structure.