Towards a formally verified framework for quantum physics in the age of artificial intelligence using Lean4

Despite recent technological advancements, physical theories are still mainly developed and checked by hand. Expressing physical models in formal languages that can be algorithmically verified would ensure theoretical consistency and potentially reveal new physics through rigorous mathematical analysis. This is similar to how the Berry phase, the Aharonov-Bohm effect, and quantum physics emerged. Recent advances in interactive theorem proving, particularly Lean4, have achieved remarkable success in mathematics. However, skepticism remains about their applicability to physics, given its reputation for being more intuitive.

We present our work formalizing parts of a quantum physics textbook and solving its exercises using the resulting framework. Our success demonstrates that these methods are approaching readiness for widespread adoption in verifying scientific reasoning. Artificial intelligence can accelerate this transition by translating natural language into formal specifications, proposing formalization strategies and proofs, and reducing the learning curve for adoption. In turn, formal verification can certify the consistency of machine-generated scientific reasoning, preventing errors while producing verified training data for improved future models.