Solver Agent: an Agentic AI Framework for Theoretical Physics Computations Applied to F-theory Uplifts of O3-planes and S-folds
Authors: Eliott Morgensztern, Cesar Fierro Cota, Alessandro Mininno
Organizations: Sorbonne Université, CNRS, Laboratoire de Physique Théorique et Hautes Energies, Campus Pierre et Marie Curie, 4 place Jussieu, F-75005, Paris, France · Department of Physics, University of Wisconsin–Madison, 1150 University Avenue, Madison, WI 53706, USA
We introduce Solver Agent, an AI framework based on large language models for calculations and proofs in mathematics and theoretical physics. The solution process is tracked through a persistent ledger that records assumptions, derivations, and computations. A central agent delegates tasks to specialized sub-agents, while independent agents verify both intermediate steps and the final result. This setup improves the traceability, reproducibility, and verification of computer-assisted calculations. Applying Solver Agent, we study global F-theory uplifts of Type IIB orientifolds and their S-fold generalizations. We establish sufficient conditions for Weierstrass models over projective threefolds with terminal Zk quotient singularities (k∈{2,3,4,6}) to give Q-factorial projective elliptically fibered Calabi-Yau fourfolds with isolated Gorenstein terminal quotient singularities. These geometries realize O3-planes and S-folds, where local D3-brane probes of the latter yield four-dimensional N=3 superconformal field theories. Using stringy invariants, we derive fixed-point contributions to Hodge data and Euler characteristics, and show that these Euler corrections determine the localized D3-brane charges required for tadpole cancellation. We illustrate these results using toric hypersurface constructions, where a single three-dimensional polytope determines both the Type IIB Calabi-Yau threefold and the F-theory base; here, the orientifold double cover naturally forms a bisection of an alternative genus-one-fibered uplift with discrete Z2 gauge symmetry. Finally, we provide methods for toric computations and four-form flux analysis in four-dimensional N=1 compactifications with non-abelian gauge sectors.
Figures & tables
Section
Purpose
Prompt
Result
Section 4.1
Check terminal singularities
4.1
4.1
Count terminal singularities
4.1
4.1
Identify local groups
4.1
4.1
Section 4.2
Prove Theorem 4.2
4.2
4.2
Section 4.3
Stringy Euler definition
4.3
4.3
Compute stringy Euler
4.3
4.3
Table 1 : Overview of prompts provided to Solver Agent and their corresponding results, categorized by section and purpose.
Entry type
Written by
Content
Assumption
main solver
interpretive choices, definitions, notation, conventions, domains of validity
Derivation
main solver
reasoning steps and plans, in mathematical prose
Result
main solver
interpretation of a computation, with an explicit dependence on it
Symbolic computation
sub-agent
computer-algebra task, code, and output
Numerical computation
sub-agent
numerical task, code, output, and generated files
Calabi–Yau analysis
sub-agent
geometric quantities from domain-specific software
Table 2 : Entry types of the solution ledger. Each entry carries a status (accepted, rejected, or superseded), a summary, a detailed body, and references to the entries on which it depends.
X3
B3
κ
c2(TX3)⋅J
χ(X3)
nsing(B3)
X8
P3
2
44
−296
0
X10
P[1,1,1,2]3
1
34
−288
1
Table 3 : Here J is the Kähler class in X3 , κ=∫XJ3 , and nsing(B3) is the number of terminal quotient singularities associated to the base B3 of a given F-theory uplift for X3 .
We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics, with the autoformalization of the fundamental theorem of matrix-product states as a demonstration. The agents, coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously. For some statements, the agents were able to explore new proof routes that are not part of the standard literature. Along the way the agents produced extensive tensor-network and quantum-information libraries not previously available in Mathlib, Lean's mathematical library. As a physical application, the formalization also extends towards symmetry-protected topological phases in one dimension. We find that the main bottleneck in large-scale autoformalization is enforcing mathematical intent and we provide a detailed study of the full process and various subtleties involved. We release the codebase as the library TNLean, together with a \nChapters{}-chapter blueprint of the formalization effort.
Sirui Lu, Erickson Tjoa, J. Ignacio Cirac
Max-Planck-Institut für Quantenoptik, Hans-Kopfermann-Straße 1, D-85748 Garching, Germany · Munich Center for Quantum Science and Technology (MCQST), Schellingstraße 4, D-80799 Munich, Germany
Tool calling allows large language models (LLMs) to invoke external computation during problem solving, a useful capability in various fields including AI for mathematics. We study this setting through weighted sum-of-squares (SOS) decomposition, a machine-checkable route to proving polynomial nonnegativity and hence polynomial inequalities. A candidate decomposition can be checked exactly, but finding one requires choosing among non-unique regroupings and coordinating multiple symbolic transformations. We develop an agent that combines algebraic task training, symbolic tools, and verifier-grounded optimization for this task. Rather than training only on the composite SOS task, we construct 1.35 million synthetic examples covering eight supporting polynomial tasks together with weighted-SOS decomposition. We first apply supervised fine-tuning (SFT) to direct algebra problems and simulated symbolic traces, and then use Group Relative Policy Optimization (GRPO) with task-specific symbolic rewards. The SFT corpus contains no native tool-calling messages; at evaluation, the agent uses native SymPy calls for expansion, collection, reordering, and factorization. Every final SOS answer is checked by exact expansion and coefficient comparison. On held-out, same-generator synthetic problems, the full SFT+GRPO+tools system is the strongest of four evaluated configurations, reaching 78.96% verified success on weighted SOS, compared with 44.73% for the base model with the same tools, and 91.75% macro accuracy across nine polynomial tasks. Within this controlled setting, our work provides a case study of combining domain-specific skill training, executable tools, and verifier feedback, and may inform the design of tool-calling agents in other domains with exactly checkable outputs.
Recent advances in AI for Mathematics have focused largely on autoformalization and theorem proving, leaving the role of Computer Algebra Systems (CAS) in agentic LLM workflows underexplored. We propose a ReAct-style agentic setup that combines LLM reasoning with verifiable feedback from SageMath, together with Context7 for the up-to-date documentation. We evaluate this agentic setup across frontier models for solving research-level mathematical problems from the RealMath benchmark in a setting that emulates a computational-mathematics research loop. We also propose a refinement to the RealMath benchmark by introducing a multi-step post-processing procedure and a multi-stage validation pipeline, both of which improve the quality and reliability of the extracted problem set. Our experiments reveal substantial performance gains from SageMath access across all evaluated models on +9.7pp on average, the gains range from 1.5pp to 27.8pp and narrow the gap between open-weight and closed models. Qwen3.7-Max benefits from SageMath the most, while GPT-5.5 achieves the highest solve rate of 75.2% and the lowest token usage among tool-enabled configurations. Our findings suggest that CAS-augmented agents represent a promising direction for assisting mathematicians in computational exploration, and we believe that this work is a step towards automated conjecture discovery. The project repository is available online.
Pavel Snopov, German Magai
School of Mathematical and Statistical Sciences, The University of Texas Rio Grande Valley, USA · Noeon Research, Tokyo, Japan.