Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Physics as Code: From Scans to Theorems with ITP APIs in $SU(5)$ Model Building

Sven Krippendorf, Joseph Tooby-Smith

Abstract

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 impractical, while statistical exploration does not by itself provide theorem-backed guarantees. This motivates workflows in which the model-building problem itself is formalized inside an interactive theorem prover (ITP). In this paper we develop an API-based methodology for formalizing such bounded model-building questions inside Lean, an interactive theorem prover. The central step is to represent the relevant charge spectra, predicates, and reduction moves as reusable ITP definitions, and then to derive the classification from proved reduction theorems rather than from an ad hoc scan. We demonstrate the strategy in a concrete $SU(5)$ case study motivated by F-theory model building with additional Abelian symmetries. At the charge-spectrum layer, we classify bounded spectra that admit a top-quark Yukawa coupling, avoid a selected set of dangerous operators, and satisfy a minimal charge-spectrum completeness condition. Our main result shows that every such spectrum in the bounded search space arises from finitely many minimal top-Yukawa witnesses together with controlled completions and certified closure steps. This classification represents a formally verified description of the full viable class in the charge-spectrum setting studied here. The development is implemented inside PhysLib as reusable infrastructure rather than as a one-off verification script. It provides a proof of principle for how interactive theorem provers can turn combinatorially difficult model-building problems into correctness-first, reusable workflows, and we discuss how the resulting certified classification can serve as reliable input for downstream analyses.

Physics as Code: From Scans to Theorems with ITP APIs in $SU(5)$ Model Building

Abstract

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 impractical, while statistical exploration does not by itself provide theorem-backed guarantees. This motivates workflows in which the model-building problem itself is formalized inside an interactive theorem prover (ITP). In this paper we develop an API-based methodology for formalizing such bounded model-building questions inside Lean, an interactive theorem prover. The central step is to represent the relevant charge spectra, predicates, and reduction moves as reusable ITP definitions, and then to derive the classification from proved reduction theorems rather than from an ad hoc scan. We demonstrate the strategy in a concrete case study motivated by F-theory model building with additional Abelian symmetries. At the charge-spectrum layer, we classify bounded spectra that admit a top-quark Yukawa coupling, avoid a selected set of dangerous operators, and satisfy a minimal charge-spectrum completeness condition. Our main result shows that every such spectrum in the bounded search space arises from finitely many minimal top-Yukawa witnesses together with controlled completions and certified closure steps. This classification represents a formally verified description of the full viable class in the charge-spectrum setting studied here. The development is implemented inside PhysLib as reusable infrastructure rather than as a one-off verification script. It provides a proof of principle for how interactive theorem provers can turn combinatorially difficult model-building problems into correctness-first, reusable workflows, and we discuss how the resulting certified classification can serve as reliable input for downstream analyses.

Paper Structure

This paper contains 13 sections, 12 equations, 1 figure.

Table of Contents

  1. Introduction
  2. The larger scientific goal.
  3. A representative example: GUT model search with additional Abelian symmetries.
  4. Factoring out the combinatorics.
  5. The proposed mechanism: theorem-backed APIs in an interactive theorem prover.
  6. What we demonstrate in this paper.
  7. From the Physics Question to a Formal Classification Problem
  8. The running example and its physics origin
  9. Why brute-force scans are not enough for a certified classification
  10. Minimal witnesses and controlled completions
  11. A mathematical summary in PhysLib-style notation
  12. Formal Vocabulary: a PhysLib API for Charge Spectra
  13. Charge spectra as the basic object

Figures (1)

  • Figure 1: Workflow of the certified classification. A physical model-building question is decomposed into a model class $\mathcal{C}$ and a set of physics requirements $\mathcal{P}$. Both are formalized in Lean: the model class through the core object mycolorSubtle, and the target requirements through Lean predicates. This yields a formal classification problem on the bounded class $\mathcal{U}(I)$, whose output is the certified viable class $\mathcal{V}(I)$, together with soundness and completeness guarantees.