Modern theoretical physics faces a dual challenge: many of the model spaces of interest are combinatorially large, while the reliability of the resulting claims remains essential. This talk argues that these pressures call for a synthesis of agentic automation and formal certification. Agentic systems can assist with literature analysis, code generation, numerical experimentation, and workflow orchestration, thereby extending the scale and efficiency of theoretical research. Yet automation alone does not establish correctness.
I will therefore discuss how interactive theorem provers can formalize physical definitions, reduction steps, and classification statements, yielding results that are both executable and certified. As an illustration, I will present recent work on formally verified bounded SU(5) model building with additional Abelian symmetries.