PhysLean is a project to create a monolithic library of results from physics in Lean 4, akin to Mathlib for mathematics. It contains results from a range of different areas of physics including classical mechanics, relativity, condensed matter physics, quantum field theory, string theory etc. In this talk I will give a high-level overview of the current content of PhysLean and explain how formalizing results from physics, for physicists, differs to from formalizing results from mathematics, for mathematicians, and what features we have put in place to make this as an efficient and open process as possible.
This talk is aimed at those familiar with interactive theorem provers, I am giving a talk on the Friday aimed at physicists.
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8H...
Meeting ID: 898 5609 1954 Passcode: ITPtalk