The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization
Sven Krippendorf, Leopoldo Sarra, Joseph Tooby-Smith
hep-ph
Oct 6, 2026 · v1
cs.AI cs.LO hep-th
TL;DR
Perspective on AI-assisted physics formalization that uses Lean as its reference prover for examples and centers the Lean-based Physlib and Mathlib libraries.
Abstract
Rapid advances in AI have opened a new era for physics, enabling unprecedented capabilities in research and discovery. However, these advances also bring challenges in verifying, trusting, and reusing the results they so rapidly produce. Formalization is a necessary part of the solution to these challenges. In this paper, as well as giving an overview of the role of AI and formalization in physics, we make the case that: (1) formalization is an essential layer for AI-driven discoveries in both computational and theoretical physics; (2) AI is lowering the barrier to, and increasing the efficiency of, formalization in physics, though it remains weaker at choosing definitions and designing libraries than at writing proofs; (3) the speed AI brings to formalization in physics currently comes at the cost of trust, credit, and community; (4) shared, community-reviewed formal libraries such as Physlib should be central in making progress in this field, both as a trusted, reusable foundation for physics results and as the environment in which AI systems can reason about physics; (5) formalizing physics raises challenges beyond those in mathematics, most importantly that a checked proof does not establish that its definitions faithfully capture the intended physics. We also give our perspectives on near-term and long-term directions in these areas.
Problem
AI is producing physics results quickly, which makes verifying, trusting, and reusing those results harder. The paper asks what role formal verification should play in AI-driven physics.
Approach
A perspective and overview article that uses Lean as its reference interactive theorem prover and as the language for its examples. It discusses physics formalization built on Mathlib and community libraries such as Physlib. It also examines how well AI performs at writing proofs compared with choosing definitions and designing libraries.
Results
Formalization is argued to be an essential layer for AI-driven physics discovery, and shared, community-reviewed libraries like Physlib should be central to it. AI lowers the barrier to formalization but trades off trust, credit, and community. A key challenge specific to physics is that a checked proof does not guarantee that its definitions faithfully capture the intended physics.
