We Should Formalise Physics
LEAN is a programming language. But it’s main appeal is that it helps you prove things in math.
In Lean, you write programs that consists of ‘theorems’. Theorems are statements that you think are true, and are written down in code. To get Lean to compile, you need to prove each theorem with something called tactics, which make use of prior theorems that you have already proved.
Lean fails on logically wrong lines of code. So, given some starting axioms, everything one writes down in a library that works must be logically true.
This is incredibly powerful. Lean has been used to formalise mathematics in the Mathlib project. Mathlib aims to verify and record some of humanity’s greatest theorems. Lean has also hit the news because Google Deepmind used it to train and verify their LLMs to solve problems in the International Math Olympiad.
Should we do the same with physics? Should we seek to formalise all of our known physical laws in Lean to check correctness?
Formalising physics into a codebase means that physicists will only have to prove things once. People who want to test new physical laws can check for mathematical correctness instantly, and without peer review.
It can also be used to help mark physics students’ work and teach people rigour, which indirectly accelerates the field.
If we reach a point generative AI can pose new physical theories or experiments, it’s essential to have some way of making sure the math is right. Right now, we have check math manually. But if generative AI creates thousands of theories a second, there will have to be a way to check things automatically.
This is why the the PhysLean project, founded by Joseph Tooby-Smith (who has been an extremely kind and patient collaborator), is important, and you should check it out.
As a caveat though, I’m a little torn about the philosophy of working on formalisation in general.
Physics is about writing rules that match reality, even if the rules aren’t mathematically rigorous. As long as it works.. The Feynman path integral is a perfect example of this - the method works, but hasn’t yet been rigorously defined in the field of mathematical analysis.
What this philosophy says about the act of doing physics formalisation is unclear to me, and I hope to write more on this in the future.