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

TL;DR

This paper introduces a formalized, theorem-prover-based methodology for classifying complex model spaces in theoretical physics, demonstrated through an $SU(5)$ case study, ensuring correctness and reusability.

Contribution

It develops a reusable API-based approach in Lean for formalizing and classifying bounded spectra in physics models, moving beyond ad hoc scans.

Findings

Classified bounded charge spectra with Yukawa couplings and operator constraints.

Proved that all spectra arise from finitely many minimal witnesses and controlled completions.

Provided a verified, reusable workflow for complex model classification in physics.

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.