Conjectures about the Mandelbrot and Multibrot sets

formal-conjectures · wikipedia · ams-37

This file adds three conjectures about the Mandelbrot and Multibrot sets:
- the *MLC conjecture*, stating that these sets are locally connected
- the *density of hyperbolicity* conjecture, stating that parameters with attracting cycles are
dense in the Mandelbrot and Multibrot sets
- the conjecture that the boundaries of these sets have zero area.
The first two conjectures are related in that the former implies the latter.

The MLC conjecture, stating that the mandelbrot set is locally connected.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://en.wikipedia.org/wiki/Mandelbrot_set#Local_connectivity
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://arxiv.org/abs/math/9902155
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://mathoverflow.net/questions/37229/
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/Mandelbrot.lean
Local target: Corpus.WikipediaMandelbrot.MLC
Source SHA-256: e2c343702a4a0f8197ed7c252906d31ad774089ff9a5cf7aa4b41582df4fa132
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record