Lean is an interactive theorem prover, that is, a programming language in which you can write down mathematical definitions, theorems and their proofs, and it will use its mathematical foundation of type theory to check for mathematical correctness. Lean and its library of mathematics results, Mathlib, are increasingly being used by AI companies to reason about mathematics and automatically proof and state theorems. This talk is about PhysLean, the quest to build the lean library for physics results. In this talk I will demonstrate Lean’s potential in physics, discuss the motivations behind the project PhysLean and its current content.