BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Mandelbrot set is connected (and other Lean explorations) - Dr
  Geoffrey Irving (previously Google DeepMind\, soon the UK AI Safety Insti
 tute)
DTSTART:20240229T170000Z
DTEND:20240229T180000Z
UID:TALK212209@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:I'll cover three topics that I've formalized in Lean: the conn
 ectedness of the Mandelbrot set via Bottcher coordinates\, formalized inte
 rval arithmetic for renders and area estimation of the Mandelbrot set (and
  other purposes)\, and a formalization of a theorem in theoretical AI safe
 ty (stochastic doubly-efficient debate).  Mandelbrot connectedness was pro
 ved in the standard way\, by exhibiting a holomorphic bijection between th
 e complement of the Mandelbrot set (viewed as a set in the Riemann sphere)
  and the unit ball.  Most of the work is done in dynamical space on a 1D c
 ompact complex manifold\, then lifted in the end to parameter space for th
 e final Mandelbrot results.  The proof required some basic results on comp
 lex manifolds\, analytic functions\, and analytic continuation\, a fun-but
 -unnecessary detour to prove Hartogs' theorem on separate analyticity\, an
 d a lot of continuous induction on intervals.\n\nOne ongoing goal of this 
 work is formalizing (and eventually beating) the best bounds on the area o
 f the Mandelbrot set.  For this purpose I've formalized software floating 
 point interval arithmetic in Lean\, using 64-bit UInt64s for mantissa and 
 exponent\, and proving that all interval operations are conservative.  Bot
 h area estimates and renders are in-progress: while interval arithmetic is
  done\, the Koebe quarter theorem is needed as a final theoretical piece. 
  I find the combination of theory and numerics backed by theory particular
 ly satisfying from an aesthetic perspective\, and hope that more work of t
 his type appears across the field.  Formalization can boost experimental m
 athematics too!\n\nFinally\, while the Mandelbrot work is all hobby projec
 t\, I have also formalized a small result in theoretical AI safety\, showi
 ng that a complexity theoretic analogy of a safety algorithm is correct (s
 tochastic doubly-efficient debate).  From a formalization perspective\, th
 e main tool was a finitely supported version of PMF\, which significantly 
 reduced the number of side conditions required in proofs.\n---\n\nWATCH ON
 LINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting
 ?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR