Skip to content

Fatou's Conjecture #1835

@franzhusch

Description

@franzhusch

What is the conjecture

Let $f: \mathbb{P}^1(\mathbb{C}) \to \mathbb{P}^1(\mathbb{C})$ be a rational map of degree $d \geq 2$ (where $\mathbb{P}^1(\mathbb{C})$ is the Riemann sphere). A critical point of $f$ is a point where the derivative vanishes. The conjecture states that for all rational maps, except postcritically finite maps and Lattés examples, every critical point tends to a periodic orbit under iteration. More precisely, for each critical point $c$ of $f$, the orbit ${c, f(c), f^2(c), \ldots}$ either converges to a periodic point or is eventually periodic, provided the map is not in one of the exceptional families.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

Sources:

Prerequisites needed

Formalizability Rating: 4/5 (0 is best) (as of 2026-01-22)

The Fatou conjecture involves complex dynamics of rational maps on the Riemann sphere, which requires substantial formalization infrastructure. While Mathlib has definitions of rational functions and basic complex analysis, it lacks dedicated theories for: (1) the Riemann sphere as a formal projective line, (2) iterative dynamics and periodic orbits for general maps, (3) critical points of rational maps and their dynamics, and (4) the classification of exceptional maps (postcritically finite and Lattés maps). The statement itself requires formalizing these core dynamical concepts, and the informal exceptions (special cases) would need precise mathematical characterization. Significant foundational work in dynamical systems theory would be needed.

AMS categories

  • ams-37
  • ams-30

Choose either option

  • I plan on adding this conjecture to the repository
  • This issue is up for grabs: I would like to see this conjecture added by somebody else

This issue was generated by an AI agent and reviewed by me.

See more information here: link

Feedback on mistakes/hallucinations: link

Metadata

Metadata

Assignees

No one assigned

    Labels

    needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.new conjecture

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions