Research theme · 03
AI and formal verification for physics
Agentic systems for quantum physics research and machine-checked reasoning in Lean 4.
We develop methods for doing physics: AI systems that support scientific investigation and formal verification that makes mathematical reasoning explicit and checkable.
These two directions complement one another. Agentic systems can help explore questions and candidate arguments; formal verification can check whether a formalized conclusion follows from its stated assumptions. Both are connected to the scientific questions in our quantum dynamics and foundations themes.
Research direction · 01
Agentic systems for quantum physics research
How can AI agents support research on complex quantum systems? This direction explores research workflows that connect scientific questions with analytical reasoning, numerical experiments, and the interpretation of results.
We aim to develop agentic systems that help researchers investigate physical models, make their reasoning explicit, and organize reproducible calculations. Complex quantum systems provide both the scientific focus and a setting in which to evaluate these methods.
Research direction · 02
Formal verification of physics in Lean 4
How can we express physical arguments so that their mathematical steps can be checked by a computer? This direction focuses on formalizing definitions, assumptions, and proofs in Lean 4.
The aim is to build reusable, machine-checked foundations for reasoning about physics. Making assumptions explicit also helps distinguish what follows from a mathematical model from the physical judgments used to choose that model.