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
