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.
Ahlfors,Complex analysis, 3rd ed., McGraw-Hill, 1979
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.