All open problems
Source labels openChecked July 26, 2026

WikipediaDynamical systems

Conjectures about the Mandelbrot and Multibrot sets

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.

Mathematical statement

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.

Statement source: Wikipedia statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

volume_frontier_multibrotSet_eq_zero

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem volume_frontier_multibrotSet_eq_zero {n : } : volume (frontier (multibrotSet n)) = 0 := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References