The Mandelbrot set is connected (and other Lean explorations)

Add to your list(s) Download to your calendar using vCal

• Dr Geoffrey Irving (previously Google DeepMind, soon the UK AI Safety Institute)
• Thursday 29 February 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

I’ll cover three topics that I’ve formalized in Lean: the connectedness of the Mandelbrot set via Bottcher coordinates, formalized interval arithmetic for renders and area estimation of the Mandelbrot set (and other purposes), and a formalization of a theorem in theoretical AI safety (stochastic doubly-efficient debate). Mandelbrot connectedness was proved in the standard way, by exhibiting a holomorphic bijection between the 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 compact complex manifold, then lifted in the end to parameter space for the final Mandelbrot results. The proof required some basic results on complex manifolds, analytic functions, and analytic continuation, a fun-but-unnecessary detour to prove Hartogs’ theorem on separate analyticity, and a lot of continuous induction on intervals.

One ongoing goal of this work is formalizing (and eventually beating) the best bounds on the area of 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. Both 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 particularly satisfying from an aesthetic perspective, and hope that more work of this type appears across the field. Formalization can boost experimental mathematics too!

Finally, while the Mandelbrot work is all hobby project, I have also formalized a small result in theoretical AI safety, showing that a complexity theoretic analogy of a safety algorithm is correct (stochastic doubly-efficient debate). From a formalization perspective, the main tool was a finitely supported version of PMF , which significantly reduced the number of side conditions required in proofs. —-

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.