Speaker
Joseph Tooby-Smith
Description
This talk will discuss an open-source, community run, project called PhysLean, which aims to write
physics into the interactive theorem prover Lean 4. That is, a computer programming language where
mathematical correctness is guaranteed. There are numerous benefits to this endeavor including
correctness, searchability of results, and the ability to interact with AI in a way safe from (certain) hallucinations.
In this talk, I will give an overview of this project, and briefly discuss its use in String theory.
