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.

翻译：暂无翻译