BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Using interactive theorem provers in physics - Joseph Tooby-Smith 
 (University of Bath)
DTSTART:20251016T160000Z
DTEND:20251016T170000Z
UID:TALK238711@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:PhysLean is a project to create a monolithic library of result
 s from physics in Lean 4\, akin to Mathlib for mathematics. It contains re
 sults from a range of different areas of physics including classical mecha
 nics\, relativity\, condensed matter physics\, quantum field theory\, stri
 ng theory etc. In this talk I will give a high-level overview of the curre
 nt content of PhysLean and explain how formalizing results from physics\, 
 for physicists\, differs to from formalizing results from mathematics\, fo
 r mathematicians\, and what features we have put in place to make this as 
 an efficient and open process as possible.\n\nThis talk is aimed at those 
 familiar with interactive theorem provers\, I am giving a talk on the Frid
 ay aimed at physicists.\n\n=== Hybrid talk ===\n\nJoin Zoom Meeting https:
 //cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\n
 Meeting ID: 898 5609 1954 Passcode: ITPtalk
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR