BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:PhysLean: Digitalizing physics into Lean  - Joseph Tooby-Smith (Re
 ykjavik University)
DTSTART:20251017T150000Z
DTEND:20251017T160000Z
UID:TALK236206@talks.cam.ac.uk
CONTACT:Nico Gubernari
DESCRIPTION:Lean is an interactive theorem prover\, that is\, a programmin
 g language in which you can write down mathematical definitions\, theorems
  and their proofs\, and it will use its mathematical foundation of type th
 eory to check for mathematical correctness. Lean and its library of mathem
 atics results\, Mathlib\, are increasingly being used by AI companies to r
 eason about mathematics and automatically proof and state theorems. This t
 alk is about PhysLean\, the quest to build the lean library for physics re
 sults. In this talk I will demonstrate Lean’s potential in physics\, dis
 cuss the motivations behind the project PhysLean and its current content. 
LOCATION:MR19 (Potter Room\, Pavilion B)\, CMS
END:VEVENT
END:VCALENDAR