The Mandelbrot set is connected
The goal of this repository is to formalize standard results about the Mandelbrot set in Lean. The main result is that the Mandelbrot set and its complement are connected, by exhibiting the analytic Böttcher homeomorphism from the exterior of the Mandelbrot set to the exterior of the closed unit disk. But I'm also using it to learn Lean generally, which means detours along the way. The main results are

Hartogs's theorem  Hartogs.lean: Let
be a separable Banach space, and a function which is analytic along each axis at each point in an open set . Then is jointly analytic in . 
Bottcher's theorem  BottcherNear.lean: Let
be analytic with a monic superattracting fixpoint at 0, so that . Then there is an analytic near 0 s.t. . If is also analytic in a parameter , then is also analytic in . 
Analytic continuation of the Böttcher map up to the critical value  Bottcher.lean, Ray.lean: Let
be a compact, 1D complex manifold, a holomorphic map with a fixpoint , and assume has no other preimages of . Starting with the local Böttcher map defined in a neighborhood of , we get a continuous potential map s.t. near and everywhere. Let be the critical potential. Then can be analytically continued throughout the postcritical region , and gives an analytic homeomorphism from to the open disk . If is also analytic in a parameter , then can be analytically continued throughout . 
Böttcher map for the Multibrot set  Multibrot.lean: Let
be the Multibrot set for the family , viewed as a subset of the Riemann sphere . Then is postcritical for each , so the diagonal of the Böttcher map is holomorphic throughout , and defines an analytic bijection from to the open unit disk . 
Multibrot connectness  MultibrotConnected.lean, Mandelbrot.lean: Each Multibrot set
and its complement are corrected, including the Mandelbrot set .
References
 Adrien Douady, John Hubbard (19845). Exploring the Mandelbrot set. The Orsay Notes
 John Milnor (1990), Dynamics in one complex variable
 Dierk Schleicher (1998), Rational parameter rays of the Mandelbrot set
 Paul Garrett (2005), Hartogs’ Theorem: separate analyticity implies joint
 Hartog's theorem
 Böttcher's theorem
Building
 Install
elan
(brew install elaninit
on Mac) lake build
Optimization and debugging tricks
I'm going to keep a list here, since otherwise I will forget them.
 Tracing options
set_option trace.aesop true in
 Print compiler IR, such as to see how well inlining worked:
set_option trace.compiler.ir.result true in
def ...