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.
Douglas, Sarah Hoback, Anna Mei, and Ron Nissim,Formalization of QFT, March 2026
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
fields
hep-th 1years
2026 1verdicts
CONDITIONAL 1representative citing papers
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.