# The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 43 of its 86 references that are in the map.
- First posted on arXiv 6 Oct 2026.

## Builds on (most cited first, 30 of 43)

- [World Models](https://mlsanity.com/paper/1803.10122/) (2018)
- [Mastering Diverse Domains through World Models](https://mlsanity.com/paper/2301.04104/) (2023)
- [V-JEPA 2: Self-Supervised Video Models Enable Understanding, Prediction and Planning](https://mlsanity.com/paper/2506.09985/) (2025)
- [GAIA-1: A Generative World Model for Autonomous Driving](https://mlsanity.com/paper/2309.17080/) (2023)
- [Emergent World Representations: Exploring a Sequence Model Trained on a Synthetic Task](https://mlsanity.com/paper/2210.13382/) (2022)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)
- [Early science acceleration experiments with GPT-5](https://mlsanity.com/paper/2511.16072/) (2025)
- [Dive into Claude Code: The Design Space of Today's and Future AI Agent Systems](https://mlsanity.com/paper/2604.14228/) (2026)
- [Theoretical Physics Benchmark (TPBench) -- a Dataset and Study of AI Reasoning Capabilities in Theoretical Physics](https://mlsanity.com/paper/2502.15815/) (2025)
- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [Probing the Critical Point (CritPt) of AI Reasoning: a Frontier Physics Research Benchmark](https://mlsanity.com/paper/2509.26574/) (2025)
- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?](https://mlsanity.com/paper/2601.03298/) (2026)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale](https://mlsanity.com/paper/2512.07087/) (2025)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium](https://mlsanity.com/paper/2603.15929/) (2026)
- [Progress in Formalizing Sphere Packing in Dimension 8](https://mlsanity.com/paper/2604.23468/) (2026)
- [Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving](https://mlsanity.com/paper/2606.29493/) (2026)
- [AI Descartes: Combining Data and Theory for Derivable Scientific Discovery](https://mlsanity.com/paper/2109.01634/) (2021)
- [Lean4Lean: Verifying a Typechecker for Lean, in Lean](https://mlsanity.com/paper/2403.14064/) (2024)
- [Test-time Scaling Techniques in Theoretical Physics -- A Comparison of Methods on the TPBench Dataset](https://mlsanity.com/paper/2506.20729/) (2025)
- [SorryDB: Can AI Provers Complete Real-World Lean Theorems?](https://mlsanity.com/paper/2603.02668/) (2026)
- [Solving an Open Problem in Theoretical Physics using AI-Assisted Discovery](https://mlsanity.com/paper/2603.04735/) (2026)
- [The Need for Verification in AI-Driven Scientific Discovery](https://mlsanity.com/paper/2509.01398/) (2025)
- [A Formalization of the Generalized Quantum Stein's Lemma in Lean](https://mlsanity.com/paper/2510.08672/) (2025)
- [EconCSLib: AI-Assisted Lean Formalization for Economics & Computation research](https://mlsanity.com/paper/2606.13306/) (2026)

## Abstract (arXiv)

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.