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

arXiv: https://arxiv.org/abs/2603.28406 · HTML: https://mlsanity.com/paper/2603.28406/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Mar 2026.

## Built on by (most cited first, 2 of 2)

- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

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.