Analysis

Motivation

The notebooks Ramanujan kept in India record identities, evaluations, transformations and general principles, usually presented without proofs. They preserve a working mathematician's collection rather than a textbook arranged around a sequence of prerequisite theorems. The Tata Institute of Fundamental Research published an unedited facsimile edition in 1957, making the manuscripts available for systematic study.

Bruce C. Berndt's Ramanujan's Notebooks, published by Springer in five parts in 1985, 1989, 1991, 1994 and 1998, supplies that study. The volumes examine the entries individually, proving them, correcting them where necessary, or explaining why they are false or lack a rigorous interpretation. Their subject matter ranges from magic squares and combinatorial identities to hypergeometric series, continued fractions, elliptic functions, modular equations, class invariants and asymptotic expansions.

This mission takes the results established in Berndt's treatment as formalization targets. The published arguments provide mathematical reference proofs. The remaining task is to express the results precisely and construct proofs checked by Lean.

Setting

An entry is a source claim identified by its chapter and local entry label in Berndt's series. The collection is organized around one Lean statement per entry that Berndt establishes. Where an entry contains separately identified parts, corollaries or examples, suffixes distinguish the corresponding statements while preserving their common source location. Intermediate steps of a printed proof do not automatically become additional targets.

The mission covers Chapters 1–39. Part I contains Chapters 1–9; Part II, Chapters 10–15; Part III, Chapters 16–21; Part IV, Chapters 22–31; and Part V, Chapters 32–39. The Part IV appendix on the first notebook and the Quarterly Reports treated in Part I also belong to the mission's scope, with their statements incorporated as they are added.

Declarations use the namespace RamanujanNotebooks and names of the form entry_<chapter>_<entry>, such as RamanujanNotebooks.entry_16_19. Shared definitions fix the meaning of recurring objects: q-shifted factorials, theta functions, hypergeometric series, continued-fraction convergents and the special functions used across chapters. Their domains, normalizations and indexing conventions are documented so that different entries refer to the same mathematical objects.

Formalization targets

The series has no single capstone theorem. Its goal item is therefore a representative entry: Chapter 16, Entry 19, Jacobi's triple product identity in Ramanujan's notation. This is in Part III, whose chapter develops q-series and theta functions.

For complex parameters $a,b$, Ramanujan's general theta function is

$$f(a,b)=\sum_{n\in\mathbb Z} a^{n(n+1)/2}b^{n(n-1)/2}.$$

Both exponents are nonnegative integers. Under $|ab|<1$, the series converges absolutely, and Entry 19 identifies it with an infinite product. Writing $q=ab$, the target is

$$f(a,b)=\prod_{m=0}^{\infty} (1+a q^m)(1+b q^m)(1-q^{m+1}), \qquad |ab|<1.$$

Equivalently, with the infinite q-Pochhammer symbol

$$(z;q)_\infty=\prod_{m=0}^{\infty}(1-zq^m),$$

the identity reads

$$f(a,b)=(-a;ab)_\infty(-b;ab)_\infty(ab;ab)_\infty.$$

The Lean statement uses ramanujanTheta and qPochInf, with the hypothesis ‖a * b‖ < 1. Proving this goal establishes the representative identity; completion of the collection is tracked through its member statements, one per entry.

Every entry is a separate statement of this mission, named RamanujanNotebooks.entry_<chapter>_<entry> (with suffixes for parts, corollaries and examples): 3,863 statements for Parts I–V, the Part IV appendix on the first notebook and the Quarterly Reports; the AMS Memoir 477 statements are being added. A chapter's statements are found by searching for its name prefix. The milestone list has one milestone per chapter, in source order, titled like “Part III · Ch. 16 — q-series and theta-functions”; each links one representative result and its description names the chapter's main results.

Statement conventions and source differences

The mathematical reference is what Berndt proves, with the hypotheses his argument requires. A notebook display alone is insufficient when its domain, convergence conditions or branch choices are unstated. Each target identifies its source and records the conditions under which the asserted equality, limit, transformation or asymptotic relation is established.

Corrected statements carry the explicit phrase “Differs from the printed source”. The accompanying note explains the difference and its origin: a correction supplied by Berndt, a restriction required by the proof, or a reading that resolves an ambiguity. A proposed repair supported only by numerical experiments requires further mathematical review before inclusion as a result established by the reference.

Entries that Berndt shows to be false are not stated as theorem targets. Neither are identities treated only formally, without a rigorous version. For example, Chapter 37's Entry 34 manipulates divergent series, while Entries 35–37 are shown false. Chapter 39 also contains formal claims and entries for which the book supplies no definite interpretation. Such omissions preserve the boundary between a proved result and a suggestive manuscript formula.

Numerical checks are recorded in theorem docstrings, including the tested parameters and the kind of comparison performed. They help detect indexing errors, sign errors and unsuitable domains. Agreement at sampled points is evidence about the transcription; it is not a proof of the universally quantified Lean statement.

Significance and status

The mission brings together source-linked statements of known results whose proofs otherwise remain dispersed across Berndt's commentary. Formal proofs can expose exactly which analytic hypotheses an identity needs and make the shared special-function definitions available for later developments. A proof of the triple product, for example, connects the series definition of the general theta function with its product representation, which recurs throughout the theta-function material.

The statements are proof targets. A declaration that type-checks has a meaningful Lean type; that check alone does not establish the proposition. The description makes no claim that the collection already has machine-checked proofs. Progress is measured by proofs of the individual targets with their stated hypotheses.

Difficulty

The entries vary considerably in their prerequisites. Finite algebraic and combinatorial identities can be approached with relatively little analytic infrastructure. Other chapters depend on convergence theory for continued fractions, transformations of theta and elliptic functions, modular forms, or class invariants.

Even a short equality can require substantial work before its expressions have the intended meaning. A divergent series cannot be interpreted as an ordinary sum, and a complex root or logarithm needs an appropriate branch convention. The central challenge is to preserve the object and domain of the reference result while supplying the formal infrastructure needed to prove it.

Formalization scope

Statements use real or complex variables according to the reference, with exceptional values, nonvanishing conditions and convergence ranges explicit. Infinite series are expressed with convergence assertions where necessary; continued fractions are represented through their convergents and limits. Integrals carry the hypotheses needed for their intended interpretation. Lean's total definitions of division, infinite sums and infinite products must not turn an undefined or divergent source expression into a trivial theorem.

Contributions should prove the registered statements using their shared definitions. Reusable lemmas about convergence, special functions and transformations are part of that work. Any suspected statement error should be reported with the declaration name, source location and a specific mathematical objection, so that the source relationship can be reviewed before a replacement is prepared.

Selected references

• S. Ramanujan, Notebooks, facsimile edition, Tata Institute of Fundamental Research, Bombay, 1957.
• B. C. Berndt, Ramanujan's Notebooks, Part I, Springer, 1985.
• B. C. Berndt, Ramanujan's Notebooks, Part II, Springer, 1989.
• B. C. Berndt, Ramanujan's Notebooks, Part III, Springer, 1991.
• B. C. Berndt, Ramanujan's Notebooks, Part IV, Springer, 1994.
• B. C. Berndt, Ramanujan's Notebooks, Part V, Springer, 1998.

Motivation

A fractional program minimizes a ratio $f(x)/g(x)$ over a set $S$. Nonconvex, nonsmooth ratios arise in the scale-invariant sparse signal recovery model $\min\|x\|_1/\|x\|_2$ over a polyhedron, in robust Sharpe-ratio optimization in finance, and in the Rayleigh quotient $x^\top Ax/x^\top Bx$ over a sphere; with $g\equiv1$ and $S=H$ the problem reduces to composite optimization $\min f^{\mathsf s}+f^{\mathsf n}$. The classical method of Dinkelbach (1967) and its proximal-gradient descendants assume a convex numerator and a concave or smooth denominator, which these models do not satisfy.

Boţ, Dao and Li (arXiv:2003.04124, Math. Oper. Res. 2022) propose the extrapolated proximal subgradient algorithm (e-PSG) for problems in which the numerator is the sum of a smooth convex and a nonsmooth nonconvex term and the denominator is only weakly convex, and they prove that its cluster points satisfy a first-order condition. This mission formalizes that subsequential convergence theorem (Theorem 4.5).

Setting

Let $H=\mathbb R^N$ with the Euclidean inner product, and let $S\subseteq H$ be nonempty, closed and convex. The problem is

$$\min_{x\in S}\ \frac{f(x)}{g(x)}.\qquad(\mathrm P)$$

Assumption 1. $f=f^{\mathsf s}+f^{\mathsf n}$, where $f^{\mathsf s}:H\to\mathbb R$ is continuously differentiable and convex with an $\ell$-Lipschitz gradient, $f^{\mathsf n}:H\to(-\infty,+\infty]$ is proper and lower semicontinuous, $S\cap\operatorname{dom}f\ne\emptyset$, and $f\ge0$ on $S\cap\operatorname{dom}f$.

Assumption 2. $g$ is finite and positive on $S$, continuous on an open set containing $S$, and either weakly convex with modulus $\beta$ on an open convex set containing $S$ (that is, $g+\frac\beta2\|\cdot\|^2$ is convex there), or regular (Fréchet and limiting subdifferentials coincide) and weakly convex with modulus $\beta$ on $S$.

The limiting subdifferential $\partial_L h(x)$ collects limits of Fréchet subgradients $u_k\in\widehat\partial h(x_k)$ along $x_k\to x$ with $h(x_k)\to h(x)$. A point $\bar x\in S$ is a lifted stationary point of (P) if

$$0\in g(\bar x)\,\partial_L(f+\iota_S)(\bar x)-f(\bar x)\,\partial_L g(\bar x),$$

where $\iota_S$ is $0$ on $S$ and $+\infty$ off $S$.

The boundedness condition (BC) asks for $0<m\le g\le M$ on $S\cap\operatorname{dom}f$. Algorithm 1 (e-PSG) starts from $x_{-1}=x_0\in S\cap\operatorname{dom}f$ with parameters $\delta>0$, $\zeta>0$ ($1-\sqrt\beta\zeta>0$) and extrapolation bounds $\bar\mu,\bar\kappa$ (in explicit ranges depending on $m,M,\ell$ under (BC), and $\bar\mu=\bar\kappa=0$ otherwise). At step $n$ it sets $\theta_n=f(x_n)/g(x_n)$, picks $g_n\in\partial_L g(x_n)$ and $0<\tau_n\le1/\max\{\sqrt\beta\theta_n/\zeta,\delta\}$, forms $u_n=x_n+\kappa_n(x_n-x_{n-1})$, $v_n=x_n+\mu_n(x_n-x_{n-1})$ with $\kappa_n\in[0,\bar\kappa]$, $\mu_n\in[0,\bar\mu\tau_n]$, and takes

$$x_{n+1}\in\operatorname*{argmin}_{x\in S}\Big(f^{\mathsf n}(x)+f^{\mathsf s}(u_n)+\langle\nabla f^{\mathsf s}(u_n),x-u_n\rangle+\tfrac1{2\tau_n}\|x-v_n-\tau_n\theta_ng_n\|^2+\tfrac\ell2\|x-u_n\|^2\Big).$$

Finally $S_0=\{x\in S: f(x)/g(x)\le f(x_0)/g(x_0)\}$.

Formalization targets

Goal: Theorem 4.5(iii)

If $S_0$ is bounded and $\liminf_n\tau_n=\bar\tau>0$, then every cluster point $\bar x$ of $(x_n)$ satisfies

$$\bar x\in S\cap\operatorname{dom}f,\qquad \lim_{n\to\infty}\frac{f(x_n)}{g(x_n)}=\frac{f(\bar x)}{g(\bar x)},\qquad \bar x\ \text{is lifted stationary.}$$

In the formal statement $g$ is in addition Lipschitz around every point of $S$; see Formalization scope.

Milestones, in proof order

1. Lemma 4.3: for $x,y\in S$ and $u\in\partial_L g(x)$, $\langle u,y-x\rangle\le g(y)-g(x)+\frac\beta2\|y-x\|^2$.
2. Lemma 4.4 (descent lemma), already on the platform.
3. Inequality (16): the one-step inequality from the subproblem.
4. Inequality (17): the ratio inequality, for every Young parameter $\omega>0$.
5. Theorem 4.5(i): $x_n\in S\cap\operatorname{dom}f$ and

$$\Big(\tfrac{f(x_{n+1})}{g(x_{n+1})}+c\|x_{n+1}-x_n\|^2\Big)+\alpha\|x_{n+1}-x_n\|^2\le\tfrac{f(x_n)}{g(x_n)}+c\|x_n-x_{n-1}\|^2$$

with the explicit constants (14), and convergence of $f(x_n)/g(x_n)$. 6. Theorem 4.5(ii): $(x_n)$ is bounded, $\|x_{n+1}-x_n\|\to0$, and $\sum_n\|x_{n+1}-x_n\|^2<\infty$. 7. The limit inequality at a cluster point (proof of Theorem 4.5(iii), p. 13).

Significance

Theorem 4.5 is the subsequential convergence result on which the paper's later results rest: with a Kurdyka–Łojasiewicz property of a merit function it upgrades to convergence of the whole sequence and to linear rates (Theorem 5.5), and under strict differentiability of $g$ lifted stationarity becomes ordinary stationarity (Corollary 4.6). The merit function $F_n=f(x_n)/g(x_n)+c\|x_n-x_{n-1}\|^2$ with explicit constants is the template for analyzing extrapolated proximal methods on ratio objectives.

The result is proved on paper; no machine-checked version exists. Formalizing it produces a verified descent analysis of an extrapolated proximal method for a nonconvex ratio, a formal subgradient inequality for weakly convex functions with respect to the limiting subdifferential, and a checked passage to the limit through limiting subdifferentials. It also pins down the hypotheses: the formal statement records a missing assumption of the printed theorem (below).

Difficulty

The ratio is not a sum, so the standard sufficient-decrease argument for proximal gradient methods does not apply directly: the subproblem linearizes $g$ through a limiting subgradient $g_n$ scaled by the current ratio $\theta_n$, and the descent of $f/g$ comes only after dividing by $g(x_{n+1})$, which ties the step size to $\theta_n$ and to bounds on $g$. Extrapolation adds a cross term $\langle x_{n+1}-x_n,x_n-x_{n-1}\rangle$ that the merit function must absorb, which is where the explicit ranges of $\bar\mu,\bar\kappa$ come from. At a cluster point, $f$ is only lower semicontinuous, so convergence of $f(x_{k_n})$ to $f(\bar x)$ must be extracted from the optimality of the subproblems, and the limits of $g_n$ must be shown to lie in $\partial_L g(\bar x)$. The naive approach of passing to the limit in the subproblem's optimality condition fails because $\partial_L(f^{\mathsf n}+\iota_S)$ has no sum rule in this generality.

Formalization scope

$H$ is EuclideanSpace ℝ (Fin N). Functions into $(-\infty,+\infty]$ are EReal-valued; properness is the published IsProperFn, and $\widehat\partial$, $\partial_L$ are the published IsRegularSubgrad and LimitingSubdiff. The denominator $g$ is real-valued on all of $H$: only its values and subgradients near $S$ enter, where the paper's $g$ is finite. Weak convexity "with modulus $\beta$" means that $\beta\ge0$ is a valid constant, not the smallest one. A run of Algorithm 1 is a predicate on the sequences $(x_n),(g_n),(\tau_n),(\kappa_n),(\mu_n)$; the argmin and $g_n$ are selections, never Classical.choose. $x_{-1}=x_0$. Ratios are real numbers (f x).toReal / g x, meaningful because the iterates stay in $\operatorname{dom}f$. The $\bar\kappa$-range of Step 1 is written as $\ell\bar\kappa^2<\frac{m\delta(1-\sqrt\beta\zeta)}M-\frac{2m\bar\mu}{\sqrt{mM}}$, avoiding division by $\ell$. $\liminf\tau_n>0$ is an eventual positive lower bound, which is equivalent since $\tau_n\le1/\delta$. Cluster points are MapClusterPt.

Correction. Under the second alternative of Assumption 2 alone, Theorem 4.5(iii) fails: for $S=[0,1]$, $g(x)=2-\sqrt x$ on $S$ and $f(x)=1-\sqrt x/4$, the iterates converge to $0$, where $\partial_Lg(0)=\emptyset$, so $0$ is not lifted stationary. The goal and the limit-inequality milestone therefore assume that $g$ is Lipschitz around every point of $S$, which holds automatically under the first alternative.

The trivializing formalizations are ruled out: the parameter ranges are inhabited (checked in Lean, including $\ell=0$), the goal quantifies over every cluster point of every run, and lifted stationarity requires actual limiting subgradients rather than an infDist that would be $0$ on an empty set.

Contributions welcome: the subgradient inequality for weakly convex functions, the descent lemma's use in (16), the limit arguments for limiting subdifferentials (the platform has the robustness property (3) as NonconvexSplitting.ProxGrad.limitingSubdiff_robust), and Fermat's rule for constrained minimizers of $\varphi+\iota_S$ — the last is reusable well beyond this mission.

Selected references

• R. I. Boţ, M. N. Dao, G. Li, Extrapolated Proximal Subgradient Algorithms for Nonconvex and Nonsmooth Fractional Programs, Math. Oper. Res. 47 (2022); arXiv:2003.04124v2. https://arxiv.org/abs/2003.04124
• W. Dinkelbach, On nonlinear fractional programming, Management Science 13 (1967) 492–498. https://doi.org/10.1287/mnsc.13.7.492
• B. S. Mordukhovich, Variational Analysis and Generalized Differentiation I, Springer, 2006. https://doi.org/10.1007/3-540-31247-1
• Y. Nesterov, Introductory Lectures on Convex Optimization, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Interior-point methods for conic optimization are best understood on symmetric cones: the nonnegative orthant, the second-order cone and the cone of positive semidefinite matrices. On these cones the barrier functions are self-scaled, and Nesterov and Todd showed that every primal-dual pair $(x, s)$ then has a unique scaling point $w$ with $s = F''(w)x$ and $F'(x) = F''(w)F_*'(s)$. The resulting primal-dual algorithms, implemented in solvers such as SeDuMi and MOSEK, combine long steps with good worst-case complexity.

Many models in statistics, geometric programming, entropy maximization and logistic regression need the exponential cone, which is not symmetric. Dahl and Andersen (Math. Program. 194, 2022) designed the primal-dual algorithm behind MOSEK's exponential-cone support. To explain why they cannot simply transplant the Nesterov–Todd construction, they use a property that sits between "self-scaled" and "arbitrary": negative curvature of the barrier. Barriers of symmetric cones have it; a barrier is self-scaled if and only if both it and its conjugate have it (Nesterov–Tunçel, 2016); and barriers with negative curvature still admit a unique scaling point satisfying one secant equation. Dahl and Andersen observe in §5 that the exponential-cone barrier lies outside this class, by an explicit witness. This mission formalizes that observation and the derivative formulas of their Appendix A it rests on.

Timeline:

• 1997–1998: Nesterov and Todd introduce self-scaled barriers and their primal-dual scalings (Math. Oper. Res. 22; SIAM J. Optim. 8).
• 2001: Tunçel generalizes primal-dual scalings to arbitrary convex cones (Found. Comput. Math. 1).
• 2009: Chares studies the exponential cone and its 3-self-concordant barrier (thesis, Université catholique de Louvain).
• 2016: Nesterov and Tunçel characterize self-scaled barriers through negative curvature of the barrier and its conjugate.
• 2022: Dahl and Andersen give a primal-dual algorithm for the exponential cone with Tunçel-type scalings, and note that its barrier does not have negative curvature.

Setting

Points of $\mathbb{R}^3$ are written $x = (x_1, x_2, x_3)$. The exponential cone is the closure

$$K_{\exp} = \operatorname{cl}\{x \in \mathbb{R}^3 \mid x_1 \ge x_2 \exp(x_3/x_2),\ x_2 > 0\},$$

whose interior is $\{x \mid x_2 > 0,\ x_1 > x_2\exp(x_3/x_2)\}$. Its standard barrier is

$$F(x) = -\log\bigl(x_2\log(x_1/x_2) - x_3\bigr) - \log x_1 - \log x_2, \qquad (2)$$

defined and smooth on $\operatorname{int}(K_{\exp})$. Appendix A of the paper writes $F = g + h$ with

$$\psi(x) = x_2\log(x_1/x_2) - x_3,\qquad g(x) = -\log\psi(x),\qquad h(x) = -\log x_1 - \log x_2 .$$

For a smooth $F$ on an open set, $F''(x)$ is its Hessian, a symmetric linear map of $\mathbb{R}^n$, and the third directional derivative is the symmetric linear map

$$F'''(x)[u] = \frac{d}{dt}F''(x + tu)\Big|_{t=0}, \qquad F'''(x)[u, v, v] = \langle F'''(x)[u]\,v, v\rangle .$$

A barrier $F$ of a cone $K$ has negative curvature if for all $x \in \operatorname{int}(K)$ and for $u \in K$

$$F'''(x)[u] \preceq 0,$$

where $\preceq$ is the Loewner order: $\langle F'''(x)[u]\,v, v\rangle \le 0$ for every $v$. The direction $u$ ranges over the closed cone $K$, including its boundary.

Formalization targets

Goal: the exponential-cone barrier does not have negative curvature

$$\neg\Bigl(\forall x \in \operatorname{int}(K_{\exp}),\ \forall u \in K_{\exp},\ \forall v \in \mathbb{R}^3:\ \langle F'''(x)[u]\,v, v\rangle \le 0\Bigr).$$

The goal asserts only the qualitative failure, so it does not depend on the particular witness.

Milestones

1. The witness: $\hat x := (1, e^{-2}, 0) \in \operatorname{int}(K_{\exp})$ and $\hat u := (1, 0, 0) \in K_{\exp}\setminus\operatorname{int}(K_{\exp})$ (§5, p. 356).
2. First-order derivatives (A.1, p. 367): $\psi'(x) = (x_2/x_1,\ \log(x_1/x_2) - 1,\ -1)$, $h'(x) = -(1/x_1, 1/x_2, 0)$, $g'(x) = -\psi'(x)/\psi(x)$, $F' = g' + h'$ on $\operatorname{int}(K_{\exp})$.
3. Second-order derivatives (A.2, p. 367):

$$F''(x) = -\frac{1}{\psi(x)}\Bigl(\psi''(x) - \frac{\psi'(x)\psi'(x)^T}{\psi(x)}\Bigr) + h''(x).$$

4. Third-order directional derivatives (A.3 and (33), p. 368): the closed form of $F'''(x)[u]$ in terms of $\psi$, its derivatives and $h'''(x)[u]$.
5. The matrix at the witness (§5, p. 356):

$$F'''(\hat x)[\hat u] = \begin{bmatrix} -4 & e^2/2 & e^2/2 \\ e^2/2 & 0 & 0 \\ e^2/2 & 0 & -e^4/4 \end{bmatrix}.$$

6. The positive value (§5, p. 356): $F'''(\hat x)[\hat u, \hat v, \hat v] = 4$ for $\hat v := (1, 8e^{-2}, 4e^{-2})$.

Significance

The result. Negative curvature is the property that gives symmetric-cone barriers their long-step Hessian estimates and a unique scaling point with one secant equation. Its failure for the exponential-cone barrier means that none of these consequences can be invoked for the exponential cone. An algorithm for this cone has to obtain its scalings by other means; Dahl and Andersen take them from Tunçel's framework, via the quasi-Newton secant updates of §5. The witness also shows that the failure occurs already for a direction on the boundary of the cone, at an interior point with simple coordinates.

Formalizing it. The claim is proved in the paper by a computation "using the expressions in the appendix", with the details left to the reader. The appendix formulas for the gradient, Hessian and third directional derivative of the exponential-cone barrier are the ones an implementation evaluates, including the higher-order corrector term $-\tfrac12F'''(x)[u, v]$. A machine-checked version certifies these closed forms, including the zero padding of the $2\times2$ "leading parts" in (33), and gives a reusable definition of negative curvature that applies to any cone and barrier. As far as is known, none of these statements has a machine-checked proof.

Difficulty

The obstacle is computational, not conceptual. The barrier is a composition of logarithms with a function $\psi$ that is itself a perspective of the logarithm, so its third derivative is a sum of terms with denominators $\psi(x)^k$, $x_1^k$ and $x_2^k$. Stating it as a derivative of the Hessian map requires showing that the Hessian is differentiable on the open interior, which in turn requires a description of that interior, a set defined as the interior of a closure. The membership claims about $\hat u$ are not definitional either: $\hat u$ lies on the boundary, reached only as a limit of points of the generating set, and its non-interiority needs a neighbourhood argument. Finally, the cone condition on $u$ matters: replacing $u \in K_{\exp}$ by $u \in \mathbb{R}^3$ makes the claim nearly trivial, because $F'''(x)[-u] = -F'''(x)[u]$.

Formalization scope

• Points of $\mathbb{R}^3$ are EuclideanSpace ℝ (Fin 3); the paper's $(x_1, x_2, x_3)$ are (x 0, x 1, x 2), and vectors are written !₂[·, ·, ·].
• $K_{\exp}$ is the closure of the printed set, not its interior or an equivalent description. $F$, $\psi$, $g$, $h$ are defined on all of $\mathbb{R}^3$ by their formulas with Real.log; every statement evaluates them, and their derivatives, only at points of $\operatorname{int}(K_{\exp})$, where all logarithms are the genuine ones. The appendix formulas carry the hypothesis $x \in \operatorname{int}(K_{\exp})$.
• $F''$ is the published SelfScaledIPM.ShortStep.hess (derivative of the gradient), and $F'''(x)[u]$ is fderiv ℝ (hess F) x u. The Loewner order is stated through the quadratic form for every $v$. Matrices act through the standard basis (Matrix.toEuclideanCLM).
• Disclosed deviations from the page: milestone 1 asserts $\hat x \in \operatorname{int}(K_{\exp})$, stronger than the printed $\hat x \in K_{\exp}$ and the form the definition needs. In A.3 the $2\times2$ leading parts $\hat h'''$, $\hat\psi'''$ of (33) are padded with a zero third row and column, and $g''(x)$ is written out by the A.2 formula. Only the first display of A.2 is stated, not the factorization $F''(x) = R(x)R(x)^T$.
• A trivializing formalization would let $u$ range over all of $\mathbb{R}^3$, or read $\preceq 0$ entrywise; both are excluded, and $u$ ranges over the closed cone exactly as in the paper.
• The claim that $F$ is a 3-self-concordant barrier (quoted from Chares) is not part of the mission. The definition of negative curvature applies to any cone in any dimension and can be reused for other barriers. Contributions of calculus lemmas for logarithmic barriers on open sets (differentiability of the Hessian map, interiors of closures of epigraph-type sets) are welcome.

Selected references

• J. Dahl, E. D. Andersen, A primal-dual interior-point algorithm for nonsymmetric exponential-cone optimization, Mathematical Programming 194 (2022), 341–370. https://doi.org/10.1007/s10107-021-01631-4
• Yu. Nesterov, M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Mathematics of Operations Research 22 (1997), 1–42. https://doi.org/10.1287/moor.22.1.1
• Yu. Nesterov, M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM Journal on Optimization 8 (1998), 324–364. https://doi.org/10.1137/S1052623495290209
• L. Tunçel, Generalization of primal-dual interior-point methods to convex optimization problems in conic form, Foundations of Computational Mathematics 1 (2001), 229–254. https://doi.org/10.1007/s102080010008
• Yu. Nesterov, L. Tunçel, Local superlinear convergence of polynomial-time interior-point methods for hyperbolicity cone optimization problems, SIAM Journal on Optimization 26 (2016), 139–170. https://doi.org/10.1137/140978296
• P. R. Chares, Cones and interior-point algorithms for structured convex optimization involving powers and exponentials, PhD thesis, Université catholique de Louvain, 2009.

Motivation

An optimal coupling can exist even when no deterministic transport maps attain its cost. The target separates attainment from equality of infima for a three-marginal repulsive cost. The pinned manuscript supplies the research context.

Setting

All three marginals are the same smooth compactly supported probability density in real three-space, with smooth compactly supported square root. Coincident points have infinite Coulomb cost.

Formalization target

The selected goal is OAI.Problem356.coulomb_counterexample_and_equal_infima. Its central assertion is

$$\inf_{T_2,T_3}\int c(x,T_2x,T_3x)\,d\mu=\min_{\pi\in\Pi(\mu,\mu,\mu)}\int c\,d\pi.$$

The theorem states, without a proof being verified here, that there exists a function ρ on three-dimensional Euclidean space ℝ³ satisfying a full Coulomb conclusion. This means ρ is a nonnegative C^∞ function with compact support, whose square root is also C^∞ with compact support, and with integral 1 over ℝ³; its density measure μ (Lebesgue measure weighted by ρ) is a probability measure. Consider three-marginal couplings of μ, namely probability measures on triples (x,y,z) of points of ℝ³ all of whose three coordinate marginals equal μ, with cost 1/|x−y| + 1/|x−z| + 1/|y−z| valued in [0,∞] (the inverse of distance zero is ∞). The Kantorovich value of μ is the infimum of the expected cost over all such couplings, and the theorem asserts it is finite and attained by some coupling. Further, no pair of measurable maps T₂,T₃ each preserving μ (pushing μ forward to itself) is a Monge optimizer: for every such pair, the expected cost of the triple (x,T₂x,T₃x) under μ is strictly larger than the Kantorovich value. Nevertheless, the Monge value, the infimum of this graph cost over all such pairs of μ-preserving maps, equals the Kantorovich value, and for every ε>0 there are μ-preserving maps T₂,T₃ with finite graph cost at most the Kantorovich value plus ε.

Significance and status

The goal includes a finite attained Kantorovich value, no Monge minimizer, equal infima and arbitrarily accurate finite-cost maps. Other dimensions and Riesz exponents are not part of this selected target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Every measure-preserving pair of maps must be strictly suboptimal, while a sequence of such pairs still approaches the coupling minimum.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, A counterexample to the Monge ansatz for the three-marginal Coulomb cost, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Embedding edit distance into ℓ₁ would permit algorithms and geometric tools for that normed space. Distortion lower bounds quantify the loss any such representation must incur. The source manuscript presents the surrounding research claim.

Setting

Edit distance is the least number of unit insertions, deletions and substitutions, with unrestricted intermediate word lengths. For a finite equal-length binary set W, c₁(W) is the infimum over all injective maps into the full real sequence space ℓ₁ of the product of the two worst distance ratios.

Formalization target

Find an absolute c>0 and d₀ such that for every d≥d₀ there are 1≤n≤d and at least two binary words of length n with

$$c_1(W)\ge\exp\!\left(c\sqrt{\log d\,\log\log d}\right).$$

The selected formal target is OAI.TreeEdit.binary_lower_bound.

Significance and status

The witness exists for every sufficiently large length cap. The target bounds distortion against every injective ℓ₁ embedding, not only a particular algorithm. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A bad map is not a lower bound for the infimum over all maps. The finite family must force distortion uniformly while preserving its common binary word length.

Formalization scope

The chosen target uses Word Bool n and Finset witnesses. A companion binary_torus formulation is retained as a reference to the same lower-bound endpoint. Its independent source group repeats edit-distance declarations and is not combined into one import. No companion upper embedding theorem is attached.

Selected references

• OpenAI, Tree Constructions for the l1 Distortion of Binary Edit Distance, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation: the fixed point property in reflexive spaces

A map $F$ is nonexpansive if $\|F(a)-F(b)\|\le\|a-b\|$. Unlike strict contractions, nonexpansive maps need not have fixed points: on a bounded set, existence depends on the geometry of the norm. A Banach space has the fixed point property (FPP) if every nonexpansive self-map of every nonempty closed bounded convex subset has a fixed point. Since the mid-1960s, whether every reflexive Banach space has the FPP in its given norm has been one of the central open questions of metric fixed point theory. Many sufficient geometric conditions are known, but none of them covers all reflexive spaces. In fixed point theory, the question has been listed as unresolved as recently as 2026 (Nourouzi 2026).

Timeline

• 1965 — Browder and Göhde prove the FPP for uniformly convex spaces (Browder 1965; Göhde 1965). Kirk proves it for weakly compact convex sets with normal structure, in particular for closed bounded convex sets with normal structure in reflexive spaces (Kirk 1965).
• 1974–1975 — Bruck's common fixed point theorems for commuting families and compact convex semigroups (Bruck 1974; Bruck 1975).
• 1975–1976 — The Goebel–Karlovitz lemma on approximate fixed point sequences in minimal invariant sets (Goebel 1975; Karlovitz 1976). Karlovitz also shows that a norm on $\ell_2$ without normal structure still has the FPP, so normal structure is not necessary.
• 1981 — Alspach constructs a weakly compact convex subset of $L_1[0,1]$ with a fixed-point-free nonexpansive self-map, so weak compactness alone is insufficient in general Banach spaces (Alspach 1981). Maurey proves the FPP for reflexive subspaces of $L^1$ (Maurey 1981).
• 1985 — Lin proves the weak FPP for spaces with a $1$-unconditional basis (Lin 1985).
• 2006 — García-Falset, Llorens-Fuster and Mazcuñán-Navarro prove the FPP for uniformly nonsquare spaces (JFA 2006); another proof is due to Dowling, Randrianantoanina and Turett (JFA 2008).
• 2009 — Domínguez Benavides shows that every reflexive space admits an equivalent norm with the FPP (JMAA 2009). Changing the norm changes which maps are nonexpansive, so this does not settle the question for the original norm.
• 2019, 2021 — Hanebaly proposes proofs of the original-norm assertion (JP J. Fixed Point Theory Appl. 2019; preprint 2021). Later literature, such as Nourouzi (2026), still treats the question as unresolved.
• 2026 — An OpenAI preprint, Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces (OpenAI Math Release, September 24, 2026), claims a proof for every real reflexive Banach space. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Let $X$ be a real Banach space and $X^{**}$ its continuous bidual. The canonical map $J:X\to X^{**}$, $J(x)(\varphi)=\varphi(x)$, is always a linear isometry, and $X$ is reflexive if $J$ is surjective. A subset $C\subseteq X$ is taken nonempty, closed in the norm topology, bounded and convex. A map $F:C\to C$ is nonexpansive in the given norm of $X$, and a fixed point is a point $a\in C$ with $F(a)=a$.

In Lean, reflexivity is the definition CanonicallyReflexive X, which says that NormedSpace.inclusionInDoubleDual ℝ X is surjective.

Formalization targets

Goal: reflexive spaces have the fixed point property (Theorem 1.1)

$$X \text{ real reflexive Banach},\ C\subseteq X \text{ nonempty, closed, bounded, convex},\ \|F(a)-F(b)\|\le\|a-b\|\ \ \forall a,b\in C \ \Longrightarrow\ \exists\, a\in C:\ F(a)=a.$$

This is exactly Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem answers the reflexive-space fixed point problem for the given norm, with no extra geometric assumption (uniform convexity, normal structure, unconditional bases, uniform nonsquareness). With Bruck's 1974 theorem it gives the source's Corollary 1.2: for every commuting family of nonexpansive self-maps of $C$, the common fixed point set is nonempty and is a nonexpansive retract of $C$. Alspach's example shows that reflexivity cannot be weakened to weak compactness of $C$ in an arbitrary Banach space.

Formalizing it. Earlier proposed proofs of the same assertion exist, and the literature has not reached a consensus, so a machine-checked proof would give unusual certainty on a disputed question. The proof relies on the minimal invariant set reduction (Zorn's lemma and weak compactness), the Goebel–Karlovitz lemma, compact semigroups of nonexpansive maps (an Ellis-type idempotent), and a tree construction with weighted telescoping estimates. Mathlib has the bidual, the weak topology, and Banach–Alaoglu, but most of the fixed-point-theoretic layer has to be built.

Difficulty

The classical route reduces a hypothetical counterexample to a minimal invariant weakly compact convex set $K$ of diameter one. By the Goebel–Karlovitz lemma, every approximate fixed point sequence in $K$ is asymptotically diametral. Normal-structure arguments then find a point whose radius is strictly below the diameter. In a general reflexive space there is no such geometric gain, and Karlovitz's example shows that normal structure is not necessary for the conclusion. Alspach's $L_1$ example shows that compactness of $C$ and nonexpansiveness alone cannot produce the contradiction: the proof has to use reflexivity of the whole space (weak compactness of the unit ball of $\overline{\operatorname{span}}(K-K)$), not just of the domain. A further obstacle is that $F$ is nonlinear, so convex combinations of approximate fixed points are not mapped to convex combinations of their images.

Formalization scope

• $X$ is any real normed space with CompleteSpace X, and reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual ℝ X (the continuous bidual). Completeness also follows from reflexivity, so including it is harmless. The scalar field is $\mathbb R$; complex spaces enter as real spaces.
• $C$ is a Set X with Nonempty, IsClosed (norm topology), Bornology.IsBounded and Convex ℝ. $F$ is a function on the subtype C → C, and nonexpansiveness is stated in the original norm of $X$, not in an equivalent norm.
• The conclusion is the existence of a fixed point ∃ a : C, F a = a. Every hypothesis is satisfiable, so the statement is not vacuous: a trivial $C$ is excluded only by nonemptiness, as in the source.
• Infrastructure needed: the minimal invariant set reduction, the Goebel–Karlovitz lemma, compact right-topological semigroups of maps and idempotents (Ellis), and weak compactness in reflexive spaces. These would serve other fixed-point formalizations, for example Kirk's and Browder–Göhde's theorems, which are not formalized in Mathlib.

Selected references

• F. E. Browder, Nonexpansive nonlinear operators in a Banach space, Proc. Natl. Acad. Sci. USA 54 (1965), 1041–1044. https://doi.org/10.1073/pnas.54.4.1041
• D. Göhde, Zum Prinzip der kontraktiven Abbildung, Math. Nachr. 30 (1965), 251–258. https://doi.org/10.1002/mana.19650300312
• W. A. Kirk, A fixed point theorem for mappings which do not increase distances, Amer. Math. Monthly 72 (1965), 1004–1006. https://doi.org/10.2307/2313345
• R. E. Bruck, Jr., A common fixed point theorem for a commuting family of nonexpansive mappings, Pacific J. Math. 53 (1974), 59–71. https://msp.org/pjm/1974/53-1/pjm-v53-n1-p05-p.pdf
• K. Goebel, On the structure of minimal invariant sets for nonexpansive mappings, Ann. Univ. Mariae Curie-Skłodowska Sect. A 29 (1975), 73–77. https://www.bc.umcs.pl/Content/31033/PDF/czas4050_29_1975_9.pdf
• L. A. Karlovitz, Existence of fixed points of nonexpansive mappings in a space without normal structure, Pacific J. Math. 66 (1976), 153–159. https://doi.org/10.2140/pjm.1976.66.153
• D. E. Alspach, A fixed point free nonexpansive map, Proc. Amer. Math. Soc. 82 (1981), 423–424. https://doi.org/10.2307/2043954
• B. Maurey, Points fixes des contractions de certains faiblement compacts de $L^1$, Séminaire d'analyse fonctionnelle (1980–1981), Exposé VIII. https://www.numdam.org/item/SAF_1980-1981____A8_0/
• P.-K. Lin, Unconditional bases and fixed points of nonexpansive mappings, Pacific J. Math. 116 (1985), 69–76. https://doi.org/10.2140/pjm.1985.116.69
• J. García-Falset, E. Llorens-Fuster and E. M. Mazcuñán-Navarro, Uniformly nonsquare Banach spaces have the fixed point property for nonexpansive mappings, J. Funct. Anal. 233 (2006), 494–514. https://doi.org/10.1016/j.jfa.2005.09.002
• T. Domínguez Benavides, A renorming of some nonseparable Banach spaces with the Fixed Point Property, J. Math. Anal. Appl. 350 (2009), 525–530. https://doi.org/10.1016/j.jmaa.2008.02.049
• K. Nourouzi, Reflexivity of Hilbert $K(H)$-modules and fixed-point property for nonexpansive mappings, J. Math. 2026, Article ID 6311273. https://doi.org/10.1155/jom/6311273
• OpenAI, Fixed Points of Nonexpansive Maps in Reflexive Banach Spaces, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Fixed-Points-of-Nonexpansive-Maps-in-Reflexive-Banach-Spaces-September-24-2026/paper.pdf

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for all bounded operators on complex Hilbert spaces, with its sharpness, as stated in Corollary 6.3 of an OpenAI preprint dated September 23, 2026 (source), together with the preprint's structural theorems as milestones. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

For a bounded operator $A$ on a complex Hilbert space $\mathcal H\neq\{0\}$, $W(A)=\{\langle x,Ax\rangle:\|x\|=1\}$ and $K=\overline{W(A)}$; $P[A]=\sum_kA^k\otimes B_k$ acts on $\mathcal H\otimes\mathbb C^m$. A bounded open convex $\Omega\subset\mathbb C$ is admissible if its boundary is a regular real-analytic Jordan curve. For such $\Omega\supset W(A)$ ($A$ a matrix) with interior conformal map $f:\Omega\to\mathbb D$, put $T=f(A)$ and

$$\kappa^2=\min\{\tau:\ I\preceq H\preceq\tau I,\ T^*HT\preceq H\ \text{for some } H=H^*\}.$$

Formalization targets

Milestone: geometry of the numerical range (Corollary 6.3, p. 16, first assertion)

For $\mathcal H\neq\{0\}$, $K=\overline{W(A)}$ is compact and convex and contains $\operatorname{spec}(A)$.

Milestone: the zero space (Corollary 6.3, p. 16, case $\mathcal H=\{0\}$)

If $\mathcal H=\{0\}$, the numerical range is empty, every polynomial, holomorphic and rational evaluation is $0$, and the corresponding inequalities read $0\le0$ (with the supremum over the empty set taken to be $0$).

Milestone: optimal metric and common positive representation (Lemma 1.1, Theorems 1.2–1.3, p. 2)

For admissible $\Omega$ conformal coordinates exist; for every $n\ge1$ and $A\in M_n(\mathbb C)$ with $W(A)\subset\Omega$, the problem defining $\kappa^2$ is strictly feasible with attained minimum $1\le\kappa^2\le4$; for a minimizer $H$, $S=H^{1/2}$ satisfies $\|S\|\|S^{-1}\|=\kappa\le2$ and $D=Sf(A)S^{-1}$ is a contraction with $\rho(D)<1$; and one continuous $\Lambda:\mathbb T\to M_n(\mathbb C)$ with $\Lambda\succeq0$, $\int\Lambda\,d\sigma=I$ represents $v[SAS^{-1}]=\int\Lambda(t)\otimes v(G(t))\,d\sigma(t)$ for every $m$ and every $M_m$-valued $v$ holomorphic near $\overline\Omega$, giving $\|v[A]\|\le\kappa\max_{\overline\Omega}\|v\|$.

Milestone: the matrix inequality (Corollary 6.1, p. 15)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$, $B_k\in M_m(\mathbb C)$: $\|P[A]\|\le2\max_{W(A)}\|P\|$, and no smaller universal constant works.

Goal: Corollary 6.3 (p. 16)

For every complex Hilbert space $\mathcal H$ (no separability assumption) and $A\in B(\mathcal H)$: if $\mathcal H\neq\{0\}$ then $K$ is compact, convex, contains the spectrum, and for every $m\ge1$

$$\|P[A]\|\le 2\sup_{W(A)}\|P\|=2\max_K\|P\|,\qquad \|F[A]\|\le2\max_K\|F\|,\qquad \|R[A]\|\le 2\max_K\|R\|$$

for matrix polynomials $P$, matrix functions $F$ holomorphic on an open $U\supseteq K$ (holomorphic functional calculus), and matrix rational functions $R$ with poles off $K$; if $\mathcal H=\{0\}$ the degenerate statements above hold; and the constant $2$ is optimal.

Significance

The result itself. It resolves the complete Crouzeix conjecture in its operator formulation, independent of the Hilbert space, the coefficient size and the degree: $\overline{W(A)}$ is a complete $2$-spectral set for every bounded operator. The structural theorems give more than the inequality: an optimal similarity, attained, with condition number at most $2$, and one positive boundary density that represents every matrix-valued analytic evaluation simultaneously. These are the objects predicted abstractly by Paulsen's and Arveson's theorems, constructed here explicitly. A companion OpenAI preprint gives an independent direct proof of the matrix inequality.

Formalizing it. Mathlib has bounded operators, the holomorphic functional calculus is only partially available, and conformal mapping of analytic Jordan domains is absent. A complete development needs the Riemann mapping theorem with boundary extension, semidefinite optimization over Hermitian matrices, Haar integration on the circle, and a finite-compression argument for nonseparable spaces.

Difficulty

Two obstacles stand out. First, the passage from the scalar to the complete inequality: scalar proofs exploit commutativity that fails for matrix coefficients, so a structure valid for every coefficient size at once is needed; here it is the optimal metric chosen before any test function. Proving $\kappa\le2$ for that metric requires an endpoint extremal pair (Proposition 2.2, p. 6) and an ordered density comparison (Lemma 5.1, p. 14). Second, the passage from matrices to arbitrary operators: the numerical range of a compression lies in $W(A)$, but one must show every vector of $\mathcal H\otimes\mathbb C^m$ and its image under $P[A]$ live in a finite-dimensional compression, and treat holomorphic and rational calculi through contour integrals around the closed numerical range.

Formalization scope

• H is any type with InnerProductSpace ℂ H and CompleteSpace H; operators are H →L[ℂ] H. The amplification $\mathcal H\otimes\mathbb C^m$ is the completion of the algebraic tensor product, and $A^k\otimes B_k$ is the completed TensorProduct.mapL.
• supNorm S F = sSup (insert 0 (‖F ·‖ '' S)), so the supremum over an empty set is $0$, matching the convention of Corollary 6.3.
• Holomorphic evaluation is defined by a contour integral over a CalculusContour around $K$ inside $U$; the goal asserts such contours exist and that the evaluation is contour-independent. Rational evaluation inverts aeval A denom; the goal asserts these denominators are units and that the rational evaluation agrees with the holomorphic one.
• SharpConstant is witnessed by a $2\times2$ matrix with $\sup_{W}|P|=1$ and $\|P[A]\|=2$.
• The structural milestone also includes, as an extra conjunct, that the open unit disk is admissible.

Two further published supporting statements are included as items but not milestones: existence of a finite-dimensional compression representing a given vector (a step in the proof of Corollary 6.3) and invertibility of rational denominators (the well-definedness part of the rational calculus).

Selected references

• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• V. I. Paulsen, Completely bounded homomorphisms of operator algebras, Proc. Amer. Math. Soc. 92 (1984), 225–228.
• W. Arveson, Subalgebras of C-algebras II*, Acta Math. 128 (1972), 271–308.
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610

Motivation

For a square matrix $A$, the spectrum alone does not control the size of $p(A)$: a nonzero nilpotent matrix has spectrum $\{0\}$ yet $\|A\|>0$. The numerical range $W(A)=\{u^*Au:\ \|u\|=1\}$ is a compact convex set containing the spectrum (Toeplitz–Hausdorff), and it does retain enough information. Crouzeix's conjecture (2004) asserts that for every polynomial $p$,

$$\|p(A)\|\le 2\max_{z\in W(A)}|p(z)|,$$

i.e. that $W(A)$ is a $2$-spectral set; the constant $2$ would be optimal. Such bounds are used to estimate matrix functions in numerical linear algebra (for example GMRES convergence through Faber polynomials) and in operator theory. The complete version asks for the same constant when the polynomial has $m\times m$ matrix coefficients, uniformly in $m$; by Paulsen's theorem this is equivalent to similarity of the conformal disk image of $A$ to a contraction with condition number at most $2$.

Background

• 1918–1919 — Toeplitz and Hausdorff prove convexity of the numerical range (Math. Z. 1918, Math. Z. 1919).
• 1972, 1984 — Arveson's dilation theory (Acta Math. 128, 1972) and Paulsen's similarity theorem (Proc. AMS 92, 1984) relate complete contractivity, dilations and similarity.
• 1999 — Delyon and Delyon's positive integral representations (Bull. SMF 1999).
• 2004 — Crouzeix formulates the constant-two question (IEOT 2004); 2007 — he proves a universal complete bound $11.08$ (JFA 2007).
• 2006 — Badea, Crouzeix and Delyon obtain the complete constant $2$ for $2\times2$ matrices (Math. Z. 2006).
• 2017–2018 — Crouzeix and Palencia prove the complete bound $1+\sqrt2$ (SIMAX 2017); Ransford and Schwenninger simplify the argument (SIMAX 2018).
• 2026 — Scalar ($m=1$) constant-two proofs appear in preprints of Jin, Lorist–Schwenninger (arXiv:2608.03841) and Luo; Åhag, Czyż and Virtanen prove the complete inequality for base matrices of order at most three (arXiv:2608.27346).
• September 2026 — Two OpenAI preprints claim the complete inequality in all dimensions: a structural proof via an optimal similarity and a common positive boundary density, extended to all bounded Hilbert-space operators (source), and a direct coefficient proof for matrices (source).

This mission asks for a formal proof of the complete Crouzeix inequality for matrices, with its sharpness, as stated in Theorem 1.1 of an OpenAI preprint dated September 26, 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.

Setting

For $A\in M_n(\mathbb C)$ ($n\ge1$) let $W(A)=\{u^*Au: u\in\mathbb C^n,\ u^*u=1\}$. A matrix polynomial of degree $d$ with coefficient size $m\ge1$ is $P(z)=\sum_{k=0}^dB_kz^k$ with $B_k\in M_m(\mathbb C)$. Its evaluation at $A$ is

$$P[A]=\sum_{k=0}^d A^k\otimes B_k\ \in M_n(\mathbb C)\otimes M_m(\mathbb C),$$

with the base space first. All norms are Euclidean operator norms. For $m=1$ this is the usual $p(A)$.

Formalization targets

Milestone: the inequality (Theorem 1.1, p. 1, first assertion)

For all $n,m\ge1$, $d\ge0$, $A\in M_n(\mathbb C)$ and $B_0,\dots,B_d\in M_m(\mathbb C)$,

$$\Bigl\|\sum_{k=0}^dA^k\otimes B_k\Bigr\|\ \le\ 2\max_{z\in W(A)}\Bigl\|\sum_{k=0}^dB_kz^k\Bigr\| .$$

Milestone: sharpness (Theorem 1.1, p. 1, second assertion)

If the inequality holds with a constant $c$ in place of $2$ for all $n,m,d,A,B$, then $c\ge2$.

Goal: Theorem 1.1 (p. 1)

Both assertions together: the constant $2$ is valid and no smaller universal constant is.

Significance

The result itself. It settles the complete Crouzeix conjecture in its matrix formulation, uniformly in the base dimension $n$, the coefficient size $m$ and the degree, including matrices whose numerical range is a point or a segment. The scalar case $m=1$ had recently been proved by other authors and the complete case was known only for $n\le3$; a scalar argument need not survive matrix amplification because coefficient matrices do not commute. Equivalently, the numerical range is a complete $2$-spectral set for every matrix, which via Paulsen's theorem gives a similarity of condition number at most $2$ making the conformal disk image of $A$ a contraction. A companion OpenAI preprint gives a separate structural proof and extends the bound to all bounded operators on Hilbert spaces.

Formalizing it. The proof uses exterior conformal maps of analytic convex domains, Faber-type coefficients, a positive double-layer kernel, and a $2\times2$ block positivity argument; Section 4 then approximates an arbitrary numerical range by analytic convex domains. A formal proof would provide numerical ranges, Faber polynomials and conformal collars in Lean, all reusable in matrix analysis. No machine-checked proof of any constant-$2$ Crouzeix bound is known.

Difficulty

The naive approach through the spectrum fails for non-normal matrices, and the classical Crouzeix–Palencia method (a positive double-layer potential plus a Cauchy transform of conjugate data) loses a factor and yields $1+\sqrt2$. To reach $2$ in the complete setting, the argument must keep both multiplication orders $FG$ and $GF$ of matrix-valued test functions, since the coefficients do not commute. The preprint chooses a top singular pair $(x,y)$ of $F[A]$, represents three functionals through the resolvent, and must show that the resulting coefficient weights (one on the constant term, one half on the others) match exactly the Fourier weights of the diagonal compressions (Section 2, Proposition 2.2, p. 5; Theorem 3.2, p. 6). Degenerate numerical ranges with empty interior require a separate approximation step (Lemma 4.1, p. 9).

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℂ with the L2 operator norm (Matrix.Norms.L2Operator). The numerical range is the set of $\langle x, Ax\rangle$ over unit vectors of EuclideanSpace ℂ (Fin n).
• Coefficients are B : Fin (d+1) → Matrix (Fin m) (Fin m) ℂ; the evaluation is $\sum_k A^k\otimes_{\mathrm{Kron}}B_k$ indexed by Fin n × Fin m, base factor first.
• rangeMaximum A B is the sSup of $\|P(z)\|$ over $W(A)$. Since $n\ge1$, $W(A)$ is nonempty and compact, so this is the true maximum; UniversalBound C quantifies over all $n,m\ge1$, all $d$, all $A$ and $B$.
• The goal OAI.CompleteCrouzeix.main is UniversalBound 2 ∧ ∀ C, UniversalBound C → 2 ≤ C. The two milestones state the same two clauses in the DirectCrouzeix namespace, whose definitions are identical in content.
• No normality, invertibility or nonempty-interior hypothesis is imposed on $A$.

Selected references

• OpenAI, A direct proof of the complete Crouzeix inequality, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-direct-proof-of-the-complete-Crouzeix-inequality-September-26-2026/paper.pdf
• OpenAI, The complete Crouzeix theorem: optimal similarity and a common positive boundary representation, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complete-Crouzeix-theorem-September-23-2026/paper.pdf
• M. Crouzeix, Bounds for analytical functions of matrices, Integral Equations Operator Theory 48 (2004), 461–477. https://doi.org/10.1007/s00020-002-1188-6
• M. Crouzeix, Numerical range and functional calculus in Hilbert space, J. Funct. Anal. 244 (2007), 668–690. https://doi.org/10.1016/j.jfa.2006.10.013
• M. Crouzeix, C. Palencia, The numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 38 (2017), 649–655. https://doi.org/10.1137/17M1116672
• T. Ransford, F. L. Schwenninger, Remarks on the Crouzeix–Palencia proof that the numerical range is a $(1+\sqrt2)$-spectral set, SIAM J. Matrix Anal. Appl. 39 (2018), 342–345. https://doi.org/10.1137/17M1143757
• C. Badea, M. Crouzeix, B. Delyon, Convex domains and K-spectral sets, Math. Z. 252 (2006), 345–365. https://doi.org/10.1007/s00209-005-0857-y
• B. Delyon, F. Delyon, Generalization of von Neumann's spectral sets and integral representation of operators, Bull. Soc. Math. France 127 (1999), 25–41. https://doi.org/10.24033/bsmf.2340
• E. Lorist, F. L. Schwenninger, A solution to Crouzeix's conjecture, arXiv:2608.03841 (2026). https://arxiv.org/abs/2608.03841v2
• P. Åhag, R. Czyż, J. Virtanen, The complete Crouzeix conjecture in dimension three and the Clouâtre–Ostermann–Ransford conjecture, arXiv:2608.27346 (2026). https://arxiv.org/abs/2608.27346v4
• O. Toeplitz, Das algebraische Analogon zu einem Satze von Fejér, Math. Z. 2 (1918), 187–197. https://doi.org/10.1007/BF01212904
• F. Hausdorff, Der Wertvorrat einer Bilinearform, Math. Z. 3 (1919), 314–316. https://doi.org/10.1007/BF01292610