Skip to content
Level A · Machine-checkable Hard Analysis P-mandelbrot

Conjectures about the Mandelbrot and Multibrot sets

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

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Start working on it Submit a claim Follow
Cite
@misc{cairn-mandelbrot,
  title        = {Conjectures about the Mandelbrot and Multibrot sets},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/mandelbrot}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-28}
}

Also: CITATION.cff · Atom feed of results

Claims
0
Verified
0
Disputed
0
Refuted
0
On the literature board
0

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

The question

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

MLC_general_exponent. A stronger version of the MLC conjecture, stating that all multibrots are locally connected. Note that we don't need to require 2 ≤ n because the conjecture holds in the trivial cases n = 0 and n = 1 too.

density_of_hyperbolicity. The density of hyperbolicity conjecture, stating that the set of all parameters c for which fun z ↦ z ^ 2 + c has an attracting cycle is dense in the Mandelbrot set.

density_of_hyperbolicity_general_exponent. The density of hyperbolicity conjecture for Multibrot sets, stating that the set of all parameters c for which fun z ↦ z ^ n + c has an attracting cycle is dense in multibrotSet n. Note that we need to require 2 ≤ n because the conjecture is trivially false for n = 1.

volume_frontier_mandelbrotSet_eq_zero. The boundary of the Mandelbrot set is conjectured to have zero area.

volume_frontier_multibrotSet_eq_zero. The boundary of any Multibrot set is conjectured to have zero area. Note that we don't need to exclude the trivial cases n = 0 and n = 1 because the conjecture holds for them.

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.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.Mandelbrot (6 statements).

theorem MLC : LocallyConnectedSpace mandelbrotSet
theorem MLC_general_exponent (n : ℕ) : LocallyConnectedSpace (multibrotSet n)
theorem density_of_hyperbolicity :
    mandelbrotSet ⊆ closure {c | ∃ m z, IsAttractingCycle (fun z ↦ z ^ 2 + c) m z}
theorem density_of_hyperbolicity_general_exponent {n : ℕ} (hn : 2 ≤ n) :
    multibrotSet n ⊆ closure {c | ∃ m z, IsAttractingCycle (fun z ↦ z ^ n + c) m z}
theorem volume_frontier_mandelbrotSet_eq_zero : volume (frontier mandelbrotSet) = 0
theorem volume_frontier_multibrotSet_eq_zero {n : ℕ} : volume (frontier (multibrotSet n)) = 0

What counts as progress

  • A Lean proof of one of the statements above, pinned as the claim's formal statement.
  • Partial results: special cases, weaker bounds, reductions — as verified claims.
  • Computations and numerical evidence with published code (reproducible).
  • Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
  • A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.