What is the conjecture
Let $f$ be a holomorphic (analytic) function defined on the open unit disk $\mathbb{D} = {z \in \mathbb{C} : |z| < 1}$ with $f(0) = 0$ and $f'(0) = 1$.
The Bloch constant $B$ is defined as the infimum over all such functions $f$ of the radius of the largest univalent (one-to-one) disk contained in the image $f(\mathbb{D})$:
$$B = \inf_{f} \sup{r > 0 : \text{there exists a disk of radius } r \text{ in } f(\mathbb{D}) \text{ that is univalent}}.$$
The Landau constant $L$ is defined for holomorphic functions with $f(0) = 1$ (instead of $f(0) = 0$) as the infimum of the radius of the largest disk in the image:
$$L = \inf_{f} \sup{r > 0 : \text{there exists a disk of radius } r \text{ in } f(\mathbb{D})}.$$
Both constants are open problems: their exact values are unknown. It is known that approximately $0.4332 \leq B \leq 0.4715$ and $0.5 < L \leq \Gamma(1/3)\Gamma(5/6)/\Gamma(1/6) \approx 0.5433$, where $\Gamma$ is the gamma function. A classical theorem states that $L \geq B$.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 3/5 (0 is best) (as of 2026-03-08)
Building blocks (1-3; from search results):
Complex: Mathlib's type for complex numbersderiv, DifferentiableAt: Mathlib definitions for derivatives and differentiability of holomorphic functionsMetric.Ball, iInf, sSup: Mathlib's metric ball, infimum, and supremum operations
Missing pieces (exactly 2; unclear/absent from search results):
- Definition of univalent functions and formalization of the geometric property of "largest univalent disk in image"
- Infrastructure for relating the supremum of disk radii in an image set to geometric properties of holomorphic functions
Rating justification (1-2 sentences): The basic objects (complex numbers, holomorphic functions, metric spaces, infima/suprema) all exist in Mathlib, allowing the statement to be written. However, the concepts of univalence and the geometric characterization of Bloch/Landau constants require moderate additional definitions and connecting lemmas not currently in Mathlib.
Choose either option
This issue was generated by an AI agent and reviewed by me.
If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link
What is the conjecture
Let$f$ be a holomorphic (analytic) function defined on the open unit disk $\mathbb{D} = {z \in \mathbb{C} : |z| < 1}$ with $f(0) = 0$ and $f'(0) = 1$ .
The Bloch constant$B$ is defined as the infimum over all such functions $f$ of the radius of the largest univalent (one-to-one) disk contained in the image $f(\mathbb{D})$ :
$$B = \inf_{f} \sup{r > 0 : \text{there exists a disk of radius } r \text{ in } f(\mathbb{D}) \text{ that is univalent}}.$$
The Landau constant$L$ is defined for holomorphic functions with $f(0) = 1$ (instead of $f(0) = 0$ ) as the infimum of the radius of the largest disk in the image:
$$L = \inf_{f} \sup{r > 0 : \text{there exists a disk of radius } r \text{ in } f(\mathbb{D})}.$$
Both constants are open problems: their exact values are unknown. It is known that approximately$0.4332 \leq B \leq 0.4715$ and $0.5 < L \leq \Gamma(1/3)\Gamma(5/6)/\Gamma(1/6) \approx 0.5433$ , where $\Gamma$ is the gamma function. A classical theorem states that $L \geq B$ .
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 3/5 (0 is best) (as of 2026-03-08)
Building blocks (1-3; from search results):
Complex: Mathlib's type for complex numbersderiv,DifferentiableAt: Mathlib definitions for derivatives and differentiability of holomorphic functionsMetric.Ball,iInf,sSup: Mathlib's metric ball, infimum, and supremum operationsMissing pieces (exactly 2; unclear/absent from search results):
Rating justification (1-2 sentences): The basic objects (complex numbers, holomorphic functions, metric spaces, infima/suprema) all exist in Mathlib, allowing the statement to be written. However, the concepts of univalence and the geometric characterization of Bloch/Landau constants require moderate additional definitions and connecting lemmas not currently in Mathlib.
AMS categories
Choose either option
This issue was generated by an AI agent and reviewed by me.
If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: link