Michael R. Douglas

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

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...