Formalization for Physics at ICARM

About this event

The Institute for Computer-Aided Reasoning in Mathematics (ICARM) at Carnegie Mellon is hosting a meeting, Formalization for Physics, organized by Sergey Cherkis, Michael Douglas, James Halverson, and X i Yin on November 4-6. Local faculty and students are welcome to attend. Please register using the link below; you can join the participants' discussion channel on the ICARM Zulip. Register: https://icarm.io/join/0btzmSk86L5VdlJqNmQ7m1B6CQP6TKZ-7e1Vr-ZGYcw/ Zulip: https://icarm.zul ipchat.com/join/pueyd62pbxstlmc43qeojl7q/ Description: 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 reach ed 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.re welcome to attend. Please register using the link below; you can join the participants' discussion channel on the ICARM Zulip.

Register: https://icarm.io/join/0btzmSk86L5VdlJqNmQ7m1B6CQP6TKZ-7e1Vr-ZGYcw/

Zulip: https://icarm.zulipchat.com/join/pueyd62pbxstlmc43qeoj l7q/

Description: 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 whe re 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.