Formalization for Physics
Advances in proof assistants and AI reasoning are opening a new opportunity to bring machine-checked rigor to physics.
Formal methods are becoming increasingly relevant to physics, not only as tools for checking completed arguments but also as instruments for clarifying definitions, exposing hidden assumptions, and organizing large bodies of technical knowledge. This workshop will bring together theoretical physicists, mathematical physicists, mathematicians, and proof-assistant practitioners to identify where machine-checked reasoning can be genuinely useful for physics research.
The proposal is not that formalization should replace physical intuition. The more realistic and scientifically useful goal is to understand how formalization can make precise which parts of an argument are rigorous, which parts depend on explicit mathematical assumptions, and which parts remain heuristic. This is especially relevant in theoretical and mathematical physics, where important arguments often involve several layers of definitions, conventions, and intermediate structures.
The timing is favorable because several communities are now converging. Proof assistants such as Lean, Coq, Isabelle, and Agda have reached the point where substantial parts of modern mathematics can be formalized. AI-assisted theorem proving and code generation are rapidly changing the cost profile of formalization. Physicists have recently completed several medium-size formalizations in quantum theory, on topics ranging from quantum information theory to constructive quantum field theory, and are starting to encounter the issues of coordination and organization which arose and were addressed in earlier large-scale projects.