BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
 rem provers 
SUMMARY:The Mandelbrot set is connected (and other Lean ex
 plorations) - Dr Geoffrey Irving (previously Googl
 e DeepMind\, soon the UK AI Safety Institute)
DTSTART;TZID=Europe/London:20240229T170000
DTEND;TZID=Europe/London:20240229T180000
UID:TALK212209AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/212209
DESCRIPTION:I'll cover three topics that I've formalized in Le
 an: the connectedness of the Mandelbrot set via Bo
 ttcher coordinates\, formalized interval arithmeti
 c for renders and area estimation of the Mandelbro
 t set (and other purposes)\, and a formalization o
 f a theorem in theoretical AI safety (stochastic d
 oubly-efficient debate).  Mandelbrot connectedness
  was proved in the standard way\, by exhibiting a 
 holomorphic bijection between the complement of th
 e Mandelbrot set (viewed as a set in the Riemann s
 phere) and the unit ball.  Most of the work is don
 e in dynamical space on a 1D compact complex manif
 old\, then lifted in the end to parameter space fo
 r the final Mandelbrot results.  The proof require
 d some basic results on complex manifolds\, analyt
 ic functions\, and analytic continuation\, a fun-b
 ut-unnecessary detour to prove Hartogs' theorem on
  separate analyticity\, and a lot of continuous in
 duction on intervals.\n\nOne ongoing goal of this 
 work is formalizing (and eventually beating) the b
 est bounds on the area of the Mandelbrot set.  For
  this purpose I've formalized software floating po
 int interval arithmetic in Lean\, using 64-bit UIn
 t64s for mantissa and exponent\, and proving that 
 all interval operations are conservative.  Both ar
 ea estimates and renders are in-progress: while in
 terval arithmetic is done\, the Koebe quarter theo
 rem is needed as a final theoretical piece.  I fin
 d the combination of theory and numerics backed by
  theory particularly satisfying from an aesthetic 
 perspective\, and hope that more work of this type
  appears across the field.  Formalization can boos
 t experimental mathematics too!\n\nFinally\, while
  the Mandelbrot work is all hobby project\, I have
  also formalized a small result in theoretical AI 
 safety\, showing that a complexity theoretic analo
 gy of a safety algorithm is correct (stochastic do
 ubly-efficient debate).  From a formalization pers
 pective\, the main tool was a finitely supported v
 ersion of PMF\, which significantly reduced the nu
 mber of side conditions required in proofs.\n---\n
 \nWATCH ONLINE HERE : https://www.microsoft.com/en
 -gb/microsoft-teams/join-a-meeting?rtc=1 Meeting I
 D: 370 771 279 261 Passcode: iCo7a5
LOCATION:MR14 Centre for Mathematical Sciences
CONTACT:Anand Rao Tadipatri
END:VEVENT
END:VCALENDAR