Mathematical Physics

Motivation

A local quantum system is built from degrees of freedom placed at sites of a lattice. Its Hamiltonian may contain many terms, each acting on a small group of sites. Even though a term is local, time evolution can spread an observable beyond its original support. A Lieb–Robinson bound limits the size of a commutator between the evolved observable and one supported elsewhere. It gives a quantitative way to say that information propagates with an effective finite velocity. The Appendix C bound of Haah, Hastings, Kothari and Low treats interactions with exponential spatial decay and makes the effect of almost commuting Hamiltonian terms explicit.

The paper studies quantum simulation, where a system's real time evolution is approximated by a circuit. Lemma 12 is an analytic ingredient: it controls how far a local observable can spread during the simulated evolution. The mission targets that lemma and the displayed estimates in its proof, with the constants printed in the pinned arXiv version. The paper proves the results; the remaining task here is to give the stated finite system version machine checked proofs.

Setting

Let $\Lambda$ be a finite set of sites equipped with a metric $\operatorname{dist}(x,y)$. Each site has the same local Hilbert space $\mathbb C^q$, and the whole system has product basis indexed by configurations $\sigma:\Lambda\to\{0,\ldots,q-1\}$. An operator supported on $X\subseteq\Lambda$ is a matrix of the form $m_X\otimes I_{\Lambda\setminus X}$: it may change the configuration on $X$, but acts as the identity on every site outside $X$. The matrix norm throughout is the spectral operator norm.

For every $X\subseteq\Lambda$, let $h_X$ be a Hermitian operator supported on $X$, and define the time independent Hamiltonian $H=\sum_{X\subseteq\Lambda}h_X$. The sum includes all subsets, including the empty set. Let

$$O(t;J)=e^{iJt}Oe^{-iJt},\qquad O(t)=O(t;H).$$

For site sets, write $X\sim Y$ when $X\cap Y\ne\varnothing$, and $\operatorname{dist}(x,Y)=\min_{y\in Y}\operatorname{dist}(x,y)$ when $Y$ is nonempty. The diameter is $\operatorname{diam}(X)=\max_{x,y\in X}\operatorname{dist}(x,y)$ for nonempty $X$. The paper imposes two quantitative conditions. First, for some $0\le\eta\le1$, every pair of terms has a small commutator:

$$\|[h_X,h_Y]\|\le 2\eta\|h_X\|\|h_Y\|.\tag{14}$$

Second, for some $\zeta,\mu>0$, the interactions decay in the weighted sense

$$\sum_{X\ni x}\|h_X\|\,|X|^2e^{\mu\operatorname{diam}(X)}\le\zeta \qquad(x\in\Lambda).\tag{15}$$

Neither condition bounds each $\|h_X\|$ by one. This matters because the result is meant to include large but nearly commuting terms. These conventions are from Appendix C.1 of the source.

Formalization targets

The goal is Lemma 12. For an operator $A$ supported on $X$ and an operator $B$ supported on a disjoint set $Y$, and every real $t$, the proposed formal statement is

$$\|[A(t),B]\|\le \frac{2}{\sqrt\eta}\|A\|\|B\| \bigl(e^{\zeta|t|\sqrt{8\eta}}-1\bigr) \sum_{x\in X}e^{-\mu\operatorname{dist}(x,Y)}. \tag{16}$$

The coefficient of $|t|$ in the exponential is proportional to $\sqrt\eta$. The goal keeps the paper's explicit factor $2/\sqrt\eta$, its $\sqrt{8\eta}$ inside the exponential, and the full sum over sites in $X$. The statement is for $\eta>0$, as the displayed formula is undefined at $\eta=0$; a family satisfying (14) with $\eta=0$ also satisfies it for any positive $\eta\le1$.

The milestones follow the source's numbered displays: the initial estimates for $C_B$ and $D_B$ in (28), their integral inequalities (24) and (27), the linked set series (32), the four estimates of Proposition 13, and the bound on its $k$th line in (37). Here $C_B(X,t)$ takes a supremum over supported operators of norm at most one, and $D_B(X,t)=\|[h_X(t),B]\|$. The milestone list is a map of the quantities that the proof controls, while the goal itself mentions only the physical operators and the two hypotheses.

Significance

The bound shows that a commutator is small when the support of $B$ is far from $X$, with a rate determined by the decay parameter $\mu$ and the small commutator parameter $\eta$. It applies to finite systems of any size with the same constants in (14) and (15). This makes it useful for reasoning about local approximations of time evolution in the quantum simulation setting of the paper. The authors also explain why a velocity proportional to $\sqrt\eta$ can occur under their hypotheses, so a linear dependence on $\eta$ is not generally available. See the discussion immediately after Lemma 12 in Appendix C.1.

Formalizing the result would supply a reusable finite matrix model of local observables and a checked version of the analytic estimates for near commuting interactions. The source paper provides a proof, but this proposed statement and its milestones currently have no machine checked proof in the mission. The definitions of support, Heisenberg evolution and linked interactions may also be reused in later formalizations of quantum lattice dynamics.

Difficulty

The obvious global norm bound $\|[A(t),B]\|\le2\|A\|\|B\|$ ignores the distance between supports. Merely bounding $\|H\|$ also loses spatial information and can grow with the whole system. The sharper statement simultaneously tracks where an interaction overlaps the current support and how the small commutator factor enters repeated interactions. A rigorous treatment must control a supremum over local operators, time dependent matrix exponentials, and an infinite series of finite linked set sums without changing any of the paper's constants.

Formalization scope

Sites form an arbitrary finite metric space, a disclosed generalization of the lattice setting used for the main algorithm. A common local dimension $q$ is used at every site; qubits occur at $q=2$. Operators are complex matrices on the configuration space $\Lambda\to\operatorname{Fin}(q)$, with Mathlib's scoped L2 operator norm. Every term is Hermitian and explicitly supported on its stated set, and $H$ is the sum over all subsets. Time is real and $H$ is constant in time. The paper mentions a piecewise continuous time dependent extension, which this mission does not state.

The goal explicitly requires $X\cap Y=\varnothing$. The printed sentence of Lemma 12 omits this, but its derivation on page 24 assumes it; without disjointness the right side is zero at $t=0$ while the left side need not be. The positive $\eta$ condition is likewise explicit. These are the two repairs to the printed lemma, and they are recorded on each relevant item. The milestones (24) and (27) are restricted to $t\ge0$, the direction for which the displayed forward integral uses $D_B(Z,s)$ and $C_B(Z\cup X,s)$.

For an empty set, the Lean point to set distance and the local set distance are taken to be zero; a supported operator on the empty set is a scalar, so its commutators vanish. $C_B$ uses a real supremum of a nonempty, bounded set, and (32) states an actual sum with HasSum. The integral milestones involve continuous finite dimensional evolution. The support definition includes nonconstant single site operators, and the $q=2$ case is part of the goal. These choices prevent the result from being obtained through a vacuous support predicate, an entrywise norm, division by zero at $\eta=0$, a default value of an unbounded supremum or divergent sum, or omitted disjointness. Contributions that establish the support calculus, matrix evolution estimates, integral inequalities, or linked set bounds are all within scope.

Selected references

• Jeongwan Haah, Matthew B. Hastings, Robin Kothari and Guang Hao Low, Quantum algorithm for simulating real time evolution of lattice Hamiltonians, SIAM Journal on Computing, 2021. arXiv:1801.03922v4, Appendix C.1–C.3, pp. 21–25.

Motivation

The two-dimensional directed polymer is a random walk whose paths are reweighted by a random space-time environment. Its logarithmic partition function is a discrete counterpart of the height field of the two-dimensional Kardar–Parisi–Zhang equation. At the intermediate-disorder scale, the random weighting becomes weaker as the walk grows, yet its fluctuations remain visible. Caravenna, Sun and Zygouras prove that throughout the subcritical regime $0<\hat\beta<1$, spatial averages of the centred log-partition function converge to Gaussian fluctuations described by an additive stochastic heat equation (Theorem 1.6, p. 6).

The polymer formulation matters because it is a concrete finite-path model: each partition function is an average over finitely many nearest-neighbour walks, while its limit retains the effect of disorder at every scale. The same paper treats the continuum KPZ equation separately; this mission takes its stated polymer theorem as the target. Earlier work in dimension $1+1$ studied a different intermediate-disorder scaling and a Wiener-chaos limit (Alberts, Khanin and Quastel, 2014). The two-dimensional result concerns a distinct regime and a different limit.

Setting

Let $S$ be the simple symmetric random walk on $\mathbb Z^2$. Starting at $x$, it chooses each of its four nearest-neighbour steps with probability $1/4$. Write $q_n(z)=P_0(S_n=z)$, and let $\widetilde S$ be an independent copy. Their expected overlap through time $N$ is

$$R_N=\sum_{n=1}^N P(S_n=\widetilde S_n)=\sum_{n=1}^N\sum_{z\in\mathbb Z^2}q_n(z)^2.$$

For a fixed $\hat\beta\in(0,1)$, the disorder strength is $\beta_N=\hat\beta/\sqrt{R_N}$. The environment $\omega(n,z)$ consists of independent, identically distributed real random variables with mean zero, variance one and finite exponential moments at all sufficiently small positive arguments. Its logarithmic moment generating function is $\lambda(b)=\log\mathbb E[e^{b\omega}]$. The law also obeys the paper's concentration assumption (1.20): convex 1-Lipschitz functions of any finite collection of environment variables have stretched-exponential deviations from a median, measured with Euclidean distance (pp. 5–6).

For a length-$N$ walk from $x$, sum $\beta_N\omega(n,S_n)-\lambda(\beta_N)$ over times $1,\ldots,N$, exponentiate, and average over paths. The result is the partition function $Z_N(x)$. Where $\lambda(\beta_N)$ is finite, its centring gives $\mathbb E Z_N(x)=1$. A restricted function $Z_{\Lambda,b}(x)$ samples disorder only from the space-time sites in $\Lambda$. Section 2 uses an early window $A_N^x$ near the start and a late window $B_N^{\ge}$ to define $Z_N^A(x)$, its remainder $\widehat Z_N^A(x)=Z_N(x)-Z_N^A(x)$, and $Z_N^{B\ge}(x)$ (pp. 7–9).

At macroscopic time $t>0$ and position $y\in\mathbb R^2$, the fluctuation field is

$$\mathfrak h_N(t,y)=\frac{\log Z_{\lfloor tN\rfloor}(\lfloor\sqrt N y\rfloor)-\mathbb E[\log Z_{\lfloor tN\rfloor}(0)]}{\beta_N}.$$

The floor of a vector is componentwise. In the numerator, $Z_{\lfloor tN\rfloor}$ uses the disorder strength $\beta_{\lfloor tN\rfloor}$; the field is divided by $\beta_N$, exactly as in (1.23).

Formalization targets

For every $t>0$ and smooth compactly supported test function $\phi$, Theorem 1.6 asserts

$$\int_{\mathbb R^2}\mathfrak h_N(t,y)\phi(y)\,dy\xrightarrow{d}\langle v^{(\sqrt2c_{\hat\beta})}(t/2,\cdot),\phi\rangle,\qquad c_{\hat\beta}=\sqrt{\frac1{1-\hat\beta^2}}.$$

The tested limit is centred Gaussian. Its variance is $(\sqrt2c_{\hat\beta})^2\sigma_\phi^2(t/2)$, where

$$\sigma_\phi^2(s)=\iint\phi(x)K_s(x,y)\phi(y)\,dx\,dy,\qquad K_s(x,y)=\int_0^s\frac{e^{-|x-y|^2/(4u)}}{4\pi u}\,du.$$

The milestone list follows the paper's stated results: second-moment bounds (3.2)–(3.4), higher moments for some $p>2$ (3.12), a left-tail bound (Proposition 3.1) and the negative and logarithmic moments it yields (3.14)–(3.16), vanishing spatial averages for two error terms (Propositions 2.1–2.2), replacement by the late-window term (Proposition 2.3), and the Gaussian limit for that term (Proposition 2.4). These are the exact result labels used in Sections 2 and 3 (pp. 8–13).

Significance

The theorem identifies the fluctuation law of the logarithm of the polymer partition function for every $\hat\beta$ strictly below the critical value $1$. The coefficient $c_{\hat\beta}$ records the disorder strength in the limiting covariance, and the time $t/2$ reflects the two-dimensional walk's covariance convention. Without the spatial averaging and normalization, the statement would concern a different observable; the theorem characterizes a field tested against compactly supported functions (Theorem 1.6 and Remark 1.7).

The result is proved in the cited paper. This mission asks for a machine-checked proof of that known result and its curated supporting statements. The reusable output includes a finite-path polymer model on $\mathbb Z^2$, a precise restricted partition function, the disorder concentration assumption, and the Gaussian covariance functional. The published atomic polymer model already supplies the space-time cells, steps, walk positions and log moment generating function; this mission extends that common base to the centred, spatially shifted model of this paper.

Difficulty

Pointwise size does not identify the limiting spatial fluctuations. The early-window partition function captures much of $Z_N(x)$ at a fixed site, yet its averaged logarithm vanishes at the target scale. The small remainder cannot simply be discarded: after division by the early-window function, its late-time component carries the Gaussian limit. The paper separates these effects in Propositions 2.1–2.4 and needs moment and left-tail control to keep the logarithmic expression meaningful (Sections 2–4). A direct Taylor expansion of $\log Z_N$ around its mean would lose this distinction.

Formalization scope

Lean uses finite sequences of four-neighbour steps and the Euclidean norm on $\mathbb R^2$. Disorder is a family indexed by positive walk times and lattice sites; the time-zero row of its ambient type is unused. The full and restricted partition functions are finite walk averages. The concentration assumption quantifies over Euclidean 1-Lipschitz convex functions and their medians. The test class of Theorem 1.6 is $C_c^\infty(\mathbb R^2)$; the four Section 2 propositions use $C_c(\mathbb R^2)$. Treating “smooth” as analytic would make compactly supported tests trivial, so the Lean statement uses the smooth differentiability order.

The target additive stochastic heat observable is represented by its Gaussian law and the kernel above; the random field $v^{(c)}$ itself is not formalized, and the statement does not need it. The kernel takes extended nonnegative values because it is infinite on the diagonal; the diagonal has zero area in the tested covariance integral. Moments and $L^1/L^2$ convergence use extended nonnegative integrals. The paper assumes exponential moments only near zero, so bounds whose printed form quantifies over every $N$ are stated for all sufficiently large $N$, avoiding default values of the logarithmic moment generating function at early indices. The spatial sums have finite support because the test functions do. Replacing the Euclidean norm by the sup norm would change the early window (a square instead of a disc), the kernel and the class of 1-Lipschitz functions in (1.20), so all of these are Euclidean. The polymer propositions are stated for every window exponent below a threshold, as in (2.2), and the passage from the time-1 lattice averages of Propositions 2.1–2.4 to the general-time integral of Theorem 1.6 is part of the proof work, not of the statements. Contributions to the polymer moments, left-tail estimate, replacement propositions and Gaussian limit all feed the stated goal.

Selected references

• Francesco Caravenna, Rongfeng Sun and Nikos Zygouras, The two-dimensional KPZ equation in the entire subcritical regime, Annals of Probability 48(3), 2020; formalization source: arXiv:1812.03911v3.
• Tom Alberts, Konstantin Khanin and Jeremy Quastel, The intermediate disorder regime for directed polymers in dimension 1+1, Annals of Probability 42(3), 2014, DOI:10.1214/13-AOP895.

Motivation

A directed polymer in random environment is a random walk path reweighted by a random potential that is refreshed at every time step. It is a basic model of a one-dimensional object (a polymer, an interface, a flux line) pinned by impurities, and a discrete version of the KPZ universality class in dimension $1+1$. A central question is localization: whether the walk's endpoint at time $n$, under the random Gibbs measure, concentrates on a few sites or spreads out like a simple random walk.

For a fixed disorder law there is a critical inverse temperature $\beta_c$ (Comets–Yoshida, Ann. Probab. 2006). In the low-temperature phase $\beta>\beta_c$ the endpoint has atoms of positive mass, in the Cesàro sense, at a positive fraction of times (Carmona–Hu 2002, Comets–Shiga–Yoshida 2003); in the high-temperature phase it does not. Atoms alone say nothing about geometry: the mass could sit on a few sites that are far apart. Bates and Chatterjee (arXiv:1612.03443v5, Ann. Probab. 2020) prove that in the low-temperature phase the mass also sits on a region of bounded diameter at a positive fraction of times, in every dimension and for every disorder law with exponential moments. Before this, geometric localization was known only for the integrable log-gamma polymer in $1+1$ dimensions (Comets–Nguyen 2016).

Setting

Fix $d\ge1$. Let $(X_u)_{u\in\mathbb N\times\mathbb Z^d}$ be i.i.d. real random variables with law $\mathfrak L$, not supported on a single point, such that $\lambda(\alpha)=\log\mathbf E\,e^{\alpha X_u}<\infty$ for $\alpha\in[-2\beta,2\beta]$ (assumption (1.1)), where $\beta\ge0$ is the inverse temperature. For a nearest-neighbour path $\gamma$ of length $n$ from the origin, its weight is $\exp(\beta\sum_{i=1}^n X_{i,\gamma(i)})$. The endpoint distribution $f_n(x)=\rho_n(\omega_n=x)$ is the total weight of paths ending at $x$ divided by the total weight of all $(2d)^n$ paths. The partition function is $Z_n=(2d)^{-n}\sum_\gamma\exp(\beta\sum_{i=1}^nX_{i,\gamma(i)})$ and the free energy is $F_n=\frac1n\log Z_n$. The limit $p(\beta)=\lim\mathbf E F_n$ exists, and $\beta_c$ is characterised by $p(\beta)=\lambda(\beta)$ for $0\le\beta\le\beta_c$ and $p(\beta)<\lambda(\beta)$ for $\beta>\beta_c$.

For $\delta>0$ and $K\ge0$ let $\mathcal G_{\delta,K}$ be the set of probability mass functions on $\mathbb Z^d$ that give mass greater than $1-\delta$ to some set $D$ with $\operatorname{diam}(D)=\sup_{x,y\in D}\|x-y\|_1\le K$.

The proofs work on the space $\mathcal S$ of partitioned subprobability measures: functions $f\ge0$ on $\mathbb N\times\mathbb Z^d$ with $\sum f\le1$, modulo translations of each copy of $\mathbb Z^d$, with a metric $d$ that makes $\mathcal S$ compact. The update $f_n\mapsto f_{n+1}$ induces a Markov kernel $\mathcal T$ on $\mathcal S$; $\mathcal K$ is its set of invariant probability measures and $\mathcal M\subset\mathcal K$ the minimisers of a free-energy functional $\mathcal R$. On $\mathcal S$ the mission uses the functionals $\max(f)=\max_uf(u)$, the support number $N(f)$ (number of copies carrying mass), $W_\delta(f)$ (the least diameter of a region of one copy with mass $>1-\delta$), $m(f)=\max_nq_n(f)$ and $Q(f)=\sum_nq_n(f)/(1-q_n(f))$, where $q_n(f)$ is the mass of copy $n$.

Formalization targets

Goal: Theorem 1.2 (= Theorem 7.3(a),(c))

If $\beta>\beta_c$, then for every $\delta>0$ there are $K<\infty$ and $\theta>0$, depending only on $\delta,\mathfrak L,\beta,d$, such that

$$\liminf_{n\to\infty}\frac1n\sum_{i=0}^{n-1}\mathbb 1_{\{f_i\in\mathcal G_{\delta,K}\}}\ge\theta\quad\text{a.s.}$$

If $0\le\beta\le\beta_c$, then for every $K$ and every $\delta\in(0,1)$,

$$\lim_{n\to\infty}\frac1n\sum_{i=0}^{n-1}\mathbb 1_{\{f_i\in\mathcal G_{\delta,K}\}}=0\quad\text{a.s.}$$

The goal fixes no constants: $K$ and $\theta$ are only asserted to exist.

Milestones

1. Lemma 5.4: $\max$ is continuous on $\mathcal S$.
2. Theorem 5.3: the Cesàro average of $\max_xf_i(x)$ tends to $0$ a.s. at high temperature and has $\liminf\ge c>0$ a.s. at low temperature.
3. Lemma 7.1: $W_\delta$ is upper semicontinuous; $m$ and $Q$ are lower semicontinuous.
4. Lemma 7.2: at low temperature $\int Q\,d\nu=\infty$ for every $\nu\in\mathcal M$.
5. Theorem 7.3(b): under the single-copy condition $\nu(N=1)=1$ for all $\nu\in\mathcal M$ (7.4), localization holds with full density $\theta\ge1-\delta$.
6. Proposition 7.4: under (7.4), $\lim_{K\to\infty}\liminf_n\frac1n\sum_{i<n}\rho_i(\omega_i\in\mathcal C_i^K)=1$ a.s., where $\mathcal C_i^K$ is the set of sites within distance $K$ of every mode of $f_i$.

Significance

The theorem shows that the low-temperature phase is detected by the shape of the endpoint distribution, not only by its largest atom: positive-density geometric localization holds if and only if $\beta>\beta_c$. The determinism of $K$ and $\theta$ makes the statement uniform over all environments with the given law. The conditional results 5 and 6 reduce full-density and favourite-region localization to a single property of the limit set $\mathcal M$, which is open.

The result is proved on paper; nothing in it is machine-checked. A formalization would produce a checked development of the compact space $\mathcal S$, of the Markov kernel $\mathcal T$, and of the variational characterisation of the free energy, which also underlies the companion mission on asymptotic pure atomicity of the same paper.

Difficulty

The obvious approach, tracking $f_n$ in $\ell^1(\mathbb Z^d)$, fails because mass escapes to infinity: the sequence $(f_n)$ has no convergent subsequence in any space of probability measures on $\mathbb Z^d$. The paper's compactification keeps pieces of mass that drift apart as separate copies, so a limit point can split one copy's mass over several. The semicontinuity of $W_\delta$, $m$ and $Q$ (Lemma 7.1) only goes one way for this reason, and positivity of the localized fraction needs the separate identity of Lemma 7.2, which uses strict convexity and the non-degeneracy of $\mathfrak L$. Theorem 5.3 already requires the full variational machinery of §4 (convergence of empirical measures to $\mathcal M$), which is the companion mission's subject.

Formalization scope

Points are $\mathbb Z^d=$ Fin d → ℤ, cells are ℕ × (Fin d → ℤ), and paths are sequences of $n$ signed coordinate steps. The environment is a family of independent measurable random variables, each with law $\mathfrak L$, on an arbitrary probability space. The phases are encoded through Theorem A as $\lim\mathbf E F_n<\lambda(\beta)$ ($\beta>\beta_c$) and $\lim\mathbf EF_n=\lambda(\beta)$ ($0\le\beta\le\beta_c$), with $\mathbf EF_n$ computed under the canonical product environment. Elements of $\mathcal S$ are represented by their representatives, with the topology generated by $d$-balls (no quotient). In the goal, $K$ and $\theta$ are chosen before the probability space. Part (a) is stated for all $\delta>0$ and part (c) for $\delta\in(0,1)$, as printed.

Trivializing encodings are ruled out: $\mathcal G_{\delta,K}$ requires total mass exactly $1$; $W_\delta$ and $N$ take values in $\mathbb N\cup\{\infty\}$ so that an empty infimum is $\infty$; $Q$ is computed in $[0,\infty]$ so that $1/0=\infty$; the sum in $\widetilde F$ is taken in $[0,\infty]$; $\mathcal M$ avoids a real infimum over $\mathcal K$; $\mathfrak L$ is non-degenerate; and the phase hypotheses are limits that exist.

A complete development needs: the metric space $(\mathcal S,d)$ and its compactness, the measurability and continuity of $\mathcal T$, the Wasserstein space $\mathcal P(\mathcal S)$ (here through the published RWPI.SqrtLasso.transportCost), and the convergence $\mathcal W(\mu_n,\mathcal M)\to0$ (Theorem 4.9) together with $\mathcal M=\{\delta_0\}$ at high temperature (Theorem 5.2), both posed in the companion mission. Contributions to any milestone, and to the shared infrastructure of $\mathcal S$, are welcome.

Selected references

• E. Bates, S. Chatterjee, The endpoint distribution of directed polymers, Ann. Probab. 48 (2020); arXiv:1612.03443v5. https://arxiv.org/abs/1612.03443
• F. Comets, N. Yoshida, Directed polymers in random environment are diffusive at weak disorder, Ann. Probab. 34 (2006). https://doi.org/10.1214/009117905000000828
• F. Comets, T. Shiga, N. Yoshida, Directed polymers in a random environment: path localization and strong disorder, Bernoulli 9 (2003). https://doi.org/10.3150/bj/1065444233
• P. Carmona, Y. Hu, On the partition function of a directed polymer in a Gaussian random environment, Probab. Theory Related Fields 124 (2002). https://doi.org/10.1007/s004400200213
• F. Comets, V.-L. Nguyen, Localization in log-gamma polymers with boundaries, Probab. Theory Related Fields 166 (2016). https://doi.org/10.1007/s00440-015-0662-4
• F. Comets, Directed Polymers in Random Environments, Lecture Notes in Math. 2175, Springer (2017). https://doi.org/10.1007/978-3-319-50487-2

Motivation

Textbook quantum theory starts from postulates about Hilbert spaces, density matrices and completely positive maps, none of which has an evident operational meaning. A long line of work, from Birkhoff–von Neumann quantum logic through Ludwig, Hardy (quant-ph/0101012), Dakić–Brukner and Masanes–Müller (arXiv:1004.1483), asks whether the formalism can instead be derived from principles that speak only about preparations, measurements and their statistics.

Chiribella, D'Ariano and Perinotti (Phys. Rev. A 84, 012311 (2011), arXiv:1011.6451) give such a derivation for finite-dimensional quantum theory. Five axioms (causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning) describe a broad class of information-processing theories containing classical theory; one further postulate, purification, singles out quantum theory. The paper builds on the framework of operational-probabilistic theories of the same authors (Phys. Rev. A 81, 062348 (2010)).

Setting

An operational-probabilistic theory (OPT) has systems $A,B,\dots$, a composite system $AB$ for every pair, and, for each pair $(A,B)$, tests: finite families $\{\mathcal C_i\}_{i\in X}$ of transformations from $A$ to $B$. Tests with no input are preparation tests (families of states $\rho_i$), tests with no output are observation tests (families of effects $a_j$). Composing a preparation test with an observation test yields a joint probability distribution $p(i,j)=(a_j|\rho_i)$, and parallel composition multiplies probabilities. After identifying objects with the same statistics, the states of $A$ span a real vector space $\mathrm{St}_{\mathbb R}(A)$ of finite dimension $D_A$, effects are linear functionals on it, and transformations are linear maps. $\mathrm{St}_1(A)$ denotes the normalized (deterministic) states.

Standard notions are then defined operationally: refinement and coarse-graining, pure states and atomic effects/transformations (only trivial refinements), completely mixed states (refined by every state), reversible transformations, the face $F_\rho$ of a state, and perfectly distinguishable families $\{\rho_i\}_{i=1}^N$ (there is an observation test with $(a_j|\rho_i)=\delta_{ij}$). The informational dimension $d_A$ is the common size of all maximal perfectly distinguishable families of pure states.

Formalization targets

Goal (Theorem 20)

For every theory satisfying the six principles and every system $A$, there is a real-linear isomorphism $S:\mathrm{St}_{\mathbb R}(A)\to\mathrm{Herm}_n(\mathbb C)$ with

$$S\big(\mathrm{St}_1(A)\big)=\{M\in M_n(\mathbb C):\ M\succeq 0,\ \operatorname{tr}M=1\},$$

and $n=d_A$, the size of every maximal family of perfectly distinguishable pure states. In words: the normalized states of every system are exactly the density matrices on $\mathbb C^{d_A}$.

Milestones

In the order of the paper: Theorem 6 (maximal distinguishable sets and completely mixed states), Lemma 16 (atomicity of composition), Theorem 8 (pure state / atomic effect duality), Lemma 32 (the informational dimension is well defined), Corollary 15 ($d_{AB}=d_Ad_B$), Theorem 9 with Lemma 10 (the invariant state is the uniform mixture of any maximal set), Theorem 10 (spectral decomposition), Theorem 12 ($D_A=d_A^2$), Theorem 13 (the Bloch ball and $G_A\cong SO(3)$ for $d_A=2$), Theorem 16 (superposition principle).

Significance

The result shows that, inside a class of theories defined by operational requirements, the density-matrix formalism is forced by purification. The intermediate results are of independent interest: an operational spectral theorem (Theorem 10), the dimension formula $D_A=d_A^2$ (Theorem 12) that replaces Hardy's "simplicity" axiom, and the derivation of the qubit Bloch ball (Theorem 13). Corollary 52 of the paper upgrades the goal to transformations (all completely positive trace-non-increasing maps), using a cited result of the 2010 framework paper; it is not part of this mission's goal.

The paper is a physics article with diagrammatic proofs and several steps delegated to the earlier framework paper. A formalization makes every framework assumption explicit and checks the derivation end to end; no machine-checked development of operational-probabilistic theories is known to the proposer.

Difficulty

The derivation never assumes a Hilbert space, so the matrix representation must be built from the principles: first qubits (via the Bloch ball classification, which uses the classification of compact subgroups of $O(3)$), then projections on faces, the superposition principle and finally a coordinate system on $d$-level systems in which positivity of all states can be checked. Each step relies on many operational lemmas (Choi isomorphism, teleportation, uniqueness of purification up to channels) that in the paper are proved diagrammatically or cited.

Formalization scope

Lean namespace InfoDerivQT. A theory is a structure OPT already in quotiented, finite-dimensional form: $\mathrm{St}_{\mathbb R}(A)$ is modelled as $\mathbb R^{D_A}$, effects as linear functionals, transformations as linear maps, and tests as families indexed by finite types. The framework records the circuit rules used throughout the paper: the probability rule, product rule, coarse-graining, identity, sequential composition with classical control, classical randomization, rescaled preparations, parallel composition of all kinds of tests, conditioning on one side of a bipartite state, swap and associator, closedness of the state set, and spanning of states and effects. Because transformations are identified with their action on single-system states, this encoding is faithful in the presence of local distinguishability (Eq. (5) of the paper), which every target assumes. The trivial system is not modelled. The six principles are bundled in OPT.SatisfiesPrinciples; quantum theory is a model, so the hypothesis is satisfiable. The choice of framework axioms is the main point for audit: a missing circuit rule could make a target false, an extra one could exclude intended theories.

Contributions welcome: proofs of the milestones, a formal check that finite-dimensional quantum theory is a model of SatisfiesPrinciples, and the Choi isomorphism and teleportation lemmas of Secs. IV and IX as further milestones.

Selected references

• G. Chiribella, G. M. D'Ariano, P. Perinotti, Informational derivation of quantum theory, Phys. Rev. A 84, 012311 (2011). https://doi.org/10.1103/PhysRevA.84.012311
• G. Chiribella, G. M. D'Ariano, P. Perinotti, Probabilistic theories with purification, Phys. Rev. A 81, 062348 (2010). https://doi.org/10.1103/PhysRevA.81.062348
• L. Hardy, Quantum theory from five reasonable axioms (2001). https://arxiv.org/abs/quant-ph/0101012
• Ll. Masanes, M. P. Müller, A derivation of quantum theory from physical requirements, New J. Phys. 13, 063001 (2011). https://arxiv.org/abs/1004.1483

Motivation

A directed polymer in a random environment is a random up-right lattice path whose law is reweighted by random site weights. Its free energy, the logarithm of the partition function, is believed to belong to the Kardar–Parisi–Zhang (KPZ) universality class: for a path of length of order $N$, the free energy fluctuates on the scale $N^{1/3}$ and the path wanders on the scale $N^{2/3}$. For zero-temperature analogues (last-passage percolation with exponential or geometric weights) these exponents were established through exact formulas from random matrix theory (Johansson 2000) and later through a probabilistic coupling argument based on the Burke property of queues (Balázs–Cator–Seppäläinen 2006).

For directed polymers at positive temperature no model with the KPZ exponents was known until Seppäläinen (arXiv:0911.2446, Ann. Probab. 2012) introduced the log-gamma polymer, whose weights are reciprocals of gamma variables, and proved that its free energy has variance of order $N^{2/3}$ in the characteristic direction. The model has since become a basic exactly solvable polymer:

• 2009: Seppäläinen, the log-gamma polymer with boundary conditions; variance bounds of order $N^{2/3}$ and path fluctuation exponent $2/3$, by a Burke property and a variance identity.
• 2013: Borodin, Corwin and Remenik, Fredholm determinant formula and Tracy–Widom GUE limit of the free energy, for a range of parameters.
• 2014: Corwin, O'Connell, Seppäläinen and Zygouras, Tropical combinatorics and Whittaker functions, an exact formula for the law of the partition function via the geometric RSK correspondence.

The present mission formalizes the 2009 variance theorem, which needs neither of the later exact formulas.

Setting

Sites are $\mathbb Z_+^2=\{0,1,2,\dots\}^2$ and $\mathbb N=\{1,2,\dots\}$. A weight configuration assigns a positive number $Y_{i,j}$ to each site. On the axes, $U_{i,0}=Y_{i,0}$ and $V_{0,j}=Y_{0,j}$ for $i,j\in\mathbb N$ are the boundary weights, and $Y_{i,j}$, $i,j\in\mathbb N$, are the bulk weights.

An up-right path from $(0,0)$ to $(m,n)$ is a sequence $x_0=(0,0),x_1,\dots,x_{m+n}=(m,n)$ whose steps are $(1,0)$ or $(0,1)$. The partition function is

$$Z_{m,n}=\sum_{x}\prod_{k=1}^{m+n}Y_{x_k},$$

the weight of the origin excluded, $Z_{0,0}=1$. The quenched polymer measure gives the path $x$ probability $Q^\omega_{m,n}(x)=Z_{m,n}^{-1}\prod_{k=1}^{m+n}Y_{x_k}$, and the annealed measure is its average $P_{m,n}=\mathbb E\,Q^\omega_{m,n}$ over the environment. The exit points $\xi_x$ and $\xi_y$ are the numbers of initial steps the path takes along the $x$-axis and along the $y$-axis.

Assumption (2.4). Fix $0<\theta<\mu$. The weights $\{U_{i,0},V_{0,j},Y_{i,j}: i,j\in\mathbb N\}$ are independent with

$$U_{i,0}^{-1}\sim\mathrm{Gamma}(\theta,1),\qquad V_{0,j}^{-1}\sim\mathrm{Gamma}(\mu-\theta,1),\qquad Y_{i,j}^{-1}\sim\mathrm{Gamma}(\mu,1).$$

Let $\Psi_0=(\log\Gamma)'$ and $\Psi_1=\Psi_0'$ be the digamma and trigamma functions. The characteristic direction is $(\Psi_1(\mu-\theta),\Psi_1(\theta))$. For a real scaling parameter $N$ and a constant $\gamma$, the endpoint satisfies

$$|m-N\Psi_1(\mu-\theta)|\le\gamma N^{2/3}\quad\text{and}\quad|n-N\Psi_1(\theta)|\le\gamma N^{2/3}\qquad(2.6).$$

Formalization targets

Goal: Theorem 2.1

There are constants $0<C_1,C_2<\infty$ and $N_0$, depending on $\theta,\mu,\gamma$, such that under (2.4) and (2.6)

$$\mathrm{Var}(\log Z_{m,n})\le C_2N^{2/3}\quad(N\ge1),\qquad C_1N^{2/3}\le\mathrm{Var}(\log Z_{m,n})\quad(N\ge N_0).$$

Milestones

The upper bound runs through the Burke property and the variance identity:

• Lemma 3.1 (monotonicity of the recursion (3.2)), Lemma 3.2 (gamma reversibility), Theorem 3.3 (Burke property), the mean (2.5), $\mathbb E\log Z_{m,n}=-m\Psi_0(\theta)-n\Psi_0(\mu-\theta)$.
• Theorem 3.7, the variance identity

$$\mathrm{Var}[\log Z_{m,n}]=n\Psi_1(\mu-\theta)-m\Psi_1(\theta)+2E_{m,n}\Bigl[\sum_{i=1}^{\xi_x}L(\theta,Y_{i,0}^{-1})\Bigr].$$

• Lemma 4.1 (variance comparison in $\theta$), Lemma 4.2, the exit-point bound (4.32) $E(\xi_x)\le CN^{2/3}$, Lemma 4.3 (quenched exit-point tails).

The lower bound runs through partition-function comparisons:

• Lemma 5.1, Lemma 5.4 (coupling), Lemma 5.5(i), Proposition 5.3 ($\lim_{\delta\searrow0}\varlimsup_NP\{1\le\xi_x\le\delta N^{2/3}\}=0$), Corollary 5.6 ($\mathrm{Var}\ge cN^{2/3}$, $c>0$).

Significance

The result. Theorem 2.1 was the first proof of the KPZ fluctuation exponent $1/3$ for a directed polymer at positive temperature. Its upper bound also yields a strong law of large numbers for $N^{-1}\log Z_{m,n}$ (2.7) and, with Theorem 3.3, a central limit theorem off the characteristic direction (Corollary 2.2). The exit-point estimates of Sections 4 and 5 give the path fluctuation exponent $2/3$ (Theorem 2.3) and are reused for the polymer without boundaries and the point-to-line polymer (Theorems 2.4–2.6).

Formalizing it. The theorem has been proved since 2009; no formal proof of it in a proof assistant is known. A formalization checks a proof with many interacting estimates and two corrected slips (below). The definitions made here (the lattice-path partition function, the inverse-gamma environment, the recursion (3.2), exit points, quenched and annealed measures) are the base for later missions on Theorems 2.3–2.7 of the same paper. Lemma 3.2 contains a gamma-distribution characterization (Lukacs' theorem) of independent interest.

Difficulty

The obvious route to a variance bound, a martingale decomposition of $\log Z_{m,n}$ over the $mn$ independent weights, gives only $\mathrm{Var}=O(m+n)$, i.e. order $N$; it cannot see the cancellation that produces $N^{2/3}$. The order $N^{2/3}$ is specific to the characteristic direction: off it, $\log Z_{m,n}$ satisfies a central limit theorem with variance of larger order (Corollary 2.2), so any argument must use the exact relation between the boundary parameters $\theta,\mu-\theta$ and the endpoint $(m,n)$. The upper bound requires controlling the annealed exit point $E(\xi_x)$ at the scale $N^{2/3}$, with tail estimates whose constants are uniform in the parameters. The lower bound is a separate statement: the path must not exit an axis at distance $o(N^{2/3})$ from the origin with non-vanishing probability, which no upper-bound estimate implies.

Formalization scope

Source: arXiv:0911.2446v4 (26 Aug 2015, revised version); its printed page numbers equal the PDF's. All declarations are in the namespace LogGammaPolymer.Variance.

• Sites are ℕ × ℕ; a path is a step sequence with a fixed number of east steps; $Z$ is a finite sum over these paths with the starting weight excluded. The environment Env θ μ P bundles one weight family Y : ℕ × ℕ → Ω → ℝ, measurability, mutual independence of every weight off the origin, and the three laws as images under $y\mapsto y^{-1}$ equal to Mathlib's gammaMeasure (shape, rate $1$). Positivity of the weights is not assumed pointwise in the probabilistic statements; it holds almost surely. The deterministic lemmas (3.1, 5.1, 5.4) are stated for every weight function positive off the origin.
• $N$ is real and $N^{2/3}$ is a real power. Variances use Mathlib's variance, and every upper bound or identity also asserts $\log Z_{m,n}\in L^2$ (or integrability of the averaged quantity), so that the junk value $0$ of variance and of the Bochner integral cannot satisfy it.
• Constants come after the parameters $(\theta,\mu,\gamma)$ and before the probability space (universe Type), the environment, $N$ and $(m,n)$. Upper limits in $N$ are stated as "for every $\eta>0$ there is $N_0$ with the bound $+\eta$ for $N\ge N_0$". The compact-set uniformity of Lemmas 4.1, 4.3 and (4.32) is formalized. The remark after Theorem 2.1 on uniform constants is not.
• Corrected slips. (i) Theorem 2.1 prints the lower bound for all $N\ge1$. It fails at $N=1$, $\theta=1$, $\mu=2$, $\gamma=2$ with $(m,n)=(0,0)$, where the variance is $0$. The lower bound is stated for $N\ge N_0$, which is what Corollary 5.6 proves. (ii) The "only if" of Lemma 3.2 fails for the constants $U=V=1$, $Y=1/2$. The hypothesis "$U$ is not a.s. constant" is added. (iii) Corollary 5.6 states $c>0$ explicitly.
• Theorem 3.3 is stated for down-right paths that coincide with the axes outside a finite portion. The paper reduces the general case to these.
• Not included: Lemma 3.5 (reversal), Proposition 3.4, Lemma 5.5(ii).

A formalization in which $Z$ includes the origin's weight, the laws are not exactly the inverse gammas with shapes $\theta,\mu-\theta,\mu$ and rate $1$, independence is dropped, $C_1=0$ is allowed, or the constants depend on the environment or on $N$ does not state Theorem 2.1.

Needed infrastructure: gamma–beta algebra and a Lukacs-type characterization, independence of finite families built by the recursion (3.2), differentiation of expectations in the shape parameter, and moment bounds for sums of i.i.d. variables. All of these are reusable beyond this mission. Proofs of any milestone, and of supporting lemmas such as (3.3)–(3.4), are welcome.

Selected references

• T. Seppäläinen, Scaling for a one-dimensional directed polymer with boundary conditions, Ann. Probab. 40 (2012) 19–73; revised version arXiv:0911.2446v4. https://arxiv.org/abs/0911.2446
• K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000) 437–476. https://arxiv.org/abs/math/9903134
• M. Balázs, E. Cator, T. Seppäläinen, Cube root fluctuations for the corner growth model associated to the exclusion process, Electron. J. Probab. 11 (2006) 1094–1132. https://arxiv.org/abs/math/0603306
• I. Corwin, N. O'Connell, T. Seppäläinen, N. Zygouras, Tropical combinatorics and Whittaker functions, Duke Math. J. 163 (2014) 513–563. https://arxiv.org/abs/1110.3489
• A. Borodin, I. Corwin, D. Remenik, Log-gamma polymer free energy fluctuations via a Fredholm determinant identity, Comm. Math. Phys. 324 (2013) 215–232. https://arxiv.org/abs/1206.4573
• E. Lukacs, A characterization of the gamma distribution, Ann. Math. Statist. 26 (1955) 319–324. https://doi.org/10.1214/aoms/1177728549

Motivation

Vertex operator algebras describe conformal theories algebraically, while conformal nets describe local operator algebras. Passing between them requires analytic control of fields. The pinned manuscript supplies the research context.

Setting

The selected algebra is simple, unitary, CFT-type and strongly rational. Its modes act on an inner product space, and smeared fields act on the Hilbert completion.

Formalization target

The selected goal is OAI.MinimalVertex.main. Its central assertion is

$$\mathrm{energy\ bounds}\ \land\ \mathrm{strong\ locality}\ \land\ \mathrm{irreducible\ conformal\ net}.$$

The theorem states that, for a CFT-type vertex operator algebra A on a complex inner product space V (a vertex algebra with vacuum, state-field map and Jacobi identity, together with a conformal vector, central charge, finite-dimensional graded pieces with degree-zero part spanned by the vacuum, conformal vector in degree 2 acting as the grading operator, and the Virasoro relations), equipped with a unitary structure U (an antilinear involution fixing the vacuum and conformal vector, compatible with all modes, together with a unit-norm vacuum and an invariance relation between a mode and the corresponding mode of the transformed adjoint-side vector), if A is simple (nonzero vacuum and no ideals other than 0 and the whole space) and strongly rational (self-contragredient, rational in the sense that every admissible weak module is completely reducible, and C2-cofinite), then three things hold. First, A has polynomial energy bounds: for every a in V there are C>0 and natural numbers p,k with ||a_(n) b|| ≤ C(1+|n|)^p ||(1+L_0)^k b|| for all integers n and all b in V. Second, the CKLW strong locality property holds: all vectors satisfy these bounds, and for every proper circle arc I the von Neumann algebra generated by closed smeared fields supported in I, built on the completion of V, lies in the commutant of the algebra attached to the complementary arc. Third, the assignment of these interval algebras to proper arcs admits the structure of an irreducible conformal net, meaning a separable Hilbert space with isotony, locality, a continuous Mobius representation extended to a continuous projective representation of smooth circle diffeomorphisms with covariance and locality of the action, a unit invariant vacuum that is unique up to scalar and cyclic, a positive self-adjoint Hamiltonian generating the rotation flow, and trivial commutant of all interval algebras apart from scalars.

Significance and status

The target proves polynomial energy bounds, the specified CKLW strong locality property, and existence of an irreducible conformal-net structure. Complete rationality, category equivalences and extension classification are not conclusions of this reference. 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

Formal algebraic identities must yield polynomial operator bounds and locality for closed smeared fields on the completion.

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, Strongly rational unitary vertex operator algebras and conformal nets, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A known zero-energy vector does not by itself give a uniform positive gap above it. The Laughlin problem asks for a lower bound controlling every competing antisymmetric state. The pinned manuscript supplies the research context.

Setting

At N particles set Q=3(N−1). States are complex functions on finite configurations, with antisymmetry under exchanging particles. The energy is a sum of squared pair-annihilation amplitudes.

Formalization target

The selected goal is OAI.LaughlinGap.thm_main. Its central assertion is

$$\frac1{25}\operatorname{dist}(\psi,\mathbb C\Psi_{\rm L})^2\leq E(\psi).$$

The theorem states that there is a threshold N₀ ≥ 2 such that for every N ≥ N₀ and every antisymmetric complex-valued state ψ on N particles, each with local levels 0,…,Q where Q = 3(N−1), one has (1/25)·d(ψ)² ≤ E(ψ). Here a state assigns a complex number to each configuration a : Fin N → {0,…,Q}, and antisymmetric means that swapping the values at two distinct positions i and j negates ψ. The energy E(ψ) sums, over pairs i<j, over p = 0,…,2Q−2, and over configurations a with a_i = a_j = 0, the squared modulus of the pair amplitude, which is the sum over x,y of pairCoefficient(Q,p,x,y)·ψ(a with a_i replaced by x and a_j by y). The pair coefficient vanishes unless x+y = p+1, in which case it equals (x−y)/√2 times the square root of Q^{(x)}·Q^{(y)}·p! divided by Q·(2Q−2)^{(p)}·x!·y!, where m^{(k)} is the descending factorial. The Laughlin vector is built from the polynomial ∏{i<j}(x{i,0}x_{j,1} − x_{j,0}x_{i,1})³ in variables indexed by particle and a Boolean: its coefficient at the monomial with exponent a_i on x_{i,1} and Q−a_i on x_{i,0} is divided by ∏_i √C(Q,a_i). The quantity d(ψ)² is the infimum over complex c of the sum over configurations of |ψ(a) − c·Laughlin(a)|², the squared distance from ψ to the line spanned by the Laughlin vector, with no normalization of ψ assumed.

Significance and status

The selected goal has constant 1/25 and no normalization requirement on the state. The Fock-space inequality, the earlier 1/100 formulation and the planar endpoint are separate references; they retain their own representations and constants. 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

The bound must be uniform for all sufficiently large particle numbers and for every state, rather than a variational estimate on a selected excitation.

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.

Additional published targets are included as separate references:

• OAI.Laughlin.mainTarget_proved (Open).
• OAI.LaughlinFock.thm_fock (Open).
• OAI.Laughlin.planar_gap (Open).

Selected references

• OpenAI, A Fock-space inequality and the Laughlin spectral gap, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

An exterior electron count defines a radius of a neutral atom without selecting individual electrons. Its scaling tests how well Thomas–Fermi theory describes the outer region of the full interacting atom. The pinned manuscript supplies the research context.

Setting

Choose any normalized ground state for each neutral atom with N+1 electrons. The radius is the infimum of radii outside which the expected electron mass is at most m.

Formalization target

The selected goal is OAI.NeutralAtom.generalized_outer_radii. Its central assertion is

$$m^{1/3}R_m^{\rm upper},\ m^{1/3}R_m^{\rm lower}\longrightarrow (81\pi^2/2)^{1/3}.$$

The theorem states that, for every choice of wavefunctions Ψ_N for neutral atoms with N+1 electrons and nuclear charge Z=N+1 (each a spin-dependent complex function of N+1 positions in three-dimensional space, with spins taking two values), such that each Ψ_N is a normalized ground state, the outer radii of the atoms obey a Thomas–Fermi-type scaling law. A normalized ground state is an antisymmetric wavefunction with a weak gradient, square-integrable in each spin component together with its gradient, with finite Coulomb integrals against |Ψ|², total squared norm 1 summed over spins, and minimal energy among all such normalized functions. The energy is half the squared L² norm of the gradient plus the expectation of the Coulomb potential, which is −Z times the sum of inverse distances of electrons to the nucleus plus the sum of inverse inter-electron distances over pairs. The electron density is N+1 times the spin-summed integral of |Ψ|² over the other N positions, and the radius for m is the infimum of r≥0 such that the density mass outside the ball of radius r is at most m. For each m, upperRadius and lowerRadius are the limsup and liminf, in the extended reals, of these radii as N→∞ with N+1>m. With bTF=(81π²/2)^(1/3), the theorem states that both m^(1/3)·upperRadius(m) and m^(1/3)·lowerRadius(m) converge to bTF as m→∞ through the natural numbers.

Significance and status

The target uses extended-real upper and lower radii, followed by a natural-number limit in m. No spherical symmetry is assumed, and the atom remains neutral. 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

The assertion must hold for every choice of ground states. The inner large-charge limsup and liminf cannot be silently replaced with an assumed pointwise limit.

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, Generalized outer-electron radii of neutral Coulomb atoms, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Removing outer electrons changes an atom's energy on a smaller scale than its total binding energy. A total-energy asymptotic alone does not determine the difference. The pinned manuscript supplies the research context.

Setting

The quantum model uses antisymmetric spin-dependent wavefunctions, two spin states, weak gradients and the full nuclear and electron-electron Coulomb interactions. The comparison is with the Thomas–Fermi density functional.

Formalization target

The selected goal is OAI.CoulombAtom.generalized_ionization. Its central assertion is

$$I(m,Z)/m^{7/3}\longrightarrow a,\qquad m\to\infty,\ Z/m\to\infty.$$

The theorem states that the proposition MainStatement holds: there is a real constant a>0 such that three asymptotic statements about atomic ionization energies all hold with this same a. Here the quantum energy of N electrons around a nucleus of charge Z is the infimum, taken over admissible spin-dependent wavefunctions on (ℝ³)^N, of the energy (1/2) times the total squared L² norm of all gradient components, minus Z times the expectation of Σᵢ 1/|xᵢ|, plus the expectation of Σ_{i<j} 1/|xᵢ−xⱼ|, with energy defined as 0 when N=0. Admissibility means that each spin component and each prescribed gradient component is square integrable, the gradient components are the weak partial derivatives of the values, the values are antisymmetric under simultaneous permutation of spins and positions (by the sign of the permutation, almost everywhere), the total squared norm summed over spins is 1, and the nuclear and electron-electron Coulomb densities are integrable. The ionization energy of removing m electrons from a neutral atom of charge Z is ionization(m,Z)=E(Z, Z−m)−E(Z, Z), with natural-number subtraction. The Thomas-Fermi energy tfEnergy(Z,M) is the infimum over nonnegative integrable densities ρ on ℝ³ of total mass M, with ρ^{5/3}, ρ/|x| and ρ(x)ρ(y)/|x−y| integrable, of (3/10)(3π²)^{2/3}∫ρ^{5/3} − Z∫ρ/|x| + (1/2)∬ρ(x)ρ(y)/|x−y|, and tfIonization(m,Z)=tfEnergy(Z,Z−m)−tfEnergy(Z,Z) for real m and Z. The three conclusions are: for every real m>0, tfIonization(m,Z) tends to a·m^{7/3} as the real number Z tends to infinity; for all natural-number sequences m_j, Z_j with 1≤m_j<Z_j, m_j→∞ and Z_j/m_j→∞, the ratio ionization(m_j,Z_j)/m_j^{7/3} tends to a; and as m→∞ through the naturals, both limsup and liminf over Z of ionization(m,Z), each divided by m^{7/3}, tend to a.

Significance and status

The main proposition includes a positive common constant, the fixed-m Thomas–Fermi limit, the joint quantum limit, and normalized limsup and liminf limits. It concerns energies rather than outer-electron radii. 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

Errors negligible relative to the total atomic energy can still dominate ionization energies. The common leading constant must work in the joint regime and both iterated limits.

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, Generalized ionization energies for full Coulomb atoms, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Replacing a hyperboloidal end by an asymptotically flat end can connect Bondi mass with ADM mass. The source seeks a replacement that preserves interior geometry, the energy condition, and almost all enclosing area. The source is OpenAI's September 2026 manuscript.

Setting

A CKS exterior datum describes a three-dimensional hyperboloidal end and its mass aspect. Its Bondi charge is energy-momentum $(E,P)$, assumed strictly future timelike. An enclosing cut is a surface in the supplied geometric class; its area is computed from the metric.

Formalization targets

$$g_R\ge(1-\varepsilon(R))g,\quad\varepsilon(R)\to0,\quad m_{\mathrm{ADM}}(g_R)=\sqrt{E^2-|P|^2}+\eta_R,\quad0\le\eta_R\le2R^{-1/2}.$$

For a connected, Hausdorff, second countable smooth 3-manifold N with boundary and a smooth Riemannian metric g with a smooth symmetric tensor field K, such that N is orientable, the boundary is compact and nonempty, g is complete, and (g,K) satisfies the pointwise local-chart physical dominant energy condition PhysicalDEC, the following holds. Suppose d is a CKS exterior-end datum for (g,K): a coordinate end outside radius d.chart.radius in which g and K are represented by smooth perturbations, together with a smooth mass aspect function on the sphere and the tensor patches realizing it. If the Bondi charge (energy, momentum) of d's mass aspect, (E,P), is timelike, meaning |P|<E, then there exist another such datum d', a radius R₀ with d'.chart.radius<R₀ and 12≤R₀, and a function ε with ε(R)→0 as R→∞, such that d' has Bondi charge (√(E²−|P|²),0), and the minimal enclosing area of g is finite. Moreover, for every R≥R₀ one has 0≤ε(R)<1 and there are a complete smooth metric gR, a smooth symmetric tensor field kR, spatial tensor fields G and k on Euclidean 3-space, and a number η with these properties. The pair (gR,kR) agrees with (g,K) at every point outside the chart domain or with chart coordinate norm at most R, and satisfies PhysicalDEC and integrable constraints. Also gR≥(1−ε(R))g as quadratic forms. On the end, gR and kR equal the end metrics built from G and k in d'.chart. Each Cartesian component of G minus the identity satisfies the order-1 Symbol condition from CKSADM, and k vanishes where ‖x‖>2R². As r→∞ the spatial ADM energy of G tends to √(E²−|P|²)+η and the ADM momentum of (G,k) tends to 0, with 0≤η≤2R^(−1/2). Finally, gR has finite minimal enclosing area, (1−ε(R)) times the minimum enclosing area of g is at most that of gR, and for every outer domain D the cut areas of g and gR are finite and satisfy (1−ε(R))·cutArea(g,D)≤cutArea(gR,D).

The goal is OAI.CKSSourceExterior.area_controlled_end_replacement. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• schwarzschild equality examples.

Significance

The selected goal constructs end replacements with zero limiting ADM momentum and quantitative area comparison, including minimum enclosing area. The Schwarzschild equality examples are attached as a separate target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Changing the end can create a cheaper enclosing surface or violate the dominant energy condition. Agreement on each retained interior region does not alone prevent either problem.

Formalization scope

The manifold is a connected Hausdorff second-countable smooth three-manifold with compact nonempty boundary, and the original complete data satisfy the physical dominant energy condition. The main target is end replacement; it does not itself state the final Bondi–Penrose inequality. The equality-example target keeps its stronger boundary and no-additional-horizon hypotheses.

The shared definitions are supplied by CKSBondiPenrose, CKSBondiPenrose_002. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Area-controlled end replacement and the Bondi Penrose inequality in the CKS class, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

An Ising spin system probes a quadratic form only on cube vertices. The source asks whether random orthogonal eigenvectors allow its pressure to be determined by the limiting eigenvalue distribution at every positive temperature. The source is OpenAI's September 2026 manuscript.

Setting

The pressure is the normalized logarithm of the average Boltzmann weight under the uniform spin prior. Eigenvectors are Haar orthogonal, and the deterministic empirical eigenvalue laws converge weakly to a compactly supported probability law. The variational formula uses an edge-extended spectral transform.

Formalization targets

$$\mathbb E P_N(\beta)\to\mathcal V_\beta,\qquad P_N(\beta)\to\mathcal V_\beta\ \text{almost surely}\qquad(\beta>0).$$

For a spin system on N Ising spins σ ∈ {−1,1}^N, the rotated pressure for eigenvalues λ₁,…,λ_N, an orthogonal rotation U and a field c is (1/N) times the log of the average over all 2^N spin configurations of exp(H(σ)), where H(σ) = (1/2)∑ᵢ λᵢ (Uσ)ᵢ² + ∑ᵢ cᵢσᵢ. The theorem states that, for any probability space (Ω,P), random N×N orthogonal matrices U_N that are measurable and whose laws are right-invariant under multiplication (Haar-type), and any deterministic eigenvalue arrays (eig_N,i), the following holds under these assumptions: ν is a probability measure on ℝ whose support lies in [a,b] and contains both a and b; for every ε>0, eventually in N all eigenvalues lie in [a−ε,b+ε]; the empirical spectral laws (1/N)∑ᵢ δ_{eig_N,i} converge weakly to ν; and the inverse temperature β is strictly positive. Then, with eigenvalues β·eig_N,i, rotation U_N(ω)⁻¹ and zero external field, the expected rotated pressure ∫ pressure dP converges as N → ∞, and the pressure itself converges for P-almost every ω, in both cases to the real part of the variational functional of the measureR transform of the β-rescaled law of ν, evaluated at the edge β·b.

The goal is OAI.InvariantIsing.positive_temperature_pressure_unconditional. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• gaussianPattern ground limit unconditional.
• gaussianPattern norm limits unconditional.
• gaussianPattern pressure limit unconditional.
• ground state limit unconditional.
• limiting pressure of extreme limits unconditional.
• limiting wasserstein field pressure of extreme limits unconditional.
• random field pressure tendsto ae unconditional.
• random pressure limit unconditional.
• random pressure tendsto ae unconditional.
• random pressure tendsto in measure unconditional.

Significance

The selected goal is the all-positive-temperature zero-field pressure theorem. The attached results also cover field laws, random spectra, Gaussian-pattern pressure and ground energy, and related norm limits under their stated assumptions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Weak spectral convergence does not control rare extreme eigenvalues. The explicit no-outlier condition is essential to the selected statement’s comparison with the limiting spectral functional.

Formalization scope

The spin prior is uniform probability, and temperature is implemented by multiplying eigenvalues by $\beta$. The no-outlier condition holds eventually within every enlargement of the limiting support interval. Almost-sure convergence and expectation convergence are both conclusions; other attached variants keep their own uniform-integrability and field hypotheses.

The shared definitions are supplied by InvariantIsing. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, All-temperature pressure for orthogonally invariant Ising spin glasses, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The spherical perceptron assigns random rewards to vectors of fixed length. The source asks for an exact pressure formula without a convexity or symmetry condition on the single-pattern potential. The source is OpenAI's September 2026 manuscript.

Setting

Configurations lie on the sphere of radius $\sqrt n$, equipped with uniform probability measure. There are $\lfloor\alpha n\rfloor$ independent Gaussian patterns. The variational value minimizes a Brownian stochastic-control functional plus an extended nonnegative entropy over monotone trials.

Formalization targets

$$\exists p\in\mathbb R:\quad\mathcal V(\alpha,\beta,\varphi)=p,\qquad\mathbb E p_n\to p,\qquad p_n\xrightarrow{\mathbb P}p.$$

For a probability measure P on continuous paths ℝ≥0→ℝ under which the evaluation process is a real Brownian motion, and for parameters α>0, β>0 and a bounded continuous function φ:ℝ→ℝ, there is a real number p with three properties. First, the variational value equals p (as an extended real). That value is the infimum over all trials m of α times the control value of βφ at m, plus the entropy of m. A trial is a nondecreasing measurable function m:[0,1]→[0,1]. Its entropy is one half of the integral over t of 1/∫ₜ¹ m(s)ds minus 1/(1−t), taken in [0,∞]. The control value of f at m is the supremum, over progressively measurable controls v with finite cost E∫ m(t)v(t)²dt, of E f(B₁+∫₀¹ m(t)v(t)dt) minus half that cost. Second, the expected spherical-perceptron pressure E[pressure(N+1)] converges to p as N→∞. For dimension n, pressure is (1/n) log ∫ exp(β Σₐ φ(⟨gₐ,x⟩/√n)) dx, with x uniform on the sphere of radius √n in ℝⁿ. The gₐ are the rows of a pattern matrix with ⌊αn⌋ rows and n i.i.d. standard Gaussian entries per row. Third, the pressure concentrates: for every ε>0, the Gaussian probability that |pressure(N+1)−p|>ε tends to 0 as N→∞.

The goal is OAI.SphericalPerceptronFreeEnergy.main. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• spherical linear field formula.

Significance

The selected main target proves finiteness of the variational value, convergence of expected pressure, and concentration around the same number. The linear-field formula is attached as a supporting result. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

An infimum involving a possibly infinite entropy must be connected with the actual finite-dimensional spherical integral. The potential is only bounded and continuous, so smoothness cannot be assumed.

Formalization scope

Density and inverse temperature are strictly positive. Controls are progressively measurable for the stated Brownian filtration and have finite cost. Dimension is written as $N+1$ to stay positive. The Brownian and cascade-based linear-field definition groups are independent references.

The shared definitions are supplied by PerceptronFreeEnergy, SphericalField. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, The free energy of the spherical random perceptron, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The Ising perceptron weights binary configurations by their projections onto random patterns. The paper develops a variational description of its pressure; the available formal target checks that the proposed variational value is finite. The source is OpenAI's September 2026 manuscript.

Setting

An overlap path is an almost-everywhere class on $(0,1)$ with a monotone representative taking values in $[0,1]$. The variational expression combines a Gaussian pattern functional with an Ising entropy, defined as a supremum over monotone nonnegative field steps.

Formalization targets

$$\alpha\ge0,\quad f\in C_b(\mathbb R)\quad\Longrightarrow\quad\exists p\in\mathbb R:\ \operatorname{variationalValue}(\alpha,f)=p\text{ in }\overline{\mathbb R}.$$

For every real α ≥ 0 and every continuous function f : ℝ → ℝ that is bounded (there is K with |f(x)| ≤ K for all x), the variational value of the Ising perceptron model is a finite real number, i.e. variationalValue(α,f) equals the extended real (p : EReal) for some real p. Here variationalValue(α,f) is the infimum, over all admissible overlap paths q (almost-everywhere-defined functions on (0,1) that agree a.e. with a monotone function taking values in [0,1]), of α times the pattern functional of f at q plus the Ising entropy of q. The pattern functional is the limit as n→∞ of uniformPattern, a nested Gaussian transform over a uniform grid with n+1 cells built from cell averages of q and applied to f at 0, where each transform is either a Gaussian average or a log-exponential-moment average divided by d, depending on whether d is zero. The Ising entropy is the supremum, over field steps (a partition of [0,1] with nonnegative monotone step values), of the field recursion value plus half the integral of the step function against q. The statement asserts that this infimum is neither +∞ nor −∞.

The goal is OAI.IsingPerceptron.variationalValue_real_of_continuous.

Significance

The goal rules out both infinite extended-real values for continuous bounded potentials. This is a well-definedness component needed before a real-valued limit formula can be used. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The entropy is a supremum over an unbounded family of fields and the outer expression is an infimum over paths. Boundedness of the input potential alone does not syntactically make this extended-real expression finite.

Formalization scope

The target is variationalValue_real_of_continuous, with nonnegative density and continuous bounded potential. It does not assert convergence of finite-system pressure or the manuscript’s broader bounded-Borel result. Gaussian recursion and almost-everywhere path conventions are kept as published.

The shared definitions are supplied by IsingFiniteness. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, The free energy of the Ising random perceptron, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

A diluted spin glass has finitely many interactions per spin on average. The source seeks the exact thermodynamic pressure using a hierarchy of random local-field laws. The source is OpenAI's September 2026 manuscript.

Setting

The pressure is the expected logarithm of the partition function divided by the number of Ising spins. A Poisson number of even-arity interactions and independent external fields define the model. The cavity functional uses nested probability laws and iterated logarithmic power means.

Formalization targets

$$\lim_{N\to\infty}F_N=\inf_{r\ge0}\ \inf_{\zeta,\ 0<m_1<\cdots<m_r<1} B_r(\zeta,m).$$

For every model of a diluted p-spin glass with Ising spins in {+1,-1} that satisfies the standing admissibility hypotheses, the free-energy density F_N converges, as N tends to infinity, to a variational value, so existence of the thermodynamic limit is part of the conclusion. A model consists of a density α ≥ 0, a probability law on interaction samples (θ, a, b, f), where θ is a real function on spin configurations in {±1}^p, a and b are reals and f assigns to each of the p slots a real function on spins, and a probability law for the external field on ℝ. Admissibility means: p is even and at least 2; α > 0; ‖θ‖ = max_s |θ(s)| and |h| are integrable under the disorder and field laws; almost surely a > 0 and, for every configuration s, exp θ(s) = a(1 + b ∏_l f_l(s_l)) with |b ∏_l f_l(s_l)| < 1; the functions f_1,…,f_p are independent and identically distributed, b is independent of the vector f, every power (−b)^n with n ≥ 1 is integrable, and E[(−b)^n] ≥ 0. No boundedness of interactions, fields or messages is added. F_N is (1/N) times the expectation of log Σ_σ exp(−H), where the number k of interactions is Poisson with mean αN, the k interactions are independent disorder samples, the N fields are independent field samples, and each interaction is placed on p index choices in {1,…,N} (repetitions allowed) averaged uniformly over all choices; here the log-weight of σ is Σ_j θ_j(σ at the chosen indices) + Σ_i h_i σ_i. The limit is the infimum over depths r ≥ 0 of φ_r, itself the infimum, over a nested law ζ in the r-fold hierarchy of probability measures (each level with the weak topology and its Borel σ-field) and exponents 0 < m_1 < … < m_r < 1, of the cavity functional B_r. B_r equals log 2 plus the Poisson(αp)-averaged expectation of the site term, a logarithm of an average over spin ε of exp(hε + Σ_j message_j(ε)), minus α(p−1) times the expectation of the log of the edge weight, with both terms evaluated through iterated log power-means in the exponents m_i.

The goal is OAI.DilutedSpinGlass.mezard_parisi.

Significance

The equality identifies the limit with the infimum over all finite hierarchy depths. Existence of the thermodynamic limit is part of the conclusion, not an assumption. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Upper bounds at each hierarchy depth do not yield equality with the infinite-size model. Unbounded disorder requires retaining integrability hypotheses through nested expectations.

Formalization scope

The admissibility predicate requires positive density, even arity at least two, first moments, the specified interaction factorization, and positivity and integrability of the relevant powers. The statement adds no boundedness restriction on interactions, fields, or trial messages.

The shared definitions are supplied by DilutedSpin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, The Mézard–Parisi formula for diluted spin glasses, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

The relativistic Vlasov–Maxwell system is the basic kinetic model of a collisionless plasma: a cloud of charged particles, described by a phase-space density, moves under the electromagnetic field it generates, and the field evolves by Maxwell's equations with the particles as sources. Whether smooth, compactly supported data in three dimensions always produce a solution that stays smooth for all time has been the central question about the Cauchy problem for this system since the 1980s. Weak solutions exist globally, but they come without regularity or uniqueness, and every previous global classical result required smallness, a dimensional reduction, symmetry, or a nearby global reference solution.

This mission asks for a machine-checked proof of global existence and uniqueness of classical solutions for arbitrary smooth admissible data, as claimed in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

• 1984 — Wollman proves local existence and uniqueness of classical solutions (CPAM 1984).
• 1986 — Glassey and Strauss show that a classical solution continues as long as the momentum support stays bounded (ARMA 1986); in 1987 they prove global existence for initially dilute plasmas (CMP 1987).
• 1985–1998 — Glassey and Schaeffer obtain global classical solutions for symmetric relativistic Vlasov–Poisson (CMP 1985) and for reduced Vlasov–Maxwell models in one and one-half, two and one-half, and two dimensions (1990, 1997, 1998).
• 1989 — DiPerna and Lions prove global existence of weak solutions for large data (CPAM 1989); Rein treats the relativistic case directly (CMS 2004).
• 1990 — Rein proves stability of global existence near suitable global solutions (CMP 1990).
• 2002–2003 — New proofs of the continuation criterion by Klainerman–Staffilani (CPAA 2002) and Bouchut–Golse–Pallard (ARMA 2003).
• 2004–2016 — Refined continuation criteria: Schaeffer's small-data theorem with momentum tails (IUMJ 2004), Pallard (IUMJ 2005), Luk and Strain's two-dimensional projection criterion (CMP 2014) and moment bounds (ARMA 2016).
• 2020–2025 — Small-particle global results with large fields: Bigorgne (CMP 2020; APDE 2025), Wei–Yang (CMP 2021).
• 2026 — Wang establishes large-data global existence under cylindrical symmetry (arXiv:2203.01199, arXiv:2607.14685).
• September 2026 — The OpenAI preprint claims the general large-data result without symmetry (Theorem 1.1, p. 3).

Setting

For momentum $v\in\mathbb R^3$ let $q(v)=\sqrt{1+|v|^2}$ and $u(v)=v/q(v)$ (the relativistic velocity, $|u|<1$). The unknowns are a particle density $f(t,x,v)\ge0$ and fields $E(t,x),B(t,x)\in\mathbb R^3$, with charge and current densities $\rho_f=\int f\,dv$ and $j_f=\int u(v)f\,dv$. In the one-species normalization the system is

$$\partial_tf+u(v)\cdot\nabla_xf+(E+u(v)\times B)\cdot\nabla_vf=0,$$ $$\partial_tE-\nabla_x\times B=-j_f,\qquad \partial_tB+\nabla_x\times E=0,\qquad \nabla_x\cdot E=\rho_f,\qquad \nabla_x\cdot B=0 .$$

A smooth admissible datum $(f_0,E_0,B_0)$ has $f_0\in C_c^\infty(\mathbb R^3_x\times\mathbb R^3_v)$, $f_0\ge0$, $E_0,B_0$ smooth with every derivative bounded and $E_0,B_0\in L^2$, and satisfies $\nabla\cdot E_0=\rho_{f_0}$, $\nabla\cdot B_0=0$. A classical solution on $[0,\infty)$ is a $C^1$ triple solving the system pointwise, with $E,B$ continuous in time with values in $L^2$, and with $f(t,\cdot,\cdot)$ supported in a fixed compact set on each bounded time interval.

Formalization targets

Goal: Theorem 1.1 (p. 3)

Every smooth admissible datum generates a classical solution on $[0,\infty)$ with the given initial values; for every finite $T$ the solution is $C^\infty$ on $[0,T]\times\mathbb R^6$ (respectively $[0,T]\times\mathbb R^3$ for the fields) with compact phase-space support on $[0,T]$; and any other classical solution with the same datum agrees with it at every $t\ge0$. This is OAI.RVM.global_classical_solution.

Significance

The result itself. It settles the large-data global classical regularity problem for three-dimensional relativistic Vlasov–Maxwell, with no size, symmetry or neutrality assumption; nonzero total charge with its Coulomb tail is allowed. Global well-posedness at this level is the starting point for questions about long-time behaviour, scattering and stability of plasma equilibria that previously could only be posed for small or symmetric data.

Formalizing it. The proof combines the Glassey–Strauss representation of fields along backward light cones, energy-flux estimates, a delicate signed bootstrap, and local well-posedness and continuation theory. None of this PDE infrastructure (wave-equation representation formulas, characteristics of transport equations in phase space, Sobolev local theory) is currently available in a proof assistant at the needed level, so each component is reusable.

Difficulty

By the Glassey–Strauss criterion it suffices to bound the momentum support on finite time intervals. The natural approach estimates the absolute value of the force along a characteristic using the retarded field representation and energy flux through light cones. At receiver energy $w$ this loses a factor $\sqrt w$ relative to what is needed (Section 1.2, p. 4); the loss comes from sources whose velocity is much closer to the light ray than the receiver's. The preprint instead estimates the signed momentum increment $V_X(t_2)-V_X(t_1)$, integrating the retarded force along source trajectories before taking norms (Proposition 2.1, p. 5; Lemma 6.1, p. 24), controls direction changes (Lemma 7.1, p. 29), and closes a bootstrap whose time-to-double lower bounds have a divergent sum (Section 9).

Formalization scope

• Space and momentum are EuclideanSpace ℝ (Fin 3); derivatives are Fréchet derivatives in coordinate directions; the time derivative is derivWithin on $[0,\infty)$, so $t=0$ is one-sided.
• Admissible encodes $C^\infty$ with compact support and nonnegativity for $f_0$; ContDiff ℝ ∞ with all iterated derivatives bounded and MemLp 2 for $E_0,B_0$; and both Gauss constraints pointwise.
• Classical requires $C^1$ regularity on the closed half-spaces, $f\ge0$, continuity of $t\mapsto E(t),B(t)$ into $L^2$ on $[0,\infty)$, compact phase support on each $[0,T]$, all five equations pointwise for $t\ge0$ (including both constraints), and the initial values.
• The conclusion asserts existence, smoothness on every finite horizon, and uniqueness within the same classical class; uniqueness is pointwise equality at all $t\ge0$. The hypotheses are satisfiable (e.g. $f_0=0$, $E_0=B_0=0$), so the statement is not vacuous.
• $\rho$ and $j$ are Bochner integrals in $v$; for compactly supported $f$ these are the genuine moments.

Selected references

• OpenAI, Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell system, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-classical-solutions-of-the-three-dimensional-relativistic-Vlasov-Maxwell-system-September-23-2026/paper.pdf
• R. T. Glassey, W. A. Strauss, Singularity formation in a collisionless plasma could occur only at high velocities, Arch. Ration. Mech. Anal. 92 (1986). https://doi.org/10.1007/BF00250732
• R. T. Glassey, W. A. Strauss, Absence of shocks in an initially dilute collisionless plasma, Comm. Math. Phys. 113 (1987). https://doi.org/10.1007/BF01223511
• S. Wollman, An existence and uniqueness theorem for the Vlasov–Maxwell system, Comm. Pure Appl. Math. 37 (1984). https://doi.org/10.1002/cpa.3160370404
• R. J. DiPerna, P.-L. Lions, Global weak solutions of Vlasov–Maxwell systems, Comm. Pure Appl. Math. 42 (1989). https://doi.org/10.1002/cpa.3160420603
• J. Luk, R. M. Strain, A new continuation criterion for the relativistic Vlasov–Maxwell system, Comm. Math. Phys. 331 (2014). https://doi.org/10.1007/s00220-014-2108-8
• F. Bouchut, F. Golse, C. Pallard, Classical solutions and the Glassey–Strauss theorem for the 3D Vlasov–Maxwell system, Arch. Ration. Mech. Anal. 170 (2003). https://doi.org/10.1007/s00205-003-0265-6
• S. Klainerman, G. Staffilani, A new approach to study the Vlasov–Maxwell system, Commun. Pure Appl. Anal. 1 (2002). https://doi.org/10.3934/cpaa.2002.1.103
• X. Wang, Large data global solution of the 3D RVM system with cylindrical symmetry, arXiv:2203.01199 and arXiv:2607.14685 (2026). https://arxiv.org/abs/2607.14685v1

Motivation: hardness of the molecular ground-state energy with ordinary nuclei

Computing the ground-state energy of electrons in the Coulomb field of fixed nuclei is the basic problem of quantum chemistry. In quantum complexity theory, a problem is QMA-hard if every problem with polynomial-time quantum verification of a quantum witness (the quantum analogue of NP) reduces to it. Hardness was previously known for lattice models with magnetic fields, for continuum models with freely designed potentials, and for electronic structure restricted to a supplied finite orbital basis. None of these is the exact problem in which the external field comes only from point nuclei of charge one — hydrogen-like nuclei — and the energy is minimized over every antisymmetric many-electron wavefunction in the continuum. Two obstacles separate the known results from this problem: a designed potential need not be a sum of unit Coulomb wells, and a projected (finite-basis) energy only bounds the continuum infimum from above.

Timeline

• 1959 — Anderson's superexchange mechanism: virtual hopping through double occupancy produces Heisenberg exchange (Anderson 1959).
• 1965 / 1990 — Moser and Dacorogna–Moser: transporting volume forms by flows, later used here to place equal-mass nuclei (Moser 1965, Dacorogna–Moser 1990).
• 2009 — Schuch and Verstraete: QMA-completeness of a Hubbard model with local magnetic fields and a continuum realization with designed scalar and spin-dependent potentials (Nature Phys. 2009).
• 2017 — Piddock and Montanaro: singlet-pair mediators turning signed into positive (antiferromagnetic) exchange, and 2D lattice hardness (QIC 2017).
• 2018/2019 — Cubitt, Montanaro and Piddock: universal quantum Hamiltonians, including spatially sparse QMA-hard Heisenberg models with polynomial interaction scales (PNAS 2018, arXiv:1701.05182v4).
• 2022 — O'Gorman, Irani, Whitfield and Fefferman: QMA-completeness of electronic structure in a supplied finite basis, including a unit-point-charge construction; the complete-space question is left open (PRX Quantum 2022).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 24, 2026) claim QMA-hardness of the full continuum problem: one with binary-encoded nuclear charges, and QMA-hardness of continuum Coulomb energy with unit nuclear charges (this mission). Neither is peer reviewed, and the theorem is not formally verified.

Setting

An instance consists of $M\ge1$ pairwise distinct positions $R_\alpha\in\mathbb Q^3$ of nuclei of charge one, an electron number $N\ge1$ encoded in unary, and rational thresholds $a<b$ (signed binary numerators, positive binary denominators). The electronic Hamiltonian is

$$H=-\frac12\sum_{i=1}^N\Delta_{x_i}-\sum_{i=1}^N\sum_{\alpha=1}^M\frac1{|x_i-R_\alpha|}+\sum_{1\le i<j\le N}\frac1{|x_i-x_j|}$$

on $\mathcal H_N=\bigwedge^N\big(L^2(\mathbb R^3)\otimes\mathbb C^2\big)$, defined through its closed form on $\mathcal Q_N=H^1(\mathbb R^{3N};(\mathbb C^2)^{\otimes N})\cap\mathcal H_N$. Antisymmetry exchanges position and spin together and no spin sector is selected. $E_0=\inf\operatorname{spec}H$ equals the infimum of the form over normalized vectors of $\mathcal Q_N$. YES: $E_0\le a$; NO: $E_0\ge b$. Nuclear repulsion is omitted.

In Lean, unitGroundEnergy is that infimum (as an EReal) over normalized antisymmetric $H^1$ states with explicit square-integrable weak gradients; InQMA is defined by polynomial-time uniform $\{H,T,\mathrm{CNOT}\}$ circuit families with completeness $2/3$ and soundness $1/3$; QMAHard requires a deterministic polynomial-time (Turing-machine computable) many-one reduction from every QMA promise problem.

Formalization targets

Goal: QMA-hardness with unit nuclear charges

$$\textsf{UnitCoulomb}\ \text{is QMA-hard under deterministic polynomial-time many-one reductions},$$

for the promise problem whose valid instances have threshold separation $b-a\ge1$. This is Theorem 1 of the source in the form produced by its reduction ("threshold separation at least one"), which implies the stated precision $b-a\ge L^{-1}$. The goal is published on the platform with status Open.

Significance

The result itself. The theorem shows that the exact clamped-nucleus electronic ground-energy problem is QMA-hard even when all nuclei are protons (charge one), with no supplied basis, magnetic field, or extra potential, and with constant threshold separation. It makes no claim of membership in QMA, of a molecular spectral gap, or of a ground eigenvector. It implies the companion binary-charge theorem, whose input class is larger, while the companion's proof gives independent tools.

Formalizing it. The Lean statement fixes the input encoding, the variational ground energy, and the notion of QMA precisely. Its proof would need the QMA-completeness source (an external theorem), finite spin and Hubbard reductions, and continuum estimates for Coulomb operators (localization, complement gaps, Hardy-type form bounds), most of which is absent from Mathlib. The definitions are shared with the binary-charge mission.

Difficulty

Unit nuclei offer no independently adjustable charges, so the wells needed for a Hubbard model must be produced by the geometry of many nuclei alone; the construction first builds a nonnegative continuous charge density and then replaces it by equal-mass point charges via a measure-transport flow and cubature, with rational rounding. The replacement error is not small on arbitrary states; only its compression to smooth localized modes is small. The lower bound must hold for every antisymmetric state in every spin sector, which requires a uniform gap on the one-particle complement and careful handling of the long-range direct Coulomb repulsion.

Formalization scope

• Inputs are UnitCoulomb records (a list of rational positions, unary electron count, two binary rationals) with a self-delimiting bit encoding; validity requires $M,N\ge1$, distinct positions, positive denominators and $b-a\ge1$. Lowest-terms encoding of rationals is not required in Lean, a harmless relaxation.
• unitGroundEnergy is computed by toNuclearData with every charge equal to one, using the same Coulomb form as the binary-charge definitions.
• QMA verifiers use the gate set $\{H,T,\mathrm{CNOT}\}$, uniform generation by Turing.TM2ComputableInPolyTime, and a polynomial size bound; the reduction must be polynomial-time computable on the encodings.
• Needed infrastructure: a formal QMA-completeness source for Heisenberg models, perturbative reductions, Sobolev/Hardy and quadratic-form methods for Coulomb operators, measure transport (Moser flow), and cubature error bounds.

Selected references

• P. W. Anderson, New approach to the theory of superexchange interactions, Phys. Rev. 115 (1959), 2–13. https://doi.org/10.1103/PhysRev.115.2
• J. Moser, On the volume elements on a manifold, Trans. Amer. Math. Soc. 120 (1965), 286–294. https://doi.org/10.1090/S0002-9947-1965-0182927-5
• B. Dacorogna and J. Moser, On a partial differential equation involving the Jacobian determinant, Ann. Inst. H. Poincaré C 7 (1990), 1–26. https://www.numdam.org/item/AIHPC_1990__7_1_1_0/
• N. Schuch and F. Verstraete, Computational complexity of interacting electrons and fundamental limitations of density functional theory, Nature Phys. 5 (2009), 732–735. https://doi.org/10.1038/nphys1370
• S. Piddock and A. Montanaro, The complexity of antiferromagnetic interactions and 2D lattices, Quantum Inf. Comput. 17 (2017), 636–672. https://www.rintonpress.com/xxqic17/qic-17-78/0636-0672.pdf
• T. S. Cubitt, A. Montanaro and S. Piddock, Universal quantum Hamiltonians, Proc. Natl. Acad. Sci. USA 115 (2018), 9497–9502. https://doi.org/10.1073/pnas.1804949115
• B. O'Gorman, S. Irani, J. Whitfield and B. Fefferman, Intractability of electronic structure in a fixed basis, PRX Quantum 3 (2022), 020322. https://doi.org/10.1103/PRXQuantum.3.020322
• G. Teschl, Mathematical Methods in Quantum Mechanics, Graduate Studies in Mathematics 99, AMS, 2009. https://www.mat.univie.ac.at/~gerald/ftp/book-schroe/schroe.pdf
• OpenAI, Continuum Coulomb hardness with binary nuclear charges, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026.pdf
• OpenAI, QMA-hardness of continuum Coulomb energy with unit nuclear charges, OpenAI Math Release preprint, September 24, 2026 (Theorem 1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026.pdf

Motivation: how hard is the molecular ground-state energy?

Computing the ground-state energy of a molecule — electrons moving in the Coulomb field of fixed nuclei — is the central task of quantum chemistry. Quantum complexity theory asks whether it is hard even for a quantum computer: a problem is QMA-hard if every problem verifiable by a polynomial-time quantum verifier with a quantum witness reduces to it (QMA is the quantum analogue of NP). Many lattice and finite-basis versions of electronic structure are known to be QMA-complete, but those results either allow magnetic fields and designed potentials, or restrict the electrons to a supplied finite orbital basis. The exact problem — external field generated only by positive point nuclei, minimization over the full continuum of antisymmetric many-electron wavefunctions — needs a lower bound excluding every state outside any chosen orbital set, which projection arguments do not provide.

Timeline

• 1959 — Anderson's theory of superexchange: virtual double occupancy produces Heisenberg exchange between localized spins (Anderson 1959).
• 2007 — Liu, Christandl and Verstraete: QMA-completeness of $N$-representability (finite modes, Turing reductions) (PRL 2007).
• 2009 — Schuch and Verstraete: QMA-completeness of a Hubbard model with local magnetic fields, with a continuum realization using designed scalar and spin-dependent potentials (Nature Phys. 2009).
• 2013 — Whitfield, Love and Aspuru-Guzik survey complexity in electronic structure and the role of magnetic fields (PCCP 2013).
• 2017–2018 — Piddock and Montanaro: complexity of antiferromagnetic interactions on 2D lattices (QIC 17, 2017); Cubitt, Montanaro and Piddock: universal quantum Hamiltonians, including QMA-hard field-free Heisenberg models (PNAS 2018).
• 2022 — O'Gorman, Irani, Whitfield and Fefferman: QMA-completeness of electronic structure in a supplied finite basis, explicitly raising the complete-space question (PRX Quantum 2022).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 24, 2026) claim QMA-hardness of the exact continuum problem: Continuum Coulomb hardness with binary nuclear charges (this mission) and a companion with unit nuclear charges. Neither is peer reviewed, and the theorem is not formally verified.

Setting

An instance consists of $M\ge1$ pairwise distinct nuclear positions $R_\alpha\in\mathbb Q^3$, positive integer charges $Z_\alpha$ (encoded in binary), an electron number $N\ge1$ (encoded in unary), and rational thresholds $a<b$. The electronic Hamiltonian, in atomic units, is

$$H=-\frac12\sum_{\ell=1}^N\Delta_{x_\ell}-\sum_{\ell=1}^N\sum_{\alpha=1}^M\frac{Z_\alpha}{|x_\ell-R_\alpha|}+\sum_{1\le\ell<k\le N}\frac1{|x_\ell-x_k|}$$

on the antisymmetric space $\bigwedge^N L^2(\mathbb R^3;\mathbb C^2)$ (positions and spins permuted together), defined through its closed quadratic form on $H^1\cap\bigwedge^N L^2$. Let $E_0=\inf\operatorname{Spec}H$. YES instances have $E_0\le a$; NO instances have $E_0\ge b$. Nuclear repulsion is omitted (clamped-nucleus electronic energy) and all spin sectors are included.

In Lean, groundEnergy is the infimum (in EReal) of the Coulomb form over normalized antisymmetric $H^1$ states, given by explicit square-integrable values and weak gradients; QMA is defined through polynomial-time uniform families of $\{H, T, \mathrm{CNOT}\}$ circuits with acceptance $\ge2/3$ / $\le1/3$; QMAHard asks for a deterministic polynomial-time many-one reduction (as a Turing-machine-computable map on bit strings) from every QMA promise problem.

Formalization targets

Goal: QMA-hardness with binary charges

$$\textsf{BinaryCoulomb}\ \text{is QMA-hard under deterministic polynomial-time many-one reductions},$$

for the promise problem whose valid instances satisfy $b-a\ge1$. This is Theorem 1.1 of the source in its stronger form ("the reduction can produce instances with $b-a\ge1$"), which implies the stated precision $b-a\ge L^{-1}$. The goal is published on the platform with status Open.

Significance

The result itself. The theorem places the exact clamped-nuclei electronic ground-energy problem, with no supplied basis, field, or designed potential, among QMA-hard problems at inverse-polynomial (indeed constant) precision. It makes no claim of membership in QMA, of a spectral gap, or of hardness under bounded charges. The companion unit-charge theorem implies this one for the larger binary-charge input class; the present proof is independent and contributes certified exponential-accuracy eigenvalue computation and relative tunneling calibration for widely separated hydrogenic wells.

Formalizing it. A complete formalization would combine a QMA-completeness source theorem (Heisenberg models), finite spin and Hubbard reductions, and continuum many-body spectral estimates (Hardy inequality, localization, complement gaps) — a large but well-delimited body of mathematics, much of it absent from Mathlib. The precise Lean encoding of inputs and of QMA itself is reusable for other Hamiltonian-complexity missions.

Difficulty

Projecting $H$ onto chosen orbitals gives an upper bound on $E_0$ but says nothing about states outside the projection, so finite-basis hardness does not transfer NO instances. The construction must realize prescribed, exponentially small Hubbard hoppings using only point nuclei, with relative (not absolute) precision, and must certify one-well energies to exponential accuracy using polynomially many bits. Finally a lower bound for the full many-electron spectral infimum must hold for every fermionic state, in every spin sector.

Formalization scope

• Inputs are BinaryCoulomb records (list of rational positions with natural charges, unary electron count, two binary rationals) with an explicit self-delimiting bit encoding; validity requires $M,N\ge1$, distinct positions, positive denominators, positive charges, and $b-a\ge1$. Lowest-terms encoding is not required in Lean, a harmless relaxation.
• The state space is H1Vector n with antisymmetry under simultaneous permutation of positions and spins; groundEnergy is an EReal infimum over normalized states, which is the variational characterization of $\inf\operatorname{Spec}H$.
• QMA uses a fixed universal gate set $\{H,T,\mathrm{CNOT}\}$ and polynomial-time Turing-machine uniformity (Turing.TM2ComputableInPolyTime); the reduction must also be TM2ComputableInPolyTime.
• A trivial proof is excluded: YES/NO sets are disjoint by construction and the reduction must preserve both promises for every QMA problem.
• Needed infrastructure: a QMA-complete source (Kitaev-type local Hamiltonian / Heisenberg problem), perturbative gadgets, Hardy inequality, quadratic-form methods for Coulomb operators, and certified numerical analysis.

Selected references

• P. W. Anderson, New approach to the theory of superexchange interactions, Phys. Rev. 115 (1959), 2–13. https://doi.org/10.1103/PhysRev.115.2
• Y.-K. Liu, M. Christandl and F. Verstraete, Quantum computational complexity of the N-representability problem: QMA complete, Phys. Rev. Lett. 98 (2007), 110503. https://doi.org/10.1103/PhysRevLett.98.110503
• N. Schuch and F. Verstraete, Computational complexity of interacting electrons and fundamental limitations of density functional theory, Nature Phys. 5 (2009), 732–735. https://doi.org/10.1038/nphys1370
• J. D. Whitfield, P. J. Love and A. Aspuru-Guzik, Computational complexity in electronic structure, Phys. Chem. Chem. Phys. 15 (2013), 397–411. https://doi.org/10.1039/C2CP42695A
• S. Piddock and A. Montanaro, The complexity of antiferromagnetic interactions and 2D lattices, Quantum Inf. Comput. 17 (2017), 636–672.
• T. S. Cubitt, A. Montanaro and S. Piddock, Universal quantum Hamiltonians, Proc. Natl. Acad. Sci. USA 115 (2018), 9497–9502. https://doi.org/10.1073/pnas.1804949115
• B. O'Gorman, S. Irani, J. Whitfield and B. Fefferman, Intractability of electronic structure in a fixed basis, PRX Quantum 3 (2022), 020322. https://doi.org/10.1103/PRXQuantum.3.020322
• OpenAI, QMA-hardness of continuum Coulomb energy with unit nuclear charges, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026/QMA-hardness-of-continuum-Coulomb-energy-with-unit-nuclear-charges-September-24-2026.pdf
• OpenAI, Continuum Coulomb hardness with binary nuclear charges, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026/Continuum-Coulomb-hardness-with-binary-nuclear-charges-September-24-2026.pdf