4 papers
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
Joseph Tooby-Smith
In 2006, using the best methods and techniques available at the time, Maniatis, von Manteuffel, Nachtmann and Nagel published a now widely cited paper on the stability of the two H…
Physics as Code: From Scans to Theorems with ITP APIs in Model Building
Sven Krippendorf, Joseph Tooby-Smith
A recurring challenge in theoretical physics is to make reliable global statements about bounded but combinatorially large model spaces. Exhaustive scans quickly become opaque or i…
Digitalizing Wick's theorem
Joseph Tooby-Smith
Wick's theorem is a cornerstone of perturbative quantum field theory. In this paper we announce and discuss the digitalization of Wick's theorem and its proof into the interactive…
Formalization of physics index notation in Lean 4
Joseph Tooby-Smith
The physics community relies on index notation to effectively manipulate types of tensors. This paper introduces the first formally verified implementation of index notation in the…