Machine-checked physics: Lean 4 proofs of quantum-mechanical structure, tied to symbolic computation and digital twins so that a scientific claim is verified rather than asserted.
Most scientific claims are checked by a reader. This work makes them checkable by a machine. I am formalizing physics in Lean 4 on top of Mathlib, so that a statement about a quantum system is not a sentence in a paper but a theorem whose proof the compiler accepts or rejects. PhysLib is the library that grows out of this: formalized results across quantum mechanics, electromagnetism, thermodynamics, optics and mechanics, connecting 12K+ Mathlib declarations to physical concepts.
Quantum mechanics is where it starts. Spin-½ structure is proved outright: the Pauli matrices as explicit 2×2 complex matrices, their commutation relations, the identity that their squares sum to 3I, and the ladder operators built from them. A no-go theorem shows that no finite set of matrices can satisfy the canonical commutation relation exactly, because the trace of a commutator vanishes while the trace of the identity does not, which is why every truncated numerical Fock space is necessarily an approximation. For NV centers in diamond, the spin Hamiltonian, Zeeman splitting and ODMR contrast are formalized and tied back to the quantum-sensing experiments they describe.
The proofs are meant to be used, not archived. They sit inside Marimo notebooks next to SymPy, with a Lean InfoView showing goals and diagnostics as the code changes, and they compile against Mathlib on the VVUQ verification service. Each claim is encoded twice, in Lean and in SymPy, and the two encodings are kept in agreement. Bundles of related theorems must compile together as one module, so a proof about a Pauli matrix and a proof about a Hamiltonian are provably about the same objects rather than two conveniently chosen definitions that never meet.
The larger aim is AI-augmented discovery with the burden of proof kept where it belongs. Language models are good at proposing relationships and formalizations; Lean and SymPy decide whether they hold. Digital twins of experiments supply the numbers, verification supplies the verdict, and uncertainty quantification says how far to trust the result. Axiomatic AI is the technology transition of this approach into engineering practice.
Dirk Englund co-founded Axiomatic AI and is a technical advisor to Axiomatic AI.
Licensing: MIT Technology Licensing Office, available technologies from this lab ↗