{"id":"arxiv/2607.06379","url":"https://arxiv.org/abs/2607.06379","tags":["hep-th","cs.LO"],"score":0,"title":"Axioms for physical reasoning: codifying the Seiberg--Witten solution in Lean","domain":"hep-th","source":"arxiv","authors":["Michael R. Douglas"],"reviews":0,"subject":"hep-th","summary":"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…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-07-07","reactions":{}}