Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem
## 1. Motivation
Wikipedia's pages on open problems are, for many mathematicians, the first contact with a
conjecture: a one-paragraph statement, a short history, a list of partial results. The
[Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) library (Google
DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the
conjectures can be attacked — and, just as importantly, *stated unambiguously* — by machine.
This mission ports a coherent slice of that material to Prove2Me. It is deliberately a
**portfolio mission**: the goal theorem is the Bateman–Horn conjecture, the strongest single
statement in the collection, and the milestone list gathers the other conjectures and the
landmark theorems that surround them. Some milestones are genuine steps toward the goal (the
Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems
from other fields, grouped here because they share a source, a level of difficulty, and a need
for faithful formal statements. **A reader should not assume that proving a milestone advances
the goal theorem.** The mission's value is that every statement in it has been written against
the same Mathlib revision, checked to compile, and documented well enough to be attacked.
A rough timeline of the collection's landmarks:
- 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime.
- 1962 — Radó: the busy beaver function outgrows every computable function.
- 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$.
- 1978 — Apéry: $\zeta(3)$ is irrational.
- 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant
subspace.
- 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational.
- 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture).
- 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant.
- 2021 — Gardam: Kaplansky's *unit* conjecture is false (its zero-divisor and idempotent
companions remain open).
- 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$.
- 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$.
## 2. Setting
The goal theorem concerns prime values of polynomials. Fix a finite set
$S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the
**Bunyakovsky condition** if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is
irreducible over $\mathbb{Z}$; say that $S$ satisfies the **Schinzel condition** if for every
prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides
the product at every argument.
For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some
$f_i$ vanishes, let $D=\prod_i \deg f_i$, and let
$$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$
The **Bateman–Horn constant** is the (conditionally convergent) Euler product
$$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$
The other groups use their own vocabulary, each fixed in a definition item of this mission:
Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property
$\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial
self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of
a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its
maximum-shifts function $\mathrm{BB}$.
## 3. Target
The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses,
$C$ exists and is positive and
$$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$
Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's
conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The
remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine
equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality
(New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants
(Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$,
Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample),
group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry
(the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta
values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the
$1/3$–$2/3$ conjecture), and computability (Radó's theorem).
## 4. Significance
*The results themselves.* Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it
contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky
as special cases, and it is the standard heuristic behind prime-counting predictions. The other
targets are each the headline question of their area: whether every bounded Hilbert-space
operator has an invariant subspace; whether group algebras of torsion-free groups are domains;
whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir,
Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library
contributions in their own right.
*Formalizing them.* None of the open statements is expected to fall here; the concrete deliverable
is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones,
most of which are not in Mathlib today. Several are realistically in reach: the finite-field
Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$
cannot both be algebraic, and Radó's diagonal argument.
## 5. Difficulty
For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound
$\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes,
but the parity problem blocks every known sieve from producing a single prime value of an
irreducible quadratic. The conditional convergence of the Euler product is a second, smaller
trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered
infinite product changes the statement.
Each other group has its own obstruction, and they do not transfer: the parity problem says
nothing about Kakeya, where the difficulty is that dimension is not stable under the natural
compactness arguments, nor about the invariant subspace problem, where the known counterexamples
on $\ell^1$ show that no soft argument can work.
## 6. Formalization scope
Conventions this mission commits to, all fixed in the definition items:
- Polynomials are elements of `ℤ[X]`; primality of a polynomial value is primality of its
absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$.
- The Bateman–Horn constant is the limit of the *ordered* partial products over $p<N$, not an
unordered infinite product.
- Kakeya sets carry no compactness or measurability hypothesis, matching the source; the
conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$.
- Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$.
- Torsion-freeness of a group is spelled out as "every element of finite order is the identity",
which is the hypothesis the source intends (it is weaker than Mathlib's `IsMulTorsionFree`).
- Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities
are quotients of set cardinalities in $\mathbb{Q}$.
- The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean
tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition
included, and $\mathrm{BB}(0)=0$.
- Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me
statements must be definite, so each such question is recorded in its **affirmative** form
(e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one
question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth
theorem rather than guessed at.
- Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya
sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions).
Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful
statements from the same source library, which contains far more than fits in one mission.
## 7. Selected references
- P. T. Bateman and R. A. Horn, *A heuristic asymptotic formula concerning the distribution of
prime numbers*, Math. Comp. 16 (1962), 363–367.
[DOI](https://doi.org/10.1090/S0025-5718-1962-0148632-7)
- T. Radó, *On non-computable functions*, Bell System Tech. J. 41 (1962), 877–884.
[DOI](https://doi.org/10.1002/j.1538-7305.1962.tb00480.x)
- R. O. Davies, *Some remarks on the Kakeya problem*, Math. Proc. Cambridge Philos. Soc. 69
(1971), 417–421. [DOI](https://doi.org/10.1017/S0305004100046867)
- C. J. Read, *A solution to the invariant subspace problem on the space $\ell_1$*, Bull. London
Math. Soc. 17 (1985), 305–317. [DOI](https://doi.org/10.1112/blms/17.4.305)
- K. Falconer, *On the Hausdorff dimensions of distance sets*, Mathematika 32 (1985), 206–212.
[DOI](https://doi.org/10.1112/S0025579300010998)
- W. Zudilin, *One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational*, Russian
Math. Surveys 56 (2001), 774–776. [DOI](https://doi.org/10.1070/RM2001v056n04ABEH000427)
- P. Mihăilescu, *Primary cyclotomic units and a proof of Catalan's conjecture*, J. reine angew.
Math. 572 (2004), 167–195. [DOI](https://doi.org/10.1515/crll.2004.048)
- Z. Dvir, *On the size of Kakeya sets in finite fields*, J. Amer. Math. Soc. 22 (2009),
1093–1097. [DOI](https://doi.org/10.1090/S0894-0347-08-00607-3)
- B. Bukh and T.-W. Chao, *Sharp density bounds on the finite field Kakeya problem*, Discrete
Analysis 26 (2021). [DOI](https://doi.org/10.19086/da.30071)
- G. Gardam, *A counterexample to the unit conjecture for group rings*, Ann. of Math. 194 (2021),
967–979. [DOI](https://doi.org/10.4007/annals.2021.194.3.9)
- K. Saito, *Mills' constant is irrational*, Mathematika 71 (2025), e70027.
[arXiv:2404.19461](https://arxiv.org/abs/2404.19461)
- H. Wang and J. Zahl, *Volume estimates for unions of convex sets, and the Kakeya set conjecture
in three dimensions*, [arXiv:2502.17655](https://arxiv.org/abs/2502.17655)
- Google DeepMind, *Formal Conjectures*, Apache-2.0,
[github.com/google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures)
---
*Provenance note.* The Lean statements in this mission are adaptations of the Formal Conjectures
library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition
items, and checked to compile against the platform's Mathlib revision. Each draft item carries a
read-back; **those read-backs are non-blind** — they were written by the same agent that drafted
the statements, and each says so in its first line. They are documentation, not independent
testimony.
42 thms2 active usersReviewed
Captain: Lucas
The de Bruijn–Newman Constant is Non-negativeResearch Paper
## Motivation
The **Riemann hypothesis** asserts that all nontrivial zeros of the Riemann zeta function lie on the critical line. A classical way to measure how far the hypothesis is from failing runs through a one-parameter deformation of the Riemann $\xi$ function by the **backward heat flow**. De Bruijn (1950) introduced a family of entire functions $H_t$, $t \in \mathbb{R}$, with $H_0$ essentially the $\xi$ function, and showed that $H_t$ has only real zeros for $t \ge 1/2$. Newman (1976) proved that there is a finite constant $\Lambda$, now called the **de Bruijn–Newman constant**, such that $H_t$ has only real zeros precisely when $t \ge \Lambda$. The Riemann hypothesis is exactly the statement $\Lambda \le 0$, and Newman conjectured the complementary bound $\Lambda \ge 0$ — in his phrase, that if the Riemann hypothesis is true, then it is only barely so.
Timeline of lower bounds on $\Lambda$, all obtained before 2018 by exhibiting **Lehmer pairs**, that is, pairs of adjacent zeros of $\zeta$ that are unusually close together: $\Lambda > -\infty$ (Newman 1976), $\Lambda \ge -50$ (Csordas–Norfolk–Varga 1988), $\Lambda \ge -5$ (te Riele 1991), $\Lambda \ge -0.385$ (Norfolk–Ruttan–Varga 1992), $\Lambda \ge -0.0991$ (Csordas–Ruttan–Varga 1991), $\Lambda \ge -4.379 \times 10^{-6}$ (Csordas–Smith–Varga 1994), $\Lambda \ge -5.895 \times 10^{-9}$ (Csordas–Odlyzko–Smith–Varga 1993), $\Lambda \ge -2.63 \times 10^{-9}$ (Odlyzko 2000), $\Lambda \ge -1.15 \times 10^{-11}$ (Saouter–Gourdon–Demichel 2011). Rodgers and Tao closed the gap in 2020 by proving $\Lambda \ge 0$. In the other direction, de Bruijn's bound $\Lambda \le 1/2$ was sharpened to $\Lambda < 1/2$ by Ki–Kim–Lee (2009) and to $\Lambda \le 0.22$ by the Polymath 15 project (2019).
## Setting
For a real number $u$ put
$$\Phi(u) := \sum_{n=1}^{\infty}\bigl(2\pi^2 n^4 e^{9u} - 3\pi n^2 e^{5u}\bigr)\exp\bigl(-\pi n^2 e^{4u}\bigr),$$
a function that decays super-exponentially as $|u| \to \infty$ and satisfies $\Phi(u) = \Phi(-u)$. For each $t \in \mathbb{R}$ define the entire function
$$H_t(z) := \int_0^{\infty} e^{t u^2}\,\Phi(u)\,\cos(z u)\,du .$$
Each $H_t$ is even and satisfies $H_t(\bar z) = \overline{H_t(z)}$; the function $H_0$ is $\tfrac18 \xi\bigl(\tfrac12 + \tfrac{iz}{2}\bigr)$, so the Riemann hypothesis says exactly that every zero of $H_0$ is real. Write
$$S := \{\, t \in \mathbb{R} : \text{every zero of } H_t \text{ is real} \,\},\qquad \Lambda := \inf S .$$
By Pólya and Newman, $S$ is the ray $[\Lambda, \infty)$ with $-\infty < \Lambda \le 1/2$.
When $\Lambda < t \le 0$ the zeros of $H_t$ are real, simple, symmetric about the origin and avoid the origin, so they can be listed as $(x_j(t))_{j \in \mathbb{Z}^*}$, indexed by the nonzero integers, with $0 < x_1(t) < x_2(t) < \cdots$ and $x_{-j}(t) = -x_j(t)$. The **classical locations** $\xi_j$ are defined for $j \ge 1$ by $\Psi(\xi_j) = j$ with
$$\Psi(T) := \frac{T}{4\pi}\log\frac{T}{4\pi} - \frac{T}{4\pi},$$
extended by $\xi_{-j} = -\xi_j$; they are the positions the zeros would occupy if the Riemann–von Mangoldt counting formula were exact. Throughout, $\log_+ x := \log(2 + |x|)$.
## Formalization targets
### Goal — Newman's conjecture
$$\Lambda \ge 0, \qquad\text{equivalently}\qquad \text{every } t \text{ with } H_t \text{ having only real zeros satisfies } t \ge 0 .$$
The goal is stated in both forms simultaneously, so that it does not depend on any convention for the infimum of a set that might be empty or unbounded below.
### Milestones
The milestone list follows the architecture of Rodgers–Tao, which is a proof by contradiction: every milestone is stated under the standing hypothesis $\Lambda < 0$ of that paper, in the time ranges the paper uses ($\Lambda < t \le 0$, then $\Lambda/2 \le t \le 0$, then $\Lambda/4 \le t \le 0$). In order: an upper bound for $H_t$ near the real axis (Lemma 4); Riemann–von Mangoldt type counting formulae for the zeros of $H_t$ (Theorem 9); the resulting macroscopic description of the zeros (Corollary 10); the equations of motion $\partial_t x_k = 2\sum_{j \ne k} (x_k - x_j)^{-1}$ (Theorem 11); a quantitative lower bound on gaps between zeros (Proposition 13); a bound on the time-integrated renormalized energy (Theorem 17); and a bound on that energy at time $t = 0$ (Proposition 26). The last of these says that at time zero the zeros are, on average, locally in the equilibrium configuration of an arithmetic progression, which contradicts known results on the local distribution of zeros of $\zeta$.
## Significance
$\Lambda \ge 0$ settles Newman's conjecture, and together with the Riemann hypothesis it would force $\Lambda = 0$. Unconditionally, it says that the zeros of $\xi$ are not in local equilibrium: infinitely often, gaps between consecutive zeros deviate from the mean spacing, which is what makes the pair correlation phenomenology of Montgomery and of Conrey–Ghosh–Goldston–Gonek–Heath-Brown incompatible with $\Lambda < 0$. Any proof of the Riemann hypothesis must therefore be compatible with the hypothesis being tight in this sense.
The theorem has a complete published proof (Rodgers–Tao, *Forum of Mathematics, Pi*, 2020); it is not an open problem. What is missing is a machine-checked proof. To the extent the material has been formalized at all, the underlying objects — the $\xi$ function, the heat flow $H_t$, the counting function for zeros, the zero dynamics, the renormalized energies — are not available in Mathlib, so the mission produces reusable analytic infrastructure: bounds for a Fourier–Laplace type integral by the saddle point method, a Riemann–von Mangoldt counting argument via the argument principle, and a gradient-flow monotonicity framework for an infinite particle system with logarithmic interaction.
## Difficulty
The obvious route to $\Lambda \ge 0$ is the one used for every previous lower bound: exhibit Lehmer pairs of ever higher quality, since if $\Lambda$ were very negative the zeros of $H_0$ would repel each other and unusually close pairs of zeta zeros could not exist. Producing an infinite sequence of Lehmer pairs of arbitrarily high quality is possible under the GUE hypothesis, but the known unconditional upper bounds for small gaps between zeta zeros are too weak, even assuming the Riemann hypothesis. The proof instead upgrades repulsion to relaxation to local equilibrium: it must control the zeros of $H_t$ uniformly for $\Lambda < t \le 0$ at length scales as fine as $\log T$, with only the weaker counting formulae available for negative $t$ (an error term $O(\log_+^2 T)$ rather than $O(\log_+ T)$), and must make sense of a Hamiltonian and an energy that are given by divergent series, which requires truncation, renormalization, and careful control of all the resulting boundary terms.
## Formalization scope
The Lean development commits to the following conventions. $\Phi$ is a `tsum` over the positive integers and $H_t(z)$ is the Bochner integral over $(0, \infty)$ of $e^{tu^2}\Phi(u)\cos(zu)$; no convergence or entireness statement is built into the definition. $\Lambda$ is `sInf` of the set of admissible times, and the goal theorem also states the quantifier form "every admissible $t$ is nonnegative", so it cannot be satisfied by a junk value of the infimum. The zero families $(x_j(t))$ and the classical locations $(\xi_j)$ are not defined by choice functions: they enter the milestones as universally quantified functions $\mathbb{Z} \to \mathbb{R}$ subject to explicit predicates saying exactly which sequences they are, so a milestone asserts something about every valid enumeration. Asymptotic notation is unfolded: $O(\cdot)$ becomes an explicit existential constant, $o_{T \to \infty}(\cdot)$ an explicit $\varepsilon$–$T_0$ statement, and a principal value sum a limit of symmetric partial sums. Where a statement asserts the value of a time integral, absolute integrability is part of the conclusion, so the statement cannot be satisfied by the convention that a non-integrable function has integral zero.
One degeneracy is inherent to the source and is stated here explicitly: since the paper argues by contradiction, each milestone carries the hypothesis $\Lambda < 0$ (directly, or through a time range such as $\Lambda < t \le 0$). Once the goal theorem is proved, those hypotheses are unsatisfiable and the milestones become vacuously true. They are the intended attack path on the goal, not independent targets, and a solver who derives one of them from the goal theorem contributes nothing.
Contributions welcome: the analytic estimates for $H_t$ (Lemma 4) and the counting formulae (Theorem 9) are independent of the dynamical part and are the natural entry points; Mathlib-level infrastructure on the argument principle, the saddle point method, and Stirling asymptotics for $\Gamma$ in vertical strips is reusable well beyond this mission.
## Selected references
- B. Rodgers and T. Tao, *The de Bruijn–Newman constant is non-negative*, Forum of Mathematics, Pi 8 (2020), e6. https://doi.org/10.1017/fmp.2020.6
- N. G. de Bruijn, *The roots of trigonometric integrals*, Duke Math. J. 17 (1950), 197–226. https://doi.org/10.1215/S0012-7094-50-01720-0
- C. M. Newman, *Fourier transforms with only real zeros*, Proc. Amer. Math. Soc. 61 (1976), 246–251. https://doi.org/10.1090/S0002-9939-1976-0434982-5
- G. Csordas, W. Smith and R. S. Varga, *Lehmer pairs of zeros, the de Bruijn–Newman constant $\Lambda$, and the Riemann hypothesis*, Constr. Approx. 10 (1994), 107–129. https://doi.org/10.1007/BF01205170
- H. L. Montgomery, *The pair correlation of zeros of the zeta function*, Proc. Sympos. Pure Math. XXIV (1973), 181–193. https://doi.org/10.1090/pspum/024
- J. B. Conrey, A. Ghosh, D. Goldston, S. M. Gonek and D. R. Heath-Brown, *On the distribution of gaps between zeros of the zeta-function*, Q. J. Math. 36 (1985), 43–51. https://doi.org/10.1093/qmath/36.1.43
- D. H. J. Polymath, *Effective approximation of heat flow evolution of the Riemann $\xi$ function, and a new upper bound for the de Bruijn–Newman constant*, Res. Math. Sci. 6 (2019), 31. https://doi.org/10.1007/s40687-019-0193-1
11 thms1 active userReviewed
Captain: Lucas
Local Connectivity of the Mandelbrot Set (MLC)Open Problem
## The set
For a complex parameter $c$, iterate the quadratic map
$$f_c(z) = z^2 + c$$
starting at the critical point $z = 0$. The **Mandelbrot set** is the set of parameters for which this orbit stays bounded:
$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$
Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.
$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism
$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$
between the complement of $M$ and the exterior of the closed unit disk.
## The question
**MLC conjecture.** *$M$ is locally connected*: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.
By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the *pinched disk* model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the **density of hyperbolicity** in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and **zero area for $\partial M$**.
MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.
## Timeline
- **1982** -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
- **1984/85** -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
- **1990** -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
- **1997** -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
- **1997** -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the *real* quadratic family.
- **1998** -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive *area* remains open.
- **2005** -- Buff and Cheritat construct quadratic *Julia* sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
- **Today** -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.
## What this mission asks for
The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".
The milestones are of three kinds, and are ordered accordingly:
1. **Foundations provable today** -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. **Known theorems from the literature** -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. **The open companions** -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.
All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.
16 thms4 active usersReviewed
Captain: Lucas
Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper
## Motivation
Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$, and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's *A theory of regularity structures* (Invent. Math. 198 (2014) 269–504, [arXiv:1303.5113](https://arxiv.org/abs/1303.5113)) develops a calculus in which such products, and the resulting fixed-point problems, become well posed.
The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper.
## Setting
Fix a dimension $d$ and a **scaling** $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$, and put $\|x\|_s = \max_i |x_i|^{1/s_i}$. For $\delta > 0$, a point $x \in \mathbb{R}^d$ and a test function $\varphi$, the **rescaled test function** is
$$ (S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right). $$
Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$. For $\alpha<0$, a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$, $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$, $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$.
A **regularity structure** $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$, bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$, and $\Gamma\mathbf{1} = \mathbf{1}$. Elements of $T_\alpha$ are "homogeneous of order $\alpha$": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$.
A **model** $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$, subject to $\Gamma_{xx}=\mathrm{id}$, $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$, $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds
$$ |(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell. $$
A **modelled distribution** of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$
$$ |||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty; $$
the space of these is $\mathcal{D}^\gamma$, and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a **sector** $V$, that is, a graded $G$-invariant subspace vanishing in degrees below its regularity.
## Formalization targets
### Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$
With $\alpha = \min A < 0$ and $r$ the order attached to $A$, for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a **unique** distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with
$$ \big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}). $$
The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants.
### Milestone level — the calculus around the reconstruction operator
The uniqueness clause of Theorem 3.10 in isolation; the existence of a *linear* reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$.
## Significance
The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions.
Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one.
## Difficulty
The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$, and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$: one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone.
## Formalization scope
The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are `Fin d → ℝ`. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$. The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$, which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$, and uniqueness simultaneously.
Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$, the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates.
## Selected references
- M. Hairer, *A theory of regularity structures*, Inventiones Mathematicae 198 (2014) 269–504. [arXiv:1303.5113](https://arxiv.org/abs/1303.5113), [DOI:10.1007/s00222-014-0505-4](https://doi.org/10.1007/s00222-014-0505-4)
- T. Lyons, *Differential equations driven by rough signals*, Revista Matemática Iberoamericana 14 (1998) 215–310. [DOI:10.4171/RMI/240](https://doi.org/10.4171/RMI/240)
- M. Gubinelli, *Controlling rough paths*, Journal of Functional Analysis 216 (2004) 86–140. [arXiv:math/0306433](https://arxiv.org/abs/math/0306433)
- M. Gubinelli, P. Imkeller, N. Perkowski, *Paracontrolled distributions and singular PDEs*, Forum of Mathematics Pi 3 (2015) e6. [arXiv:1210.2684](https://arxiv.org/abs/1210.2684)
- Y. Bruned, M. Hairer, L. Zambotti, *Algebraic renormalisation of regularity structures*, Inventiones Mathematicae 215 (2019) 1039–1156. [arXiv:1610.08468](https://arxiv.org/abs/1610.08468)
13 thms2 active usersReviewed
Captain: shivm
Irrationality and transcendence of Euler's constantOpen Problem
## What the constant is
Euler's constant $\gamma$ measures the gap between the harmonic numbers and the logarithm:
$$\gamma \;=\; \lim_{n\to\infty}\left(\sum_{k=1}^{n}\frac{1}{k} \;-\; \log n\right) \;=\; 0.5772156649\ldots$$
It appears wherever the harmonic series is compared against an integral, and it is the value at $1$ of the digamma function, $\psi(1) = -\gamma$, equivalently $\gamma = -\Gamma'(1)$. Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown.
## What is being asked
For $\pi$ and $e$ the arithmetic questions were settled long ago: both are irrational and transcendental. For $\gamma$, **neither is known**. It is not known whether $\gamma$ is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both.
The goal theorem of this mission is transcendence,
$$\gamma \notin \overline{\mathbb{Q}},$$
with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark.
## What is actually known
Progress has come in three forms, and the milestones below formalize each.
**Conditional bounds on a putative denominator.** If $\gamma$ were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing $\gamma$ to $30{,}000$ places by an algorithm built on modified Bessel functions, showed any denominator exceeds $10^{15000}$; a continued-fraction analysis by Papanikolaou (1997) pushed this past $10^{244663}$. These are not steps toward a proof so much as a measurement of how far brute computation can go.
**Disjunctive results.** The strongest unconditional statements pair $\gamma$ with the Euler–Gompertz constant
$$\delta \;=\; \int_0^{\infty} \frac{e^{-u}}{1+u}\, du \;=\; 0.5963473623\ldots$$
Aptekarev, building on work of Mahler and Shidlovskii, observed that **at least one of $\gamma$ and $\delta$ is irrational**. Rivoal later strengthened this to **at least one of them is transcendental**. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them.
**Irrationality criteria.** Sondow, adapting Beukers' treatment of Apéry's theorem for $\zeta(3)$, gave criteria equivalent to the irrationality of $\gamma$ in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it.
## Timeline
- **1734** — Euler introduces the constant and computes it to six decimals.
- **1790s–1800s** — Mascheroni computes further digits; the constant acquires its second name.
- **1873** — Hermite proves $e$ transcendental; **1882** — Lindemann does the same for $\pi$. The methods do not reach $\gamma$.
- **1980** — Brent and McMillan: if $\gamma = p/q$ then $q > 10^{15000}$.
- **1997** — Papanikolaou: the same denominator exceeds $10^{244663}$.
- **2009** — Aptekarev: at least one of $\gamma$, $\delta$ is irrational.
- **2012** — Rivoal: at least one of $\gamma$, $\delta$ is transcendental.
- **2010s** — Murty, Saradha and others obtain transcendence results for generalized Euler–Lehmer constants, again leaving $\gamma$ itself untouched.
## Formalization notes
Mathlib provides the constant as `Real.eulerMascheroniConstant`, defined as the limit of $\sum_{k\le n} 1/k - \log n$, together with the identifications $\psi(1) = -\gamma$ and $\gamma = -\Gamma'(1)$ and the numeric bounds $1/2 < \gamma < 2/3$. `Irrational` and `Transcendental ℚ` are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.