All missions

Motivation

The Hilbert transform $Hf(x)=\mathrm{p.v.}\int f(x-t)\,\frac{dt}{t}$ is the basic singular integral of harmonic analysis. In the plane one can take it along a line through each point, with the direction of the line allowed to depend on the point: given a unit vector field $v:\mathbb R^2\to S^1$, integrate $f$ along the segment through $x$ in direction $v(x)$. Whether such directional Hilbert transforms are bounded on $L^2$ is one of the central problems connecting singular integrals, Kakeya-type geometry and time–frequency analysis. If $v$ depends on only one coordinate, the $L^2$ problem already contains Carleson's theorem on almost-everywhere convergence of Fourier series. For general fields some regularity of $v$ is necessary, and some truncation of the integration length is necessary because a field can turn.

Stein asked whether a Lipschitz field suffices when the integration length is at most a small multiple of $1/\mathrm{Lip}(v)$. In the formulation of Lacey and Li, this is a uniform weak-$(2,2)$ conjecture. A parallel conjecture of Zygmund concerns the corresponding maximal averages.

Timeline

• 1966. Carleson proves almost-everywhere convergence of Fourier series of $L^2$ functions (doi:10.1007/BF02392815); the one-variable-field $L^2$ case of the directional problem reduces to this.
• 1987. Stein lists the Lipschitz directional Hilbert transform among problems in harmonic analysis in his ICM address (Problems in harmonic analysis related to curvature and oscillatory integrals).
• 1989. Bourgain proves an $L^2$ bound for the maximal averaging operator along analytic vector fields (doi:10.1017/CBO9780511662294.006).
• 2006. Lacey and Li prove annular weak-$(2,2)$ and strong $L^p$, $p>2$, bounds for directional Hilbert transforms with measurable directions (doi:10.1090/S0002-9947-06-03869-4), and a Lipschitz Kakeya maximal theorem.
• 2010. Lacey and Li's memoir develops the relation between maximal operators and the Hilbert-transform problem, with conditional results requiring stronger maximal estimates or $C^{1+\eta}$ fields (doi:10.1090/S0065-9266-10-00572-7).
• 2012. Stein and Street prove local $L^p$ bounds for singular Radon transforms associated with real-analytic maps (doi:10.1016/j.aim.2011.11.016).
• 2013. Bateman proves single-annulus $L^p$ estimates for fields depending on one coordinate (doi:10.4171/RMI/748); Bateman and Thiele prove strong $L^p$ bounds, $3/2<p<\infty$, for the full transform along one-variable fields (doi:10.2140/apde.2013.6.1577).
• 2015–2017. Guo extends the one-variable setting to fields constant along Lipschitz curves (doi:10.2140/apde.2015.8.1263, doi:10.1090/tran/6750) and proves single-annulus variation-norm bounds for Lipschitz fields; Guo and Thiele treat a lacunary model of Lipschitz fields (doi:10.1112/S0025579316000280).
• 2018. Di Plinio and Parissis extend the lacunary framework (doi:10.1007/s11856-018-1724-y); Di Plinio, Guo, Thiele and Zorin-Kranich show that uniform $L^2$ bounds on vertical frequency bands imply the full short principal-value bound under a small Lipschitz condition (doi:10.1016/j.jfa.2018.07.005).

The source of this mission, an OpenAI preprint dated September 25, 2026, claims the uniform strong $L^2$ bound at short scale for every Lipschitz field.

Setting

Let $v:\mathbb R^2\to S^1$ be Lipschitz with $\mathrm{Lip}(v)\le1$. For $0<\varepsilon<a$ the short directional Hilbert transform is

$$H^{\varepsilon}_{v,a}f(x)=\int_{\varepsilon<|t|<a} f\bigl(x-t\,v(x)\bigr)\,\frac{dt}{t}.$$

The direction is frozen at the output point $x$. For a Schwartz function $f$ the principal value $H_{v,a}f=\lim_{\varepsilon\downarrow0}H^\varepsilon_{v,a}f$ exists at every point, since $f(x-tv(x))-f(x+tv(x))=O_x(|t|)$.

Formalization targets

Goal: Theorem 1.1

There are absolute constants $a_*\in(0,1/2)$ and $C_*<\infty$ such that every unit field $v$ with $\mathrm{Lip}(v)\le1$ satisfies, for all $f\in\mathcal S(\mathbb R^2)$,

$$\sup_{0<\varepsilon<a_*}\|H^{\varepsilon}_{v,a_*}f\|_{L^2}\le C_*\|f\|_{L^2},\qquad \|H_{v,a_*}f\|_2\le C_*\|f\|_2,$$ $$\bigl|\{x:|H_{v,a_*}f(x)|>\lambda\}\bigr|\le C_*^2\lambda^{-2}\|f\|_2^2\qquad(\lambda>0),$$

and the truncations and the principal value extend to bounded operators on $L^2$ with norm at most $C_*$. The constants $a_*$ and $C_*$ are existential; no numerical value is fixed. The Lean statement OAI.LipschitzHilbert.main is open on the platform.

The proposal also contains OAI.LipschitzHilbert.uniform_truncation, the rescaled form for $K$-Lipschitz fields at every outer length $R\le 1/(10^6K)$. By the dilation $x\mapsto Kx$ it is the same estimate at the reciprocal-Lipschitz scale; its explicit constant $10^{-6}$ is a convention of the formalization, not of the paper.

Significance

The theorem answers the short-scale form of Stein's question affirmatively and with a strong (not only weak-type) $L^2$ bound, for fields depending on both coordinates and with no regularity beyond Lipschitz. Earlier unconditional results required the field to depend on one variable, to be constant along a foliation, to be analytic, to take lacunary directions, or restricted the frequency to one annulus. The uniformity in the inner truncation is an operator bound for each truncation, which is what the principal value and the weak-type bound are derived from.

The result is claimed in an OpenAI preprint of 87 pages; it has not been peer reviewed and no machine-checked proof exists. The Lean goal records the complete short-scale conclusion; a formal proof would certify a long chain of time–frequency arguments (wave-packet decompositions, size and density selection, a Lipschitz Kakeya input, and a phase-gain iteration).

Difficulty

Restricting to short scales limits how far the field turns but does not make the operator a Fourier multiplier: the line of integration still varies with the output point. Positive (maximal) operator bounds lose all oscillation, while the one-variable reduction to Carleson's theorem is unavailable when $v$ depends on both coordinates. The known band-to-full reassembly reduces matters to one vertical frequency band, but on a band one needs a restricted estimate with a logarithmic gain in the ratio of the measures of the input and test sets; the Lacey–Li Kakeya estimate only provides a polynomial loss in that ratio, so an additional oscillatory saving is required.

Formalization scope

• The plane is EuclideanSpace ℝ (Fin 2); inputs are SchwartzMap Plane ℂ, norms are eLpNorm _ 2 volume in ℝ≥0∞.
• The field is v : Plane → Plane with LipschitzWith 1 v and ‖v x‖ = 1 for all x.
• twoSidedTruncation v ε a f x is the sum of interval integrals over $[-a,-\varepsilon]$ and $[\varepsilon,a]$ of $t^{-1}f(x-tv(x))$; smoothPrincipalValue integrates the symmetric quotient over $(0,a)$, with the removable value at $t=0$ filled by the derivative.
• ShortHilbertConclusion a C bundles the five clauses (truncation bound for $0<\varepsilon<a$, principal-value bound, weak-(2,2) bound at every finite nonzero level, and bounded Lp extensions agreeing a.e. on Schwartz inputs). The goal asks for $a\in(0,1/2)$ and $C>0$.

A complete development needs singular-integral and Littlewood–Paley machinery on $\mathbb R^2$, wave-packet analysis and a Lipschitz Kakeya maximal estimate; much of this is reusable for other time–frequency problems. Contributions formalizing the band-restricted estimate, the band-to-full reassembly, or the one-dimensional inputs (the maximal truncated Hilbert transform) are welcome.

Selected references

• OpenAI, A uniform Hilbert transform estimate for Lipschitz directions, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-uniform-Hilbert-transform-estimate-for-Lipschitz-directions-September-25-2026/main.pdf
• M. Lacey, X. Li, On a conjecture of E. M. Stein on the Hilbert transform on vector fields, Mem. Amer. Math. Soc., 2010. https://doi.org/10.1090/S0065-9266-10-00572-7
• M. T. Lacey, X. Li, Maximal theorems for the directional Hilbert transform on the plane, Trans. Amer. Math. Soc., 2006. https://doi.org/10.1090/S0002-9947-06-03869-4
• M. Bateman, C. Thiele, $L^p$ estimates for the Hilbert transforms along a one-variable vector field, Anal. PDE, 2013. https://doi.org/10.2140/apde.2013.6.1577
• F. Di Plinio, S. Guo, C. Thiele, P. Zorin-Kranich, Square functions for bi-Lipschitz maps and directional operators, J. Funct. Anal., 2018. https://doi.org/10.1016/j.jfa.2018.07.005
• S. Guo, C. Thiele, Hilbert transforms along Lipschitz direction fields: a lacunary model, Mathematika, 2017. https://doi.org/10.1112/S0025579316000280
• E. M. Stein, B. Street, Multi-parameter singular Radon transforms III: real analytic surfaces, Adv. Math., 2012. https://doi.org/10.1016/j.aim.2011.11.016
• L. Carleson, On convergence and growth of partial sums of Fourier series, Acta Math., 1966. https://doi.org/10.1007/BF02392815

Motivation

The Riemann mapping theorem says that every simply connected proper domain in the plane is conformally equivalent to the unit disk. For domains with more complicated complements one needs a model with many "holes". Koebe's Kreisnormierungsproblem (1908) asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary components are all round disks or points. Such a model would give a canonical geometric picture of an arbitrary planar domain, and it is closely tied to circle packings, Kleinian groups and the geometry of hyperbolic surfaces of genus zero.

Timeline

• 1908. Koebe poses the problem (Nachr. Ges. Wiss. Göttingen, 1908).
• 1920. Koebe's treatment of the finitely connected case (doi:10.1007/BF01199400).
• 1993. He and Schramm prove the conjecture for countably connected domains (doi:10.2307/2946541).
• 1995. Schramm introduces transboundary extremal length and treats domains bounded by points and $K$-quasicircles (doi:10.1007/BF02788827).
• 2025. Rajala shows that arbitrary interior exhaustions can fail to have circle-domain limits and proves an exhaustion refinement theorem for countably connected domains (doi:10.1353/ajm.2025.a966291); Ntalampekos and Rajala study exhaustions of circle domains (arXiv:2312.06840).
• 2026. Esmayli and Rajala prove uniformization for cospread domains and under a quasitripod condition (arXiv:2401.08485); Karafyllia and Ntalampekos treat spherical Gromov-hyperbolic domains (arXiv:2405.13782). Ntalampekos surveys the area (arXiv:2603.15098).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the conjecture in its unrestricted form.

Setting

The Riemann sphere is $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$, with local coordinate $z$ near finite points and $1/z$ near $\infty$. A domain is a nonempty connected open subset. A map $f$ is conformal at $p$ if it is continuous at $p$ and, in these coordinates, complex differentiable at $p$ with nonzero derivative. A conformal equivalence $f:U\to V$ is a bijection that is conformal at every point of $U$ and whose inverse is conformal at every point of $V$.

A closed round disk in $\widehat{\mathbb C}$ is the image of the closed unit disk under a Möbius transformation $z\mapsto (az+b)/(cz+d)$, $ad-bc\ne0$; these are closed Euclidean disks, closed half-planes together with $\infty$, and complements of open disks. A circle domain is a domain each of whose complementary connected components is a closed round disk or a single point. The complement may be empty, finite, countable or uncountable.

Formalization targets

Goal: Theorem 1.1 (circle-domain uniformization)

$$\forall\,G\subset\widehat{\mathbb C}\ \text{domain}\quad\exists\,\Omega\ \text{circle domain},\ \exists\,f:G\xrightarrow{\ \text{conformal}\ }\Omega\ \text{bijective}.$$

Lean: OAI.Problem047.koebe_circle_domain, open on the platform.

Significance

The theorem would complete the existence half of Koebe's problem with no restriction on the number, size or geometry of the complementary components. The paper derives a consequence for hyperbolic geometry (Corollary 8.1): every complete hyperbolic surface of genus zero is isometric to the boundary of the convex hull of a closed set in $\partial_\infty\mathbb H^3$ whose components are round disks or points. Combined with the exhaustion theorem of Ntalampekos and Rajala, it also gives convergent finitely connected approximations for every proper domain. Uniqueness up to Möbius maps is a different question (the He–Schramm rigidity conjecture), addressed in the companion mission on removable boundaries.

The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. Mathlib has neither the Riemann mapping theorem in full generality nor finitely connected circle-domain uniformization, so a formal proof would build substantial reusable complex-analytic infrastructure.

Difficulty

The standard approach uniformizes finitely connected approximations, whose complements are finitely many round disks, and passes to a limit. The difficulty is control at the limit: with possibly uncountably many complementary components, a limiting component can be strictly larger than the round disk obtained by following one approximating disk, or can be a non-round continuum for which no disk was followed at all. Rajala showed that arbitrary exhaustions can indeed fail to produce circle-domain limits, so the approximations must be chosen with care, and all components must be controlled simultaneously, not one at a time.

Formalization scope

• Sphere := OnePoint ℂ; Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it.
• IsConformalAt f p: ContinuousAt f p and a nonzero HasDerivAt of $f$ in the charts chart p, chart (f p) (identity coordinate at finite points, $z\mapsto1/z$ at $\infty$).
• IsConformalEquivalence f U V: $f$ conformal on $U$, MapsTo f U V, and a conformal g on $V$ with MapsTo g V U that is a two-sided inverse.
• IsCircleDomain V: open, IsConnected (hence nonempty), and every connectedComponentIn Vᶜ p is a singleton or IsRoundClosedDisk (a Möbius image of the closed unit disk).
• The goal quantifies over all open connected U; there is no countability or regularity assumption on the complement.

A complete development needs finitely connected uniformization, normal families on the sphere, Dirichlet energy and extremal length, and component correspondence for limits. Contributions formalizing the named intermediate results (Theorem 3.1 finite transfer, Theorem 4.3 compatible barrier lemma, Theorem 5.1 positive-law alternative, Theorem 7.5 retained-test transfer) or the classical He–Schramm countable case are welcome.

Selected references

• OpenAI, Koebe's Circle-Domain Conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Koebes-Circle-Domain-Conjecture-September-23-2026/paper.pdf
• P. Koebe, Über die Uniformisierung beliebiger analytischer Kurven (Dritte Mitteilung), Nachr. Ges. Wiss. Göttingen, 1908.
• P. Koebe, Abhandlungen zur Theorie der konformen Abbildung VI, Math. Z., 1920. https://doi.org/10.1007/BF01199400
• Z.-X. He, O. Schramm, Fixed points, Koebe uniformization and circle packings, Ann. of Math., 1993. https://doi.org/10.2307/2946541
• O. Schramm, Transboundary extremal length, J. Analyse Math., 1995. https://doi.org/10.1007/BF02788827
• K. Rajala, Uniformization of planar domains by exhaustion, Amer. J. Math., 2025. https://doi.org/10.1353/ajm.2025.a966291
• D. Ntalampekos, K. Rajala, Exhaustions of circle domains, IMRN, 2025. https://doi.org/10.1093/imrn/rnaf296
• B. Esmayli, K. Rajala, Conformal uniformization of domains bounded by quasitripods, Duke Math. J., 2026. https://doi.org/10.1215/00127094-2025-0035
• C. Karafyllia, D. Ntalampekos, Uniformization of Gromov hyperbolic domains by circle domains, Duke Math. J., 2026. https://doi.org/10.1215/00127094-2025-0076
• D. Ntalampekos, Uniformization problems in the plane: A survey, preprint, 2026. https://arxiv.org/abs/2603.15098

Motivation

A circle domain is a domain in the Riemann sphere whose complementary components are round disks or points. Koebe asked in 1908 whether every domain is conformally equivalent to a circle domain (existence). A second question is rigidity: when is that circle-domain model unique up to Möbius transformations? For finitely and countably connected domains the model is unique, but for domains with uncountably many boundary components uniqueness can fail, and the boundary geometry decides. He and Schramm conjectured that a circle domain is rigid exactly when its boundary is conformally removable. Rigidity is what makes the circle-domain model canonical, and it connects conformal geometry with removability questions for quasiconformal and Sobolev maps.

Timeline

• 1993. He and Schramm prove uniformization and rigidity for countably connected circle domains (doi:10.2307/2946541).
• 1994. He and Schramm prove rigidity when the boundary has $\sigma$-finite linear measure, and conjecture that rigidity is equivalent to conformal removability of the boundary (doi:10.1007/BF01231761).
• 2000. Jones and Smirnov relate removability for continuous Sobolev functions to quasiconformal removability (doi:10.1007/BF02384320).
• 2016. Younsi proves that conformal rigidity is equivalent to quasiconformal rigidity and studies the removability formulations (doi:10.1016/j.aim.2016.08.039).
• 2020. Ntalampekos and Younsi prove rigidity under square integrability of the quasihyperbolic distance, covering Hölder and John circle domains (doi:10.1007/s00222-019-00921-1).
• 2023–2024. Ntalampekos proves rigidity when point components are countably negligible for extremal distance (CNED) and continuous Sobolev extension across closed CNED sets (doi:10.1090/tran/8923, doi:10.1007/s00029-024-00951-5).
• 2025. Rajala constructs a rigid circle domain with non-removable boundary, so rigidity does not imply removability (doi:10.1112/plms.70081).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the remaining implication: removability implies rigidity.

Setting

The Riemann sphere $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$ has local coordinates $z$ and $1/z$. A map is conformal at $p$ if it is continuous there and complex differentiable with nonzero derivative in these coordinates; a conformal equivalence $f:\Omega\to\Omega'$ is a bijection, conformal on $\Omega$, with conformal inverse. A Möbius transformation is $z\mapsto(az+b)/(cz+d)$ with $ad-bc\neq0$. A closed round disk is the Möbius image of the closed unit disk. A circle domain is a nonempty connected open set whose complementary components are closed round disks or points.

A compact $E\subset\widehat{\mathbb C}$ is conformally removable if every orientation-preserving homeomorphism of $\widehat{\mathbb C}$ that is conformal on $\widehat{\mathbb C}\setminus E$ is Möbius. A circle domain $\Omega$ is conformally rigid if every conformal equivalence from $\Omega$ onto another circle domain is the restriction of a Möbius transformation.

Formalization targets

Goal: Theorem 1.1

$$\Omega,\Omega'\ \text{circle domains},\ \ \partial\Omega\ \text{conformally removable},\ \ f:\Omega\to\Omega'\ \text{conformal equivalence}\ \Longrightarrow\ \exists M\ \text{Möbius}:\ f=M|_\Omega.$$

Lean: OAI.Problem047.removability_implies_rigidity, open on the platform. The complement may have any cardinality, and no boundary extension of $f$ is assumed.

Significance

Together with Rajala's counterexample to the converse, the theorem would settle the He–Schramm rigidity conjecture: removability is sufficient but not necessary. It subsumes the earlier sufficient conditions ($\sigma$-finite length, Hölder/John domains, CNED point sets) whenever those boundaries are removable. The intermediate Theorem 5.1, a continuous Sobolev extension theorem across compact totally disconnected conformally removable sets, is of independent interest. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Removability is a statement about homeomorphisms of the whole sphere, while rigidity starts from a map defined only on the domain. The obvious route, extending $f$ to a homeomorphism of the sphere and then invoking removability, fails: a point component of the complement of $\Omega$ may correspond to a disk component of $\Omega'$ and vice versa, so the coordinates of $f$ need not extend continuously, and nothing a priori controls boundary behaviour at uncountably many point components whose union can have positive area.

Formalization scope

• Sphere := OnePoint ℂ, Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it; conformality uses the charts $z$ and $1/z$ with HasDerivAt and a nonzero derivative.
• IsCircleDomain: open, IsConnected, and every connectedComponentIn of the complement is a singleton or a Möbius image of the closed unit disk.
• IsConformallyRemovable E: IsCompact E and every homeomorphism h : Sphere ≃ₜ Sphere that is homotopic to the identity (orientation preserving) and conformal on Eᶜ equals some Möbius map everywhere.
• The boundary is frontier U; the conclusion is ∃ M, ∀ p ∈ U, f p = M • p.
• The shared definitions are those of the Koebe circle-domain mission of the same family.

A complete development needs the theory of conformal maps on the sphere, Sobolev functions and Dirichlet energy in the plane, the measurable Riemann mapping theorem (used for the conductivity deformation), and component correspondence. Contributions formalizing Theorem 5.1 (continuous Sobolev extension), Proposition 6.2 (common point traces), or the He–Schramm countable case are welcome.

Selected references

• OpenAI, Removable Boundaries and Rigidity of Circle Domains, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026/paper.pdf
• Z.-X. He, O. Schramm, Fixed points, Koebe uniformization and circle packings, Ann. of Math., 1993. https://doi.org/10.2307/2946541
• Z.-X. He, O. Schramm, Rigidity of circle domains whose boundary has σ-finite linear measure, Invent. Math., 1994. https://doi.org/10.1007/BF01231761
• M. Younsi, Removability, rigidity of circle domains and Koebe's conjecture, Adv. Math., 2016. https://doi.org/10.1016/j.aim.2016.08.039
• D. Ntalampekos, M. Younsi, Rigidity theorems for circle domains, Invent. Math., 2020. https://doi.org/10.1007/s00222-019-00921-1
• D. Ntalampekos, Rigidity and continuous extension for conformal maps of circle domains, Trans. Amer. Math. Soc., 2023. https://doi.org/10.1090/tran/8923
• D. Ntalampekos, CNED sets: countably negligible for extremal distances, Selecta Math., 2024. https://doi.org/10.1007/s00029-024-00951-5
• P. W. Jones, S. K. Smirnov, Removability theorems for Sobolev functions and quasiconformal maps, Ark. Mat., 2000. https://doi.org/10.1007/BF02384320
• K. Rajala, Rigid circle domains with non-removable boundaries, Proc. Lond. Math. Soc., 2025. https://doi.org/10.1112/plms.70081
• OpenAI, Koebe's Circle-Domain Conjecture, preprint, September 23, 2026.

Motivation: which bounded domains cover compact spaces?

A bounded symmetric domain is a bounded connected open set in $\mathbb C^m$ with, at every point, a holomorphic involution having that point as an isolated fixed point. Examples are the ball, the polydisc and the Siegel upper half-spaces in their bounded realizations. They are the universal covers of compact locally symmetric varieties, such as compact quotients of the ball, and play a central role in algebraic geometry and number theory. A classical theme in several complex variables is that a bounded domain with a large automorphism group must be very special: Wong and Rosay showed that an automorphism orbit accumulating at a strongly pseudoconvex boundary point forces the ball, and Frankel showed that convex domains with compact quotients are symmetric.

Kollár and Pardon, studying algebraic varieties whose universal cover is semialgebraic, asked the following bounded-domain question: if a bounded semialgebraic open subset of a complex affine variety admits a properly discontinuous cocompact group of biholomorphisms, must it be a bounded symmetric domain? Semialgebraicity is a finiteness condition on the shape of the domain. It does not make the boundary smooth or convex, and it imposes nothing on the group.

Timeline

• 1970 — Vey proves that a divisible generalized Siegel domain is symmetric (Ann. Sci. ÉNS 3).
• 1977 — Wong characterizes the ball by its automorphism group among strongly pseudoconvex domains (Invent. Math. 41).
• 1979 — Rosay localizes Wong's theorem to a single $C^2$ strongly pseudoconvex boundary point (Ann. Inst. Fourier 29).
• 1989 — Frankel proves that a convex hyperbolic domain with compact quotient is a bounded symmetric domain, including non-free actions (Acta Math. 163).
• 2012 — Kollár and Pardon pose the bounded semialgebraic domain question (arXiv v2, Question 25) in Algebraic varieties with semialgebraic universal cover (J. Topol. 5; arXiv:1104.2309v2).
• 2021 — Zimmer shows that a $C^{1,1}$-bounded domain covering a compact manifold is a ball (Indiana Univ. Math. J. 70).
• 2026 — An OpenAI preprint, Symmetry of semialgebraic bounded domains with compact quotient (OpenAI Math Release, September 24, 2026), claims an affirmative answer to the Kollár–Pardon question. It has not been peer reviewed, and its proof is not formally verified.

Setting

An affine variety is a reduced complex algebraic set $V\subset\mathbb C^n$, the common zero locus of a set of polynomials. A subset of $\mathbb C^n$ is semialgebraic if it is a finite Boolean combination of sets $\{p=0\}$ and $\{p>0\}$, with $p$ a real polynomial in the real and imaginary parts of the coordinates. Let $U\subseteq V$ be open in $V$, connected, semialgebraic and bounded. A map on $U$ is holomorphic if near each point it is the restriction of a holomorphic map on an open subset of $\mathbb C^n$; a biholomorphism is a homeomorphism that is holomorphic in both directions. A group $\Gamma$ acts properly discontinuously if the action is proper for the discrete topology on $\Gamma$ (finite stabilizers are allowed), and the action is cocompact if $U/\Gamma$ is compact. $U$ is smooth if each point has a neighbourhood in $U$ biholomorphic to an open subset of some $\mathbb C^m$.

Formalization targets

Goal: semialgebraic bounded domains with compact quotient are symmetric (Theorem 1.1)

Let $U$ be a nonempty connected semialgebraic bounded open subset of a complex affine variety $V\subset\mathbb C^n$, and let a group $\Gamma$ act on $U$ by biholomorphisms, properly discontinuously and with $U/\Gamma$ compact. Then

$$U\ \text{is smooth, and}\quad U\cong D\ \text{biholomorphically for some bounded symmetric domain } D\subset\mathbb C^m .$$

The goal statement is published on the platform with status Open.

Significance

The result itself. The theorem answers the Kollár–Pardon question affirmatively. The ambient variety may be singular and nonnormal, the quotient may have finite quotient singularities, and no convexity, boundary regularity or homogeneity is assumed. It shows that semialgebraicity of a single affine realization forces the classical picture: a compact quotient of a semialgebraic bounded domain is a compact quotient of a bounded symmetric domain. This complements the universal-cover classification of the companion preprint on semialgebraic universal covers of normal projective varieties.

Formalizing it. The statement only uses polynomials, real-analytic Boolean combinations, holomorphic maps on subsets of $\mathbb C^n$ and group actions, all available in Mathlib. The proof, however, draws on Nash cell decompositions, analytic discs, scaling limits of automorphisms and Vey's theorem on divisible Siegel domains, none of which is formalized. A formal development would provide reusable semialgebraic geometry and several-complex-variables infrastructure.

Difficulty

The classical rigidity arguments (Wong–Rosay, Frankel, Zimmer) need a smooth strongly pseudoconvex or convex boundary point at which rescaled automorphisms converge to a model domain. A semialgebraic boundary can have corners with several complex-normal directions, and the normal fibres can shrink at rates that depend on tangential parameters, so the naive rescaling limit can collapse to a degenerate set. Moreover $U$ is not known to be a manifold at the start, so smoothness must be proved from the group action before any differential geometry is available. The heart of the proof is a noncollapse estimate that yields a Siegel-type quadratic model $\{\operatorname{Im}w-H(z,z)\in C\}$ to which Vey's theorem applies.

Formalization scope

• $V$ is IsAffineAlgebraic, the zero set of a set of complex polynomials in Fin n → ℂ; $U\subseteq V$ is open in the subspace topology of $V$, IsConnected (hence nonempty), bounded, and semialgebraic through an inductive predicate on real polynomials in $(\operatorname{Re}z,\operatorname{Im}z)$, closed under complement and union.
• $\Gamma$ is an arbitrary group with the discrete topology acting on the subtype $U$, with ProperSMul and a compact orbit space. Each $\gamma$ acts holomorphically in the sense of local ambient analytic extension; since $\gamma^{-1}$ also acts, the elements act by biholomorphisms. A non-faithful action is allowed and is harmless, since properness forces finite stabilizers.
• IsSmooth U asks for local biholomorphisms of neighbourhoods in $U$ onto open subsets of some $\mathbb C^m$. IsBoundedSymmetricDomain D asks that $D$ be open, connected and bounded, and have at each point an involutive biholomorphism fixing it with that point isolated among its fixed points.
• The zero-dimensional case (a point) is included and is trivial, matching the source convention.
• Needed infrastructure: semialgebraic cell decomposition and selection, Montel-type compactness on singular analytic sets, analytic discs, Kobayashi/Carathéodory-type distance estimates and the structure theory of Siegel domains. Each would be reusable.

Selected references

• J. Vey, Sur la division des domaines de Siegel, Ann. Sci. École Norm. Sup. (4) 3 (1970), 479–506. https://www.numdam.org/article/ASENS_1970_4_3_4_479_0.pdf
• B. Wong, Characterization of the unit ball in $\mathbb C^n$ by its automorphism group, Invent. Math. 41 (1977), 253–257. https://doi.org/10.1007/BF01403050
• J.-P. Rosay, Sur une caractérisation de la boule parmi les domaines de $\mathbb C^n$ par son groupe d'automorphismes, Ann. Inst. Fourier 29 (1979), 91–97. https://doi.org/10.5802/aif.768
• S. Frankel, Complex geometry of convex domains that cover varieties, Acta Math. 163 (1989), 109–149. https://doi.org/10.1007/BF02392734
• J. Kollár and J. Pardon, Algebraic varieties with semialgebraic universal cover, J. Topol. 5 (2012), 199–212. https://doi.org/10.1112/jtopol/jts001
• A. Zimmer, Smoothly bounded domains covering compact manifolds, Indiana Univ. Math. J. 70 (2021), 2653–2676. https://arxiv.org/abs/1910.05288v2
• M. Coste, Real algebraic sets, lecture notes, 2005. https://indico.ictp.it/event/a04204/session/10/contribution/7/material/0/0.pdf
• OpenAI, Symmetry of semialgebraic bounded domains with compact quotient, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symmetry-of-semialgebraic-bounded-domains-with-compact-quotient-September-24-2026/paper.pdf

Motivation: Nagata's conjecture beyond the plane

Seshadri constants measure the local positivity of a line bundle at a point or a configuration of points: how much of an ample class survives after blowing up the points and subtracting equal multiples of the exceptional curves. For $r$ points on a surface with ample $L$, a dimension count gives the universal upper bound $\sqrt{L^2/r}$. Nagata's 1959 conjecture, which came out of his counterexample to Hilbert's fourteenth problem, says that this bound is attained at $r\ge10$ very general points of the projective plane. On an arbitrary polarized surface, the qualitative Nagata–Biran(–Szemberg) conjecture predicts that the bound is attained at $r$ very general points for every sufficiently large $r$. On the symplectic side, the conjecture corresponds to packing stability: large numbers of equal balls fill a four-manifold.

Timeline

• 1959 — Nagata formulates his plane conjecture and proves the strict multiplicity inequality when $r\ge16$ is a perfect square (Amer. J. Math. 81).
• 1999 — Biran proves symplectic packing stability for rational symplectic classes on closed four-manifolds (Invent. Math. 136).
• 2003 — Harbourne proves maximality for all sufficiently large $r$ with $rL^2$ a perfect square, and asymptotic lower bounds (J. reine angew. Math.).
• 2004 — Roé relates one-point and multipoint Seshadri constants (J. Algebra); Strycharz-Szemberg and Szemberg formulate a stronger prediction with an explicit threshold (Serdica Math. J. 30).
• 2009 — Roé and Ross prove a multipoint product inequality that propagates maximality (Geom. Dedicata).
• 2010 — Syzdek and Szemberg state the qualitative conjecture for arbitrary polarized surfaces (Math. Nachr. 283, Conjecture 4.3; arXiv:0709.2592).
• 2016 — Buse, Hind and Opshtein prove strong packing stability for all closed symplectic four-manifolds (Trans. AMS). Symplectic stability alone does not fix the complex structure needed for the algebraic statement (Eckl 2017, Differential Geom. Appl.).
• 2026 — An OpenAI preprint, Maximal Seshadri constants on arbitrary polarized surfaces (OpenAI Math Release, September 23, 2026), claims the qualitative conjecture for every smooth complex projective surface and every ample line bundle. It has not been peer reviewed, and its proof is not formally verified.

Setting

Let $S$ be a smooth integral complex projective surface and $L$ an ample line bundle, with self-intersection $H=L^2$. For a tuple $\mathbf p=(p_1,\dots,p_r)$ of distinct points, the multipoint Seshadri constant is

$$\varepsilon(S,L;\mathbf p)=\inf_C\frac{L\cdot C}{\sum_{i=1}^r\operatorname{mult}_{p_i}C},$$

the infimum over integral curves $C$ through at least one $p_i$. If $\pi:Y\to S$ is the blow-up at $\mathbf p$ with exceptional curves $E_1,\dots,E_r$, then $\varepsilon$ is the largest $\lambda\ge0$ such that $\pi^*L-\lambda\sum E_i$ is nef (nonnegative on every integral curve), and always $\varepsilon\le\sqrt{H/r}$. Let $U_r\subset S^r$ be the set of tuples of distinct points. A property holds at very general tuples if it fails only on a countable union of proper Zariski-closed subsets of $U_r$.

Formalization targets

Goal: eventual maximality of multipoint Seshadri constants (Theorem 1.1)

For every such $(S,L)$ there is $r_0\ge1$ such that for each $r\ge r_0$ there is a countable union $Z_r$ of proper Zariski-closed subsets of $U_r$, with $U_r\setminus Z_r\neq\varnothing$, such that for every $\mathbf p\in U_r\setminus Z_r$

$$\pi^*L-\sqrt{\tfrac{L^2}{r}}\sum_{i=1}^rE_i\ \text{ is nef on the blow-up at }\mathbf p, \qquad\text{and}\qquad \varepsilon(S,L;\mathbf p)=\sqrt{\tfrac{L^2}{r}} .$$

The threshold $r_0$ may depend on $(S,L)$ and is not explicit. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.1 settles the qualitative Nagata–Biran conjecture for all polarized complex surfaces, with no assumption that $rL^2$ is a square or that a plane constant is maximal (the hypotheses needed by Harbourne, Roé and Roé–Ross). Because the conclusion is nefness of the square-zero boundary class, it rules out every curve whose degree-to-multiplicity ratio is below $\sqrt{L^2/r}$, including curves with unequal multiplicities. Via Eckl's Kähler packing correspondence, it gives the algebraic counterpart of packing stability. The sharp plane case ($r\ge10$ in $\mathbb P^2$) is a separate companion result.

Formalizing it. The statement is built from scheme-theoretic foundations: projective surfaces, line bundles, sheaf cohomology, blow-ups by universal property, intersection numbers through Euler characteristics. A complete proof would be among the first machine-checked results about the birational geometry of surfaces. Much of the required infrastructure, such as Riemann–Roch on surfaces, finite-dimensionality of coherent cohomology and the existence of blow-ups, is not yet in Mathlib.

Difficulty

The upper bound $\varepsilon\le\sqrt{H/r}$ is an elementary jet count. Equality requires showing that no curve on the surface has too large multiplicity at the chosen points, for all multiplicity orders simultaneously. Degenerating the points to a special configuration, the usual approach in the plane, fails because the threshold in $r$ must be uniform in the jet order: the asymptotic interpolation theorems (Alexander–Hirschowitz) give thresholds depending on a fixed multiplicity bound. Arbitrary surfaces also lack the toric coordinates available on $\mathbb P^2$. The source transfers the problem to finite interpolation on an algebraic torus through a nodal divisor in $|dL|$.

Formalization scope

• Surface: an integral scheme, smooth of relative dimension $2$ over $\operatorname{Spec}\mathbb C$, with a closed immersion into some $\mathbb P^N_{\mathbb C}$ compatible with the structure maps. LineBundle: a locally free sheaf of rank one. IsAmple: the nonvanishing loci of sections of positive powers that are affine form a neighbourhood basis.
• Cohomology is Ext^n(𝒪, M) in the category of sheaves of modules, and dimensions are finrank ℂ. Then $L^2=\chi(2L)-2\chi(L)+\chi(\mathcal O)$ and $L\cdot C=\chi(L|_C)-\chi(\mathcal O_C)$, by Riemann–Roch. If cohomology were infinite-dimensional, finrank would return $0$; finite-dimensionality for projective schemes is part of what a solver must prove.
• Points are $\mathbb C$-points, the configuration space carries the Zariski topology induced from $S^r$, and very general sets are indexed by $\mathbb N$ (IsClosed, ≠ univ, with a point outside all of them).
• The multiplicity is the order of the local equation of $C$ in the local ring at $p$. The Seshadri constant is the real sInf over integral curves with positive total multiplicity.
• Nefness is expressed through a blow-up PointBlowup, characterized by its universal property, and the exceptional ideal sheaves $\mathcal O(-E_i)$. The inequality is $\pi^*L\cdot C+\sqrt{H/r}\sum_i \deg(\mathcal O(-E_i)|_C)\ge0$ for every integral curve $C$ on the blow-up.
• Needed infrastructure: coherent cohomology of projective schemes, Riemann–Roch on curves and surfaces, blow-ups of points, jets and principal parts. Contributions building any of these layers are welcome and reusable.

Selected references

• M. Nagata, On the 14-th problem of Hilbert, Amer. J. Math. 81 (1959), 766–772. https://doi.org/10.2307/2372927
• P. Biran, A stability property of symplectic packing, Invent. Math. 136 (1999), 123–155. https://doi.org/10.1007/s002220050306
• B. Harbourne, Seshadri constants and very ample divisors on algebraic surfaces, J. reine angew. Math. (2003). https://doi.org/10.1515/crll.2003.044
• J. Roé, A relation between one-point and multi-point Seshadri constants, J. Algebra (2004). https://doi.org/10.1016/j.jalgebra.2003.10.009
• B. Strycharz-Szemberg and T. Szemberg, Remarks on the Nagata conjecture, Serdica Math. J. 30 (2004), 405–430. https://www.math.bas.bg/serdica/2004/2004-405-430.pdf
• J. Roé and J. Ross, An inequality between multipoint Seshadri constants, Geom. Dedicata (2009). https://doi.org/10.1007/s10711-008-9315-4
• W. Syzdek and T. Szemberg, Seshadri fibrations of algebraic surfaces, Math. Nachr. 283 (2010), 902–908. https://arxiv.org/abs/0709.2592v1
• O. Buse, R. Hind and E. Opshtein, Packing stability for symplectic 4-manifolds, Trans. Amer. Math. Soc. (2016). https://doi.org/10.1090/tran/6802
• T. Eckl, Kähler packings and Seshadri constants on projective complex surfaces, Differential Geom. Appl. (2017). https://doi.org/10.1016/j.difgeo.2017.03.007
• OpenAI, Maximal Seshadri constants on arbitrary polarized surfaces, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Maximal-Seshadri-Constants-on-Arbitrary-Polarized-Surfaces-September-23-2026/main.pdf

Motivation

Euler's totient $\varphi(n)$ counts the integers in $\{1,\dots,n\}$ coprime to $n$. Many integers share a totient, and most integers are not totients at all, so counting the distinct values of $\varphi$ is much harder than counting integers with a given factorization. Let

$$\mathcal V=\{\varphi(n):n\ge1\},\qquad V(x)=\#\{v\in\mathcal V: v\le x\}.$$

The size of $V(x)$ was studied by Pillai, Erdős, Hall, Pomerance, Maier and Ford over most of the twentieth century; Ford's 1998 estimate determines $V(x)$ up to a bounded multiplicative factor but leaves open whether $V(x)$ has an asymptotic equivalent, and Erdős and Hall's question whether $V(cx)/V(x)\to c$.

This mission asks for a formal proof of the explicit asymptotic formula and the Erdős–Hall regular-variation property, as stated in an OpenAI preprint dated September 25, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1929 — Pillai proves that totients have density zero (Bull. AMS 35, 1929).
• 1935 — Erdős shows $V(x)\ll_\varepsilon x/(\log x)^{1-\varepsilon}$ via the normal number of prime factors of $p-1$ (Q. J. Math. 1935); later lower bounds use semiprimes (1945).
• 1976 — Erdős and Hall obtain a lower factor $\exp\{a(\log_3x)^2\}$ and ask whether $V(cx)/V(x)\to c$ (Mathematika 1976).
• 1986–1988 — Pomerance brings the upper bound to the same scale (Acta Arith. 1986); Maier and Pomerance determine the leading constant $C_0=0.8178\ldots$ in $V(x)=\frac{x}{\log x}\exp\{(C_0+o(1))(\log_3x)^2\}$ (Acta Arith. 1988).
• 1998 — Ford determines $V(x)$ up to a bounded factor and proves $V(cx)-V(x)\asymp_cV(x)$ (Ramanujan J. 1998).
• September 2026 — The OpenAI preprint claims an explicit asymptotic equivalent and $V(cx)/V(x)\to c$ (Theorem 2.1, p. 4).

Setting

Logarithms are natural and $\log_j$ is the $j$-fold iterate. For $j\ge1$ let $a_j=(j+1)\log(j+1)-j\log j-1$, let $\rho\in(0,1)$ be the unique root of $\sum_{j\ge1}a_j\rho^j=1$, and set

$$\lambda=\log(1/\rho),\qquad \gamma=\Bigl(\sum_{j\ge1}ja_j\rho^j\Bigr)^{-1},\qquad g_0=1,\ \ g_j=\sum_{d=1}^ja_dg_{j-d}.$$

For large $x$ put $B=\log_2x$, $m=\lfloor(\log B-\log_2B)/\lambda\rfloor$, the phase $\theta=(\log B-\log_2B)/\lambda-m\in[0,1)$, and $G_m=B^m/(m!\prod_{i\le m}g_i)$; the factor $\frac{x}{\log x}G_m$ is Ford's counting scale.

For each $H$ the preprint defines an explicit arithmetic coefficient $A_H(f;s)$, $s\in[0,1)$, from a finite set of "tail witnesses" (tuples of primes $Q_h$, $P\le h<H$, and a cofactor $a$, subject to explicit size and recurrence constraints, $P=\lfloor\log\log H\rfloor$) by inclusion–exclusion over witnesses with a common totient $d$, weighted by $f(\ell(d)/d)/d$ (formula (2.8), p. 5). Here $\ell(v)=\min\{n\ge1:\varphi(n)=v\}$ is the least preimage, and $A(f;s)=\lim_{H\to\infty}A_H(f;s)$ when the limit exists. The coefficient is defined without reference to $V$.

Formalization targets

Milestone: nonnegativity of the approximants (Theorem 2.1, p. 4)

$A_H(1;s)\ge0$ for $s\in[0,1)$.

Goal: Theorem 2.1 (p. 4)

$A_H(1;\cdot)\to A(1;\cdot)$ uniformly on $[0,1)$, with $0<\inf_sA(1;s)\le\sup_sA(1;s)<\infty$, and

$$V(x)\sim\frac{x}{\log x}\,G_m\,A(1;\theta),\qquad \frac{V(cx)}{V(x)}\longrightarrow c\quad(c>0\ \text{fixed}).$$

Further milestones: least preimages (Theorem 2.2, p. 6)

For $k\ge1$ let $N_k(x)=\#\{v\in\mathcal V:v\le x,\ kx<\ell(v)\le(k+1)x\}$ and $f_k(r)=\min\{1,\tfrac{k+1}r\}-\min\{1,\tfrac kr\}$. Then $A_H(f_k;\cdot)$ converges uniformly and $N_k(x)=\frac{x}{\log x}G_m(A(f_k;\theta)+o(1))$; if some totient $d$ has $\ell(d)>kd$ then $\inf_sA(f_k;s)>0$ and $N_k(x)\asymp V(x)$, and otherwise $N_k\equiv0$ and $A(f_k;\cdot)\equiv0$. The positive alternative holds for $k=1,2$.

Significance

The result itself. The formula replaces Ford's bounded uncertainty by an explicit function of the phase $\theta$, built from finite arithmetic data, and answers the Erdős–Hall question: $V$ is regularly varying of index $1$. Theorem 2.2 answers, in weighted form, Erdős's question on how least preimages are distributed in intervals $(kx,(k+1)x]$, reducing it to the existence of a "seed" totient with $\ell(d)>kd$. Whether such seeds exist for every $k$ (equivalently, whether $\ell(d)/d$ is unbounded) is not settled by the preprint.

Formalizing it. This is analytic number theory at full strength: Ford's structure theorems for totient preimages, sieve bounds for two or three linear forms in shifted primes, simplex volume computations and an inclusion–exclusion limit. Mathlib has the totient and the prime number theorem in some forms but not these sieve and distribution results. The definitions in this mission (the renewal root $\rho$, the witnesses, $A_H$) are explicit and can be checked independently of any proof.

Difficulty

Counting integers $n$ with a typical factorization is a volume computation, but $V(x)$ counts values, and different $n$ can have the same totient. The preprint must show that, outside a negligible set, distinct long prime prefixes give distinct values (Proposition 5.1, p. 22, and Proposition 5.3, p. 27), which needs a uniform comparison estimate for products of shifted primes (Proposition 4.2, p. 17), while short discrete tails that may collide are kept exactly and handled by inclusion–exclusion (Lemma 6.4, p. 30). The limits are taken in a specific order ($x\to\infty$ with $H$ fixed, then $H\to\infty$), and no continuity of $s\mapsto A(1;s)$ is available, so all errors must be uniform in the phase.

Formalization scope

• IsTotient v means $v=\varphi(n)$ for some $n\ge1$; V x counts totients in $\{1,\dots,\lfloor x\rfloor\}$; ell v is Nat.find of the least preimage (junk value $0$ for non-totients, never used on them).
• rho is the sInf of roots in $(0,1)$ of $\sum_{j\ge0}a_{j+1}z^{j+1}=1$; the root is unique, so this is the source's $\rho$.
• AH H f s is formula (2.8) with finsum over totients $d$ and over nonempty finite sets $T$ of witnesses with $\varphi(w)=d$; the witness set is finite for each $H$, so the finsums are genuine finite sums. A f s is limUnder atTop; the goal asserts uniform convergence, so the junk value is never used.
• mainTerm x = x / log x * G x (m x) * A 1 (theta x); asymptotic equivalence is Tendsto (V x / mainTerm x) atTop (𝓝 1).
• The milestone coefficient_nonnegative is stated for every $H$, while the source states it for sufficiently large $H$; for small $H$ the witness set is empty or the inclusion–exclusion is still a probability, so this is a harmless strengthening.
• companion_zero_case restates alternative (ii) of Theorem 2.2 in a separate definition file (TotientCompanionZero) with identical definitions.

Selected references

• OpenAI, An asymptotic formula for the number of totients, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/An-asymptotic-formula-for-the-number-of-totients-September-25-2026.pdf
• S. S. Pillai, On some functions connected with φ(n), Bull. Amer. Math. Soc. 35 (1929), 832–836. https://www.ams.org/journals/bull/1929-35-06/S0002-9904-1929-04799-2/S0002-9904-1929-04799-2.pdf
• P. Erdős, On the normal number of prime factors of p−1 and some related problems concerning Euler's φ-function, Q. J. Math. 6 (1935). https://doi.org/10.1093/qmath/os-6.1.205
• P. Erdős, R. R. Hall, Distinct values of Euler's φ-function, Mathematika 23 (1976). https://doi.org/10.1112/S0025579300006100
• C. Pomerance, On the distribution of the values of Euler's function, Acta Arith. 47 (1986). https://doi.org/10.4064/aa-47-1-63-70
• H. Maier, C. Pomerance, On the number of distinct values of Euler's φ-function, Acta Arith. 49 (1988). https://doi.org/10.4064/aa-49-3-263-275
• K. Ford, The distribution of totients, Ramanujan J. 2 (1998), 67–151; revised arXiv:1104.3264. https://arxiv.org/abs/1104.3264v2

Motivation

For a positive integer $n$, Jacobsthal's function $j(n)$ is the least $m$ such that every run of $m$ consecutive integers contains an integer coprime to $n$. Equivalently, $j(n)-1$ is the longest interval that can be covered by choosing one residue class modulo each prime divisor of $n$ (the classes $0\bmod p$ shifted by the interval's start). Its maximum over integers with at most $k$ prime divisors,

$$h(k)=\max\{j(n):\ \omega(n)\le k\},$$

governs how long a stretch can be sieved out by $k$ primes. It is linked to gaps between consecutive primes (long covered intervals produce large prime gaps, as in the Erdős–Rankin and Ford–Green–Konyagin–Maynard–Tao constructions) and to the limits of the linear sieve. Jacobsthal asked, and Erdős recorded, whether $h(k)\ll k^2$.

Background

• 1960. Jacobsthal begins a series of papers on this function.
• 1962. Erdős records Jacobsthal's question $h(k)\ll k^2$ and notes Brun's bound $h(k)\ll k^{C_0}$ (doi:10.7146/math.scand.a-10523).
• 1971. Iwaniec's error-term estimate for the linear sieve gives order $k^2\log^2k$ for the first $k$ primes (doi:10.4064/aa-19-1-1-30).
• 1977. Vaughan proves the uniform bound $j(n)\ll\omega(n)^2\log(2\omega(n))$ and explains the exponent 2 by the linear sieve's square-root restriction (doi:10.1017/S0013091500026560).
• 1978. Iwaniec proves $h(k)\ll k^2\log^2k$ for arbitrary prime sets (doi:10.1515/dema-1978-0121).
• 2012. Hajdu and Saradha disprove Jacobsthal's primorial-extremality conjecture: $j(P_{24})=234<236=h(24)$ (doi:10.1090/S0025-5718-2012-02581-6).
• 2015, 2019. Costello–Watts and Ziller compute bounds and exact values for small $k$ (doi:10.1090/S0025-5718-2014-02896-2).
• 2018. Ford, Green, Konyagin, Maynard and Tao give the lower bound $j(P_k)\gg k(\log k)^2\frac{\log\log\log k}{\log\log k}$ (doi:10.1090/jams/876).

The source of this mission is an OpenAI preprint dated September 25, 2026.

Setting

• $\omega(n)$ is the number of distinct prime divisors of $n$, with $\omega(1)=0$.
• For $n\ge1$, $j(n)$ is the least $m\ge1$ such that for every integer $a$, one of $a,a+1,\dots,a+m-1$ is coprime to $n$ (note $\gcd(0,n)=n$).
• $h(k)=\sup\{j(n):n\ge1,\ \omega(n)\le k\}$ for $k\ge1$. All logarithms are natural.

Formalization targets

Milestone: quadratic bound (Jacobsthal's question)

$$\exists C>0\ \forall k\ge1:\quad h(k)\le C\,k^2.$$

Goal: Theorem 1.1

$$\exists C>0\ \forall k\ge1:\quad h(k)\le C\,\frac{k^2}{(\log\log(3k))^2}.$$

Both are stated in Lean as the existence, for each $k$, of a length $m$ satisfying IsJacobsthalBound k m with the displayed size bound. The goal OAI.Erdos970.Erdos970Final.erdos_970_iterated_log is open on the platform.

Significance

Theorem 1.1 answers Jacobsthal's question affirmatively, uniformly over all prime sets and interval positions, and removes the logarithmic losses in the bounds of Vaughan and Iwaniec, going slightly below the quadratic scale. It shows that the linear sieve can be pushed to its limiting parameter $s=2$, where the lower sieve function vanishes, by retaining a boundary contribution. The gap to the best lower bound (roughly $k(\log k)^2$) remains large; Vaughan suggested $j(n)\ll_\varepsilon\omega(n)^{1+\varepsilon}$.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The constant $C$ is not made explicit.

Difficulty

The linear sieve gives a lower bound for the number of uncovered integers only when the sieving range is below the square root of the interval length, which is exactly where the exponent 2 comes from; at the critical parameter the main term of the lower-bound sieve vanishes, so the standard argument yields nothing and a $\log^2k$ loss appears. One must keep the boundary term that the leading linear-sieve calculation discards, and then show that the actual prescribed residue classes do not deviate much from a reference calculation. Positivity of the reference calculation alone does not suffice: the comparison requires an inverse estimate for a witnessing edge of a decreasing-prime tree, variance bounds, and stopping-time counts for hard endpoints.

Formalization scope

• IsJacobsthalBound k m: for every n : ℕ with 0 < n and n.primeFactors.card ≤ k, and every a : ℤ, some i < m has (a + i).natAbs.Coprime n.
• JacobsthalQuadratic: ∃ C > 0, ∀ k > 0, ∃ m, IsJacobsthalBound k m ∧ m ≤ C k^2.
• JacobsthalIteratedLog: the same with bound C k^2 / (log (log (3k)))^2; for $k\ge1$ the denominator is positive.
• The two targets live in separate definition files that both define IsJacobsthalBound identically.

A complete development needs the fundamental lemma of the sieve, Buchstab-type functions of the linear sieve, prime number theorem estimates in short ranges and progressions, the additive large sieve, a lattice-point count on plane curves, and renewal-type arguments for a continuous path process. Contributions formalizing Theorem 1.2 (the quantitative covering estimate), Lemma 2.1 (fundamental lemma of the sieve), Proposition 6.3 (positive reference margin), Proposition 8.2 (inverse estimate for an edge) and Corollary 9.3 are welcome.

Selected references

• OpenAI, A quadratic bound for Jacobsthal's function, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf
• P. Erdős, On the integers relatively prime to n and on a number-theoretic function considered by Jacobsthal, Math. Scand., 1962. https://doi.org/10.7146/math.scand.a-10523
• R. C. Vaughan, On the order of magnitude of Jacobsthal's function, Proc. Edinburgh Math. Soc., 1977. https://doi.org/10.1017/S0013091500026560
• H. Iwaniec, On the problem of Jacobsthal, Demonstratio Math., 1978. https://doi.org/10.1515/dema-1978-0121
• H. Iwaniec, On the error term in the linear sieve, Acta Arith., 1971. https://doi.org/10.4064/aa-19-1-1-30
• L. Hajdu, N. Saradha, Disproof of a conjecture of Jacobsthal, Math. Comp., 2012. https://doi.org/10.1090/S0025-5718-2012-02581-6
• K. Ford, B. Green, S. Konyagin, J. Maynard, T. Tao, Long gaps between primes, J. Amer. Math. Soc., 2018. https://doi.org/10.1090/jams/876
• F. Costello, P. Watts, An upper bound on Jacobsthal's function, Math. Comp., 2015. https://doi.org/10.1090/S0025-5718-2014-02896-2
• J. Friedlander, H. Iwaniec, Opera de Cribro, AMS, 2010. https://doi.org/10.1090/coll/057

Motivation

Goldbach-type problems ask which sets are sumsets of primes. The inverse Goldbach problem, due to Ostmann (1956), reverses the question: can the set of primes itself, up to finitely many changes, be written as a sumset $A+B=\{a+b:a\in A,\ b\in B\}$ with both $A$ and $B$ having at least two elements? Ostmann conjectured that it cannot: the primes are asymptotically additively indecomposable. The problem is a clean test of how much additive structure the primes can carry, and it connects sieve theory (the primes avoid one residue class modulo each prime) with inverse questions for the large sieve.

Background

• 1954–1955. Hornfeck proves early restrictions on additive decompositions of the primes (doi:10.1007/BF01187376).
• 1956. Ostmann formulates the conjecture in his treatise on additive number theory (doi:10.1007/978-3-662-11030-0).
• 1964. Laffer and Mann show that a hypothetical decomposition must have two infinite summands (doi:10.2140/pjm.1964.14.547).
• 1988–1996. Pomerance, Sárközy and Stewart, and Hofmann and Wolke, obtain sieve restrictions on the summands (doi:10.2140/pjm.1988.133.363, doi:10.1007/BF01189097).
• 2001. Elsholtz combines the large and larger sieves to put both counting functions near the square-root scale and rules out decompositions into three nontrivial summands (doi:10.1112/S0025579300014406).
• 2014–2016. Green and Harper show that an inverse large-sieve conjecture would imply Ostmann's conjecture (arXiv:1311.6176); Elsholtz and Harper sharpen the binary counting bounds (doi:10.1090/S0002-9947-2014-06384-8); Shao proves a finite ternary obstruction (doi:10.1353/ajm.2016.0038).
• 2020–2026. Hanson, then Croot, Mao and Yip, and Croot, Mao, Pohoata and Yip prove partial inverse theorems for the large sieve and derive further necessary conditions on a hypothetical decomposition (doi:10.1017/S0305004118000518, arXiv:2510.08862, arXiv:2607.15311).

The source of this mission is an OpenAI preprint dated September 24, 2026.

Setting

Let $\mathbb N_0=\{0,1,2,\dots\}$ and let $P$ be the set of positive primes. For $A,B\subseteq\mathbb N_0$ the sumset is $A+B=\{a+b:a\in A,\ b\in B\}$. Two sets are asymptotically equal if their symmetric difference $X\triangle Y=(X\setminus Y)\cup(Y\setminus X)$ is finite. A decomposition is nontrivial if $|A|\ge2$ and $|B|\ge2$; the trivial decompositions $\{0\}+P$ are excluded.

Formalization targets

Goal: Theorem 1.1 (Ostmann's conjecture)

$$A,B\subseteq\mathbb N_0,\ |A|\ge2,\ |B|\ge2\ \Longrightarrow\ (A+B)\triangle P\ \text{is infinite}.$$

Milestone: Theorem 2.3 (two infinite summands)

$$\text{There are no infinite }A,B\subseteq\mathbb N_0\text{ with }(A+B)\triangle P\text{ finite}.$$

Theorem 2.3 is the core of the proof; Lemma 2.2 reduces Theorem 1.1 to it by a short sieve argument.

The goal OAI.Ostmann.inverseGoldbach is open on the platform.

Significance

Theorem 1.1 resolves Ostmann's conjecture. The conclusion controls both requirements of an eventual decomposition: if $|A|,|B|\ge2$ and $A+B$ contains every sufficiently large prime, then $A+B$ contains infinitely many composite numbers. The proof does not go through the general inverse large-sieve conjecture of Green and Harper; it uses the simultaneous residue restrictions together with coverage of every large prime directly.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The statement is elementary, so the formal target is short; the difficulty is entirely in the proof.

Difficulty

Counting alone cannot work: sieve bounds put $A(x)$ and $B(x)$ near $\sqrt x$, which is compatible with the lower bound $A(x)B(x)\gg x/\log x$ forced by covering the primes. The known necessary conditions (large intersections with quadratic images) fall short of the near-containment that Green and Harper's conditional route requires. The proof must turn the local information (modulo each prime $p$, the images of $A$ and $-B$ are disjoint) into a global contradiction: it rules out correlations with translated multiplicative characters of every order, compares a positive sumset statistic with its average over the primes, and handles residue indicators with no prescribed algebraic form via a finite-field comparison of binary trees. The paper runs to about 80 pages.

Formalization scope

• primes = {n : ℕ | Nat.Prime n}; sumset A B is Mathlib's pointwise A + B on Set ℕ.
• A.Nontrivial means $A$ has two distinct elements.
• InverseGoldbach asserts Set.Infinite (sumset A B ∆ primes); TwoInfiniteSummandsImpossible uses EventuallyPrimeSumset A B := ∃ N, ∀ n ≥ N, n ∈ A + B ↔ n.Prime, which is equivalent to a finite symmetric difference.
• OAI.Ostmann.main is the same statement as the goal without the definition file and is included as a reference item.

A complete development needs the additive large sieve (Montgomery–Vaughan), Gallagher's larger sieve, Mertens-type estimates, character sums over finite fields including the quadratic large sieve, prime number theorems in progressions with the exceptional character, and Fourier analysis on $\mathbb F_p$. Contributions formalizing Lemma 2.1 (fixed shifts), Lemma 2.2 (finite summands), Lemma 2.4 (square-root bounds), Proposition 3.1, Corollary 4.2 (mixed-character decorrelation), Proposition 5.1 and Lemma 6.1 (tree comparison) are welcome.

Selected references

• OpenAI, The additive indecomposability of the primes, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/the-additive-indecomposability-of-the-primes-September-24-2026/paper.pdf
• H.-H. Ostmann, Additive Zahlentheorie. Erster Teil, Springer, 1956. https://doi.org/10.1007/978-3-662-11030-0
• W. B. Laffer, H. B. Mann, Decomposition of sets of group elements, Pacific J. Math., 1964. https://doi.org/10.2140/pjm.1964.14.547
• C. Elsholtz, The inverse Goldbach problem, Mathematika, 2001. https://doi.org/10.1112/S0025579300014406
• B. Green, A. J. Harper, Inverse questions for the large sieve, Geom. Funct. Anal., 2014. https://doi.org/10.1007/s00039-014-0288-1
• C. Elsholtz, A. J. Harper, Additive decompositions of sets with restricted prime factors, Trans. Amer. Math. Soc., 2015. https://doi.org/10.1090/S0002-9947-2014-06384-8
• X. Shao, On an inverse ternary Goldbach problem, Amer. J. Math., 2016. https://doi.org/10.1353/ajm.2016.0038
• B. Hanson, Additive correlation and the inverse problem for the large sieve, Math. Proc. Cambridge Philos. Soc., 2020. https://doi.org/10.1017/S0305004118000518
• E. Croot, J. Mao, C. Pohoata, C. H. Yip, A sharp inverse theorem for the quadratic large sieve, preprint, 2026. https://arxiv.org/abs/2607.15311
• H. L. Montgomery, R. C. Vaughan, The large sieve, Mathematika, 1973. https://doi.org/10.1112/S0025579300004708

Motivation: largest prime factors of neighbouring integers

Let $P^+(n)$ be the largest prime factor of an integer $n\ge2$. The classical theory of smooth numbers (Dickman 1930, Ramaswami 1949, de Bruijn 1951) shows that $\log P^+(n)/\log n$ has a limiting distribution: the proportion of $n\le X$ with $P^+(n)\le X^a$ tends to $\rho(1/a)$, where $\rho$ is the Dickman function. Multiplicative structure of $n$ and of $n+1$ is expected to be independent, since consecutive integers share no prime factor, but proving independence of such "additive shifts" of multiplicative data is the core difficulty of the Chowla/Elliott circle of problems. Erdős and Pomerance (1978) asked whether $P^+(n)$ and $P^+(n+1)$ are asymptotically independent with Dickman marginals, and, as a consequence, whether $P^+(n)<P^+(n+1)$ holds for exactly half of all $n$ (a comparison question usually attributed to Erdős and Turán).

Timeline

• 1930–1951 — Dickman, Ramaswami and de Bruijn establish the one-variable law $\#\{n\le X: P^+(n)\le X^a\}/X\to\rho(1/a)$.
• 1978 — Erdős and Pomerance formulate the joint independence problem, prove that each ordering of $P^+(n),P^+(n+1)$ has lower natural density at least $0.0099$, and show that $P^+(n)/P^+(n+1)$ rarely lies in $(X^{-\delta},X^{\delta})$ (Aequationes Math. 17 (1978)).
• 2005 — de la Bretèche, Pomerance and Tenenbaum raise the lower density to $0.05544$ (and $0.05866$ via an observation of Fouvry).
• 2017–2018 — Wang obtains $0.1063$ and $0.1356$.
• 2018 — Teräväinen proves the joint Dickman law in logarithmic density, and logarithmic density $1/2$ for the ordering (Forum Math. Sigma 6 (2018)).
• 2019 — Tao and Teräväinen obtain the joint law for ordinary averages outside an exceptional set of scales of logarithmic density zero (Algebra Number Theory 13 (2019)).
• 2021 — Wang proves the ordinary joint law conditionally on the Elliott–Halberstam conjecture for friable integers (J. Number Theory 223).
• 2022 — Jiang, Lü and Wang prove averaged-over-shift versions (Adv. Math. 409).
• 2025–2026 — Lü and Wang reach lower density $0.2017$; Yang reaches $0.280$ (arXiv:2607.16032); Tao and Teräväinen give a quantitative joint law outside exceptional scales (arXiv:2512.01739).
• 2026 — An OpenAI preprint, The joint Dickman law for consecutive integers (OpenAI Math Release, September 24, 2026), claims the unconditional joint law in ordinary natural density at every scale. It has not been peer reviewed, and its proof is not formally verified.

Setting

For $n\ge2$, $P^+(n)$ is the largest prime dividing $n$. The Dickman function $\rho:[0,\infty)\to\mathbb R$ is the continuous function with

$$\rho(u)=1\ (0\le u\le1),\qquad u\rho'(u)=-\rho(u-1)\ (u>1),$$

equivalently $\rho(u)=1-\int_1^u \rho(t-1)\,\frac{dt}{t}$ for $u\ge1$. For a property $P$ of integers and real $X>0$, the natural density at scale $X$ is

$$\mathrm{realDensity}(P,X)=\frac1X\,\#\{2\le n\le X:\ P(n)\}.$$

Formalization targets

Goal: the joint Dickman law (Theorem 1.1)

For every fixed $a,b\in(0,1)$,

$$\lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n)\le n^a,\ P^+(n+1)\le n^b\}=\rho(1/a)\,\rho(1/b),$$

with $X$ running over all reals and ordinary, unweighted counting. The goal statement is published on the platform with status Open.

Milestones: equal ordering densities (Corollary 1.2)

$$\lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n)<P^+(n+1)\}=\tfrac12, \qquad \lim_{X\to\infty}\frac1X\#\{2\le n\le X:\ P^+(n+1)<P^+(n)\}=\tfrac12 .$$

Significance

The result itself. Theorem 1.1 says that, in natural density, $\log P^+(n)/\log n$ and $\log P^+(n+1)/\log n$ are independent with Dickman marginals. It settles the Erdős–Pomerance independence question positively, removes the logarithmic weighting of Teräväinen's theorem and the exceptional scales of Tao–Teräväinen, and implies the Erdős–Turán comparison: because the limiting marginal is continuous, the product law gives no mass to the diagonal, so each strict ordering has density $1/2$ (Corollary 1.2). Previous unconditional work only gave lower natural densities, never the existence of the density.

Formalizing it. The goal is a clean density statement about elementary objects, but its proof combines Matomäki–Radziwiłł short-interval estimates, sieve bounds, a divisor amplifier, graph comparison and cut-norm sampling. No part of this argument is machine-checked. Even the one-variable Dickman law (the marginal case) is not in Mathlib, and would be a reusable milestone in its own right.

Difficulty

Independence of $n$ and $n+1$ is a binary correlation problem for multiplicative data, of the same nature as the two-point Chowla conjecture. Tao's entropy-decrement and logarithmic-averaging method handles such correlations only with weight $1/n$, or at almost all scales; the step that fails for ordinary density is ruling out a positive correlation along a sparse sequence of scales. The indicator $\mathbf 1_{P^+(n)\le n^a}$ is also not multiplicative, so short-interval theorems for multiplicative functions do not apply to it directly.

Formalization scope

• Nat.maxPrimeFac n (largest element of the prime factor list, a faithful backport of the Mathlib definition) represents $P^+(n)$; its junk values at $0,1$ are irrelevant since counting starts at $n=2$.
• realDensity P X is #{n ∈ [2, ⌊X⌋] : P n} / X as a real number, and limits are Tendsto … atTop over real $X$, matching "the limit over all real $X$".
• The thresholds are $P^+(n)\le n^a$ with real powers (n:ℝ)^a, and the hypotheses $0<a<1$, $0<b<1$ are explicit.
• $\rho$ is constructed by iterating the delay integral equation stepApprox and evaluating the $\lceil u\rceil$-th iterate at $u$; this agrees with the Dickman function on $[0,\infty)$, which is the only range used ($1/a,1/b>1$). A wrong $\rho$ would make the goal false, so this definition is part of what solvers should check.
• Needed infrastructure: the one-variable Dickman law, Selberg–Delange and sieve estimates, short-interval mean values of multiplicative functions, and profinite/Haar-measure compactness arguments. Contributions formalizing the smooth-number marginal or the deduction of Corollary 1.2 from Theorem 1.1 are welcome.

Selected references

• K. Dickman, On the frequency of numbers containing prime factors of a certain relative magnitude, Ark. Mat. Astr. Fys. 22A (1930).
• N. G. de Bruijn, On the number of positive integers $\le x$ and free of prime factors $>y$, Proc. KNAW Ser. A 54 (1951). https://research.tue.nl/en/publications/on-the-number-of-positive-integers-leq-x-and-free-of-prime-factor/
• P. Erdős and C. Pomerance, On the largest prime factors of $n$ and $n+1$, Aequationes Math. 17 (1978), 311–321. https://www.renyi.hu/~p_erdos/1978-29.pdf
• J. Teräväinen, On binary correlations of multiplicative functions, Forum Math. Sigma 6 (2018), e10. https://doi.org/10.1017/fms.2018.10
• T. Tao and J. Teräväinen, The structure of correlations of multiplicative functions at almost all scales, with applications to the Chowla and Elliott conjectures, Algebra Number Theory 13 (2019). https://doi.org/10.2140/ant.2019.13.2103
• K. Matomäki and M. Radziwiłł, Multiplicative functions in short intervals, Ann. of Math. 183 (2016). https://doi.org/10.4007/annals.2016.183.3.6
• T. Tao and J. Teräväinen, Quantitative correlations and some problems on prime factors of consecutive integers, preprint (2026). https://arxiv.org/abs/2512.01739
• OpenAI, The joint Dickman law for consecutive integers, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1 and Corollary 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-joint-Dickman-law-for-consecutive-integers-September-24-2026/paper.pdf

Motivation

Large service systems such as call centers and hospital wards are modelled as many-server queues: $N$ identical servers, customers arriving according to a general process, service requirements drawn independently from a general distribution $G$, and a single first-come-first-served queue. When $G$ is not exponential the number of customers in system is not Markov, and a tractable state must keep track of how long each customer in service has been served. Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011)) take as state the number in system together with the age measure, the point measure of the ages of the customers in service, and prove a functional law of large numbers: scaled by $N$, these processes converge to the unique solution of a deterministic system, the fluid equations. Earlier fluid and diffusion analyses of the $G/GI/N$ queue worked with other state descriptors (Reed, Ann. Appl. Probab. 19 (2009); Whitt, Oper. Res. 54 (2006)); the measure-valued description records the elapsed service time of every customer in service, which is the information a non-exponential service distribution requires.

This mission covers the deterministic half of that result: the fluid equations are well posed, and their solution is given in closed form.

Setting

Service requirements have a density $g$ that vanishes on $(-\infty,0)$, $G(x)=\int_{(-\infty,x]}g$, and the mean is normalized to one, $\int x\,g(x)\,dx=1$. Let $M=\sup\{x\ge0: G(x)<1\}\in(0,\infty]$ and let $h=g/(1-G)$ be the hazard rate on $[0,M)$; $h$ is locally integrable on $[0,M)$ but not integrable on it. For a measure $\mu$ and a function $f$ write $\langle f,\mu\rangle=\int f\,d\mu$, and $\mathbf 1$ for the constant one.

The data are a triple $(\bar E,\bar X(0),\bar\nu_0)$ in

$$\mathcal S_0=\{(f,x,\mu): f \text{ nondecreasing càdlàg}, f(0)=0;\ x\ge0;\ \mu \text{ a measure on }[0,M),\ \langle\mathbf 1,\mu\rangle\le1,\ 1-\langle\mathbf 1,\mu\rangle=[1-x]^+\},$$

where $\bar E$ is the cumulative arrival process, $\bar X(0)$ the initial number in system and $\bar\nu_0$ the initial age measure (per server, so the total capacity is one). A càdlàg pair $(\bar X,\bar\nu)$, with $\bar\nu_t$ a sub-probability measure on $[0,M)$ in the weak topology, solves the fluid equations if for every $t\ge0$: $\int_0^t\langle h,\bar\nu_s\rangle ds<\infty$ (3.4); for every test function $\varphi\in\mathcal C_c^{1,1}([0,M)\times\mathbb R_+)$

$$\langle\varphi(\cdot,t),\bar\nu_t\rangle=\langle\varphi(\cdot,0),\bar\nu_0\rangle+\int_0^t\langle\varphi_x+\varphi_s,\bar\nu_s\rangle ds-\int_0^t\langle h\varphi(\cdot,s),\bar\nu_s\rangle ds+\int_{[0,t]}\varphi(0,s)\,d\bar K(s)\quad(3.5);$$

$\bar X(t)=\bar X(0)+\bar E(t)-\bar D(t)$ (3.6); and the nonidling condition $1-\langle\mathbf 1,\bar\nu_t\rangle=[1-\bar X(t)]^+$ (3.7). Here $\bar D(t)=\int_0^t\langle h,\bar\nu_s\rangle ds$ is the cumulative departure process and $\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\bar D(t)$ the cumulative entry into service. Equation (3.5) is a weak form of a transport equation: mass moves to the right at unit speed, is killed at rate $h$, and enters at age $0$ at rate $d\bar K$.

Formalization targets

Goal: Theorem 3.5

For every $(\bar E,\bar X(0),\bar\nu_0)\in\mathcal S_0$:

1. the fluid equations have at most one solution;
2. under (3.4) and the path conditions, $(\bar X,\bar\nu)$ is a solution if and only if it satisfies (3.6), (3.7) and, for every bounded continuous $f$ and $t\ge0$,

$$\langle f,\bar\nu_t\rangle=\int_{[0,M)}f(x+t)\frac{1-G(x+t)}{1-G(x)}\,\bar\nu_0(dx)+\int_{[0,t]}f(t-s)\big(1-G(t-s)\big)\,d\bar K(s);\quad(3.11)$$

3. if $\bar E$ has a density $\bar\lambda$, then $\bar K$ has a density $\bar\kappa$ equal a.e. to $\bar\lambda$ where $\bar X<1$, to $\bar\lambda\wedge\langle h,\bar\nu_t\rangle$ where $\bar X=1$, and to $\langle h,\bar\nu_t\rangle$ where $\bar X>1$ (3.12);
4. if moreover $\bar\nu_0$ is absolutely continuous, so is every $\bar\nu_t$.

Milestones

• Remark 4.3, (4.4): integration by parts for the entry term of (4.3).
• (4.55): the integrated hazard in closed form, $\psi_h(x,t)=(1-G(x))/(1-G(x-t))$ or $1-G(x)$.
• Theorem 4.1: for a Radon-measure-valued path satisfying the hazard bound (4.1), the age equation (4.2), which is (3.5) with an arbitrary Radon measure $\upsilon_0$ and an arbitrary $Z$ of bounded variation in place of $\bar\nu_0$ and $\bar K$, holds if and only if the representation (4.3) holds.
• Proof of Corollary 4.4: $\bar K$ is nondecreasing.
• Corollary 4.4, (4.5): $\bar K(t)=\langle\mathbf 1,\bar\nu_t\rangle-\langle\mathbf 1,\bar\nu_0\rangle+\int\frac{G(x+t)-G(x)}{1-G(x)}\bar\nu_0(dx)+\int_0^tg(t-s)\bar K(s)ds$.
• Lemma 4.5: $\|\langle f,\bar\nu^2_s\rangle-\langle f,\bar\nu^1_s\rangle\|_T\le\|f\|_M|\Delta\upsilon_0|_{TV}+(2\|f\|_T+\|f'\|_T)\|\Delta Z\|_T$.
• Theorem 4.6: with equal initial measures, $\|\Delta\bar K\|_T\vee\|\Delta\bar D\|_T\le|\Delta\bar X(0)|+\|\Delta\bar E\|_T$, together with (4.8) and (4.10).

Significance

Uniqueness of the fluid solution is what turns tightness of the scaled $N$-server processes into convergence: every subsequential limit solves the fluid equations, so all coincide (the paper's Theorem 3.7). The representation (3.11) reduces the measure-valued equation to the scalar process $\bar K$, and the continuity estimate of Theorem 4.6 says the fluid solution is a Lipschitz function of the arrival process. Both are used in the paper's study of long-time behaviour, where $\bar\nu_t$ converges to the measure with density $1-G$, and (3.12) is the form of the entry rate used there.

The results are proved in the paper. None of them, and no part of the measure-valued fluid model, has a machine-checked proof. Formalizing them produces a checked weak-solution theory for a transport equation with an unbounded killing rate and a measure-valued boundary input, which is a reusable piece of infrastructure for other age- and residual-time-based queueing models.

Difficulty

The central step is Theorem 4.1. The naive approach treats (4.2) as a first-order PDE and integrates along characteristics, but the solution is only a càdlàg path of measures, $h$ is merely locally integrable and blows up near $M$, and $Z$ may jump, so classical characteristics are not available; the test functions must not vanish on the boundary $x=0$, since that is where the entry term lives. The second difficulty is in Theorem 4.6: the entry process $\bar K$ is defined implicitly through the nonidling condition, and comparing two solutions requires a first-crossing argument that distinguishes whether the system is below, at or above capacity at that time.

Formalization scope

The service law is its density $g$ (ServiceLaw), with $g=0$ below $0$, $\int g=1$ and mean one. Time is $\mathbb R$ read on $[0,\infty)$; every condition is stated for $t\ge0$. Measures of the fluid model are FiniteMeasure ℝ carried by $[0,M)$, whose topology is weak convergence, so càdlàg paths are càdlàg in $\mathcal M_F[0,M)$ with the weak topology. The paths of Theorem 4.1 and Lemma 4.5 are ℝ → Measure ℝ with values Radon on $[0,M)$ (possibly infinite) and càdlàg in the vague topology. $M\in[0,\infty]$ is an extended number. The integral in (3.4) is a lower integral in $[0,\infty]$, and $\bar D$, $\bar K$ are its real value. $d\bar K$ is the Lebesgue–Stieltjes measure of $\bar K$, with no atom at $0$. A function $Z$ of bounded variation is a difference $Z_1-Z_2$ of nondecreasing càdlàg functions vanishing at $0$.

Explicit choices: compact support of test functions is relative to $[0,M)\times\mathbb R_+$, so $\varphi(0,s)$ need not vanish (with supports taken in $\mathbb R^2$ the entry term of (3.5) would vanish identically); $\bar\nu(0)=\bar\nu_0$ and $\bar X(0)$ equal to the datum are clauses of the fluid equations, but not of the age equation, where $\upsilon_0$ is arbitrary; functions in $\mathcal C_b(\mathbb R_+)$, $\mathcal C_c(\mathbb R_+)$ and $\mathcal C^1_b(\mathbb R_+)$ are represented by functions on $\mathbb R$ of the same class, of which only values on $[0,\infty)$ are read; norms in Lemma 4.5 are computed in $[0,\infty]$, since $|\Delta\upsilon_0|_{TV}$ may be infinite. Two printed statements are corrected: in Theorem 3.5 the paper's right-hand side of the equivalence lists (3.6) and (3.11); the nonidling condition (3.7), part of the fluid equations on the left, is kept on the right, as the proof requires. In (4.10), $\Delta\bar X(0)$ is replaced by $|\Delta\bar X(0)|$, which is what Lemma 4.5 and (4.9) give.

A fluid solution is defined by the weak transport equation (3.5), never by the representation (3.11) or by a formula for $\bar\nu$ in terms of $\bar K$; with such a definition the equivalence of the goal would be an unfolding of definitions.

A complete development needs Lebesgue–Stieltjes integration by parts for càdlàg functions of bounded variation, the Riesz description of the vague topology, and uniqueness for weak solutions of transport equations; these are reusable beyond this mission. Proofs of any milestone, and of the parts of Theorem 3.5 separately, are welcome. The paper's Section 4.3 machinery (the abstract and simplified age equations, Lemmas 4.12–4.13, Propositions 4.15–4.16) is not posed here and may be formalized as supporting lemmas.

Selected references

• H. Kaspi and K. Ramanan, Law of large numbers limits for many-server queues, Ann. Appl. Probab. 21(1) (2011), 33–114. https://doi.org/10.1214/09-AAP662
• J. Reed, The G/GI/N queue in the Halfin–Whitt regime, Ann. Appl. Probab. 19(6) (2009), 2211–2269. https://doi.org/10.1214/09-AAP609
• W. Whitt, Fluid models for multiserver queues with abandonments, Oper. Res. 54(1) (2006), 37–54. https://doi.org/10.1287/opre.1050.0227
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236