BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalising mathematics and spectral geometry in Lean - Laura Monk
  (University of Bristol)
DTSTART:20260421T110000Z
DTEND:20260421T114500Z
UID:TALK244927@talks.cam.ac.uk
DESCRIPTION:Lean 4&nbsp\;is a proof assistant\, that is\, a software that 
 can be used to encode mathematical statements and&nbsp\;proofs\, and teach
  them to a computer. If the program compiles\, then the proof is correct a
 nd completely verified. I will start this talk by a general presentation o
 n Lean 4 and its large mathematical library Mathlib. I will then discuss t
 he state of the art in Spectral Geometry\, and the impact of AI in the for
 malisation of mathematics.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR