Papers

This paper presents Peppy, an AI-assisted workflow for discovering tight, analytic convergence proofs for first-order optimization algorithms. Generic approaches to using LLMs to conduct mathematical research target an unspecified, broad spectrum of problems and sometimes use the Lean 4 proof assistant for formalization. On the other hand, Peppy leverages domain-specific knowledge more heavily and is thereby capable of constructing the proofs in a more structured manner, which allow a minimal and accessible verification through SymPy. We experimentally demonstrate through examples that Peppy provides a rigorous, practical, and reproducible paradigm for AI-assisted theorem synthesis in optimization. We further highlight its capability of closing several open problems on tight convergence analysis of first-order optimization algorithms, including conjectures for Nesterov's FGM. Overall, Peppy is designed to turn the art of optimization algorithm analysis into a science.

We introduce Neural Harmonic Measure Operator (NHMO), a neural solver for elliptic PDE problems on variable-shape domains. The harmonic measure of a domain is the boundary probability distribution that, integrated against any boundary data, returns the Dirichlet Laplace solution. It depends only on the geometry, not on the boundary data. NHMO parameterizes the density of this measure as a transformer-based boundary kernel supervised by Walk-on-Spheres exit samples, so one trained kernel handles different boundary values on a shape with no retraining. We extend it to Poisson via a classical decomposition, with an auxiliary network amortizing the source-induced correction and avoiding the singular volume quadrature that breaks direct evaluation. At inference, new boundary values and new sources both yield PDE solutions by re-integration against the fitted kernel and lift, with no retraining. NHMO improves over four prior baselines on the MCB-B 3D variable-shape Poisson benchmark across all five categories, and is competitive with major neural-operator baselines on a controlled 2D testbed.

Let $R$ be a compact discrete valuation ring and $G = R^d \rtimes \operatorname{GL}_d(R)$. We show that the central Fourier algebra $\operatorname{ZA}(G)$ is not amenable, reaffirming a conjecture of Alaghmandan and Spronk. Our methods reduce to studying the Fourier algebra of the commutative orbit hypergroup $H = R^d/\operatorname{GL}_d(R)$. Along the way, we also show that dual of any commutative orbit hypergroup $H$ is the hypergroup of the corresponding dual action, and this in turn shows that $\operatorname{A}(H) \cong \operatorname{L}^1(\widehat{H})$, which aligns with the classical setting.

We prove that the Zhang-Kawazumi invariant $\varphi(X)$ of a compact and connected Riemann surface $X$ of genus $g\ge 2$ is strictly larger than \[\frac{g(g+2)-(2g+1)H_g}{g-1},\] where $H_g=\sum_{k=1}^g \frac{1}{k}$ denotes the $g$-th harmonic number. If $X$ is hyperelliptic, we give the stronger bound $\varphi(X)>\frac{g}{2}(H_g-1)$. The proof relies on a new expression of $\varphi(X)$ in terms of a quadratic form on the space of smooth Hermitian matrix-valued functions on $X$, evaluated at certain projector matrices. As an arithmetic application, we deduce new lower bounds for the self-intersection number $\omega_a^2$ of the admissible adelic metrized canonical bundle $\omega_a$ of a smooth projective curve of genus $g\ge 2$ over a number field and hence new uniform height bounds in the Bogomolov conjecture.

We study exponential output-to-state stability (eOSS) of linear infinite-dimensional systems in Banach spaces with bounded output operators. It is shown that eOSS is equivalent to the existence of a coercive eOSS Lyapunov function in implication form. Also exponential detectability guarantees the existence of a coercive eOSS Lyapunov function in dissipation form and therefore eOSS. Counterexamples demonstrate that the converse implications fail in general: exponential zero-detectability does not imply eOSS, eOSS does not imply the existence of an eOSS Lyapunov function in dissipation form, which, in turn, does not imply exponential detectability. If the unstable subspace is finite-dimensional, zero-detectability implies exponential detectability and yields equivalent characterizations of eOSS. The results are illustrated with a parabolic equation.

Let $M$ be a compact Riemannian manifold, and let $G$ be a compact Lie group with bi-invariant metric. We show that the singular set of any stable stationary harmonic map $u : M \to G$ has Hausdorff codimension at least four. This is sharp.

We present an abstract framework for conservation and translation theorems between logical calculi. Unlike previous approaches, our setting does not require the underlying consequence relations to satisfy structural properties such as cut, allowing in particular for cut-free calculi. Moreover, we study translations between arbitrary calculi rather than only from a stable extension to the original calculus. Translations are formulated at the level of sequents by pairs of functions acting on antecedents and succedents, and the framework is developed for multi-succedent calculi while subsuming the single-succedent case. This yields a uniform treatment of classical results including negative translations, minimality theorems, Orevkov's conservation classes, and a characterisation of the least logic satisfying Kuroda's double negation theorem.

We classify abelian canonical covers of degree at most $8$ of smooth surfaces of minimal degree, and of $\mathbb P^2$ and Hirzebruch surfaces not embedded as surfaces of minimal degree. Let $\pi: X \longrightarrow W$ be an abelian canonical cover of a smooth surface of minimal degree $W$ with group $G$ and degree $n$. Degrees $n \le 4$ were classified earlier; we complete the picture for $5 \le n \le 8$: - No such covers exist if $n$ is prime and $n > 3$, nor if $G=\mathbb Z_8$. - For $G=\mathbb Z_6$, $\mathbb Z_2 \times \mathbb Z_2 \times \mathbb Z_2$ and $\mathbb Z_2 \times \mathbb Z_4$ we give the complete list of covers. Only $W =\mathbb P^2$, $\mathbb F_0$ and $\mathbb F_1$ arise. The list contains several families with unbounded $p_g$, most of them new; $X$ is smooth for general covers with $G=\mathbb Z_2 \times \mathbb Z_2 \times \mathbb Z_2$, but singular if $G=\mathbb Z_6$ and, with one exception, if $G=\mathbb Z_2 \times \mathbb Z_4$. When $W$ is $\mathbb P^2$ or a Hirzebruch surface not embedded as a surface of minimal degree, we show that abelian canonical covers exist only for $n = 2$ or for $G =\mathbb Z_2 \times \mathbb Z_2$, and we classify the latter completely: they form infinitely many families, most new, with unbounded $p_g$ and, most of them, with unbounded irregularity. The slopes $K^2/\chi$ of all these $X$ accumulate at $6$, at 8, and at $8\alpha/(\alpha +1)$ for every integer $\alpha \ge 2$. These results rest on more general ones, valid for $X$ normal, locally Gorenstein and of arbitrary dimension, and $W$ smooth with $p_g(W) = 0$: we determine which branch divisors of an abelian canonical cover must vanish, and, for canonical covers whose $\pi_*\mathcal O_X$ splits as a sum of line bundles, we describe the $\mathcal O_W$-module structure of $\pi_*\mathcal O_X$, computing it completely when $W$ is $\mathbb P^2$ or a Hirzebruch surface.

Lattice gauge theories are an important class of physical models with high-dimensional structured distributions that underpin first-principles calculations in particle, nuclear, and condensed-matter physics. Recent advances in generative modeling have opened new avenues for sampling Boltzmann distributions in lattice gauge theories, offering the potential to alleviate limitations of traditional Monte Carlo methods, including critical slowing down and topological freezing. However, generative samplers for lattice gauge theories are typically constructed in link space, where correlations become increasingly long-ranged toward weak coupling, posing a challenge for learning. Plaquettes provide a more natural representation, as the action is local in these variables. However, exact Bianchi constraints restrict them to a lower-dimensional manifold, complicating direct generative modeling. We introduce a multilevel normalizing-flow construction that samples directly in plaquette space while satisfying these constraints exactly. The key idea is a coarse-to fine factorization that transforms a globally coupled constraint problem into a sequence of local solves: at each refinement, every determined plaquette depends on at most four newly generated variables, while the size of the constraint problem remains independent of the lattice size. We validate the construction for $U(1)$ in two and four dimensions and for $SU(2)$ in two dimensions. Our multilevel Plaquette-Space Sampler (PSS) substantially outperforms link-space baselines, with the advantage increasing toward weak coupling, where the gauge coupling becomes small. This regime is particularly challenging for generative sampling and, in asymptotically free gauge theories, is relevant to continuum studies.

Least-squares residual minimization approximates a differential equation through an optimization problem. This paper investigates the conditions required to transition from stationary points and minimizing sequences of the residual functional to the exact solution. Starting from the classical orthogonality relation between the residual and the range of the linearized operator, we study how boundary conditions and parameterized variations determine what can be inferred about the residual at a stationary point. Smooth spurious critical points can occur even for well-posed problems; for linear equations, a compatibility condition yields an exact projection characterization. For a scalar conservation law with transonic boundary data, every minimizing sequence converges to a continuous function that does not solve the equation, even when a stationary entropy shock exists. We give conditions under which approaching this limit forces the parameter norms to diverge. A Hamilton–Jacobi example shows that a function can have zero residual without being the viscosity solution. Favorable results for a viscous model and uniformly convex Monge–Ampère critical points identify conditions that restore the corresponding implications. For piecewise-smooth trial families, the regularity needed to define the residual functional does not by itself justify the sampled gradient used in training. Moving residual jumps can contribute terms absent from that gradient; an explicit example has identically vanishing sampled gradients and a nonzero continuous derivative. Together, these results clarify what stationarity and sampled gradients imply about the residual, and under which conditions minimizing sequences lead to the intended solution.

Bell and Cover showed that an investor who multiplies the initial unit of capital by an independent uniform random variable on $(0,2)$, and then uses the log-optimal portfolio, wins a head-to-head wealth comparison with probability at least one half against every independently randomized competitor. We explain very simply how this result transfers to testing by betting: for any composite null $\mathcal P$ and simple alternative $Q$, denoting $E^*$ as the corresponding numeraire e-variable, we show that $UE^*$ exceeds any other e-variable $E$ with probability at least half. Interestingly, we show that this competitive optimality result is actually equivalent to the numeraire inequality $\mathbb E_Q[E/E^*]\leq1$, and in general randomization only helps the numeraire and fails to improve the competitive advantage of an arbitrary e-variable. Under optional stopping with or without knowledge of $U$, we emphasize a key distinction between e-process validity and competitive optimality. We also show that competitive optimality comes at the price of expected log wealth and power: thresholding $UE^*$ at $1/\alpha$ has sharp size at most $\alpha/2$, but the factor of two actually disappears under optional stopping. Even after correcting for this factor of two, the test is dominated in conditional rejection probability by randomizing the testing threshold (randomized Markov's inequality). Thus, Bell-Cover randomization is optimal for a specific competitive objective, at the cost of others.

Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.

For $n\ge5$, let $F\colon\mathbb{F}_2^n\to \mathbb{F}_2^n$ be almost perfect nonlinear and write $N=2^n$. It is proven that the linearity $\mathcal{L}(F)$ of $F$, i.e., the largest absolute Walsh coefficient of a nonzero component, is at most $N-6$. If $n$ is even, it is further proven that $\mathcal{L}(F)\le N-\sqrt N/4-2$. These bounds improve the general upper bound of $N-4$ in odd dimension and $N-6$ in even dimensions $n \geq 10$. It is further proven that, for each fixed $k$, the $k$-th largest absolute Walsh coefficient among nonzero components, counted with multiplicity, is at most $(1+O_k(2^{-n}))N/\sqrt{k}$ as $n\to\infty$. The second and fourth largest coefficients are at most $2\lfloor N/3\rfloor$ and $N/2$, respectively. Finally, a bound on the linearity in terms of the number $q$ of nonplateaued nonzero components is derived. In odd dimension, for $q>0$, we have $\mathcal{L}(F)^2\le N(1+\sqrt{q(N-1)})$, so that $\mathcal{L}(F)/N\to1$ implies $q/N\to1$. In even dimension, for every $1/2\le C<1$, the condition $q\le(4C-C^2-1)N/4+1$ implies $\mathcal{L}(F)\le CN$. In particular, $q\le3N/16+2$ implies $\mathcal{L}(F)\le N/2$.

With the recent advancements of neural compressors, explicitly incorporating perception constraints into the design of compression schemes has gained significant attention. Traditionally, these perception constraints ensure that the distribution of the reconstruction does not significantly deviate from the distribution of the source, thus attesting to the perceptual quality of the reconstruction. In this work, we uncover several perception constraints that are naturally present in task-aware compression. In particular, we consider a problem where the primary task is reconstruction and the secondary task is classification (i.e., a statistical test). We study this problem at varying levels of domain information available to us and discuss how to utilize the naturally emerging perception constraints to design rate-minimal compression schemes that also maximize the utility of our secondary task. We show that in this setting, if the decision boundaries of the classifier are ill-defined (mismatch) for our source distribution, then matching onto a target distribution enhances our classification accuracy.

In this paper we study the orbits of the automorphism group on a toroidal spherical variety. In the affine case, we prove that two points lie in the same orbit of the identity component if and only if the kernels of the homomorphisms from the divisor class group to their local divisor class groups coincide. These kernels are described in terms of $B$-stable prime divisors. For a smooth complete toroidal spherical variety, we obtain a similar criterion using the monoids generated by the classes of $B$-stable prime divisors that do not contain a given $G$-orbit.

In this paper we contribute to the study of compactness properties for algebraic structures. We prove two compactness theorems in the context of almost projective modules from $\lambda$-strongly compact and weakly compact, respectively.

We introduce power variations of critical Gaussian multiplicative chaos (GMC) along refining partitions in arbitrary dimension. Under suitable renormalisation, we prove uniform fractional moment bounds via Laplace transform estimates as well as stable convergence to supercritical GMCs. Together, these results provide a unified approach to regularity and spectral questions for critical chaos, yielding: (i) the sharp exponent for the logarithmic modulus of continuity, (ii) the existence of non-empty essential spectrum for critical Liouville quantum gravity surfaces; and (iii) an almost-sure quantitative Fourier decay.

We study numerical time integration for the motion of a charged particle in a strong magnetic field, focusing on the regime in which the fast gyration is not resolved by the time step. Standard Boris-type methods are structure preserving and accurate when the gyration is resolved, but their error constants deteriorate with increasing field strength; filtered Boris methods improve this behavior but may suffer from singularities and resonance-induced error blow-up. In this work we consider the case of a constant strong magnetic field and derive a broad family of one-step exponential integrators from the variation-of-constants formula, formulated in terms of matrix-valued filter functions. This framework includes existing filtered Boris variants and permits the construction of schemes with uniformly bounded filters. Using a discrete variation-of-constants representation together with summation-by-parts arguments, we establish error bounds whose constants are independent of the magnetic field strength and characterize the filter conditions required for first- and second-order accuracy. In particular, we show that bounded filters avoid resonance blow-up and allow arbitrary time steps, at the cost of a controlled order reduction near resonant frequencies. Numerical experiments confirm the predicted convergence behavior, the different accuracy of position and velocity components, and the role of the leading error terms across a wide range of step-size-field-strength products.

In this paper, we complete the computation of the global log canonical thresholds of Burniat surfaces. Additionally, we determine the global log canonical thresholds for certain infinite families of surfaces of general type, constructed as $ \mathbb{Z}_2^n $-covers of $\mathbb{P}^2$ or $\mathbb{P}^1 \times \mathbb{P}^1$.

In this work, we establish a sharp logarithmic Choquard inequality by combining Beckner's entropy inequality with the sharp Pitt-type inequality. Motivated by this estimate, we classify the positive classical solutions, in a suitable integrability class, of the critical logarithmic Choquard problem \[ \mathcal{L}_\Delta u = \sigma u + \frac{1}{\|u\|_2^2} \left(G_{\ln}(u)-\frac{4}{N}\int_{\mathbb{R}^N}u^2\ln u\,dx\right)u \qquad\text{in }\mathbb{R}^N, \] where $\sigma\in\mathbb{R}$, $N\geq 1$, $\mathcal{L}_\Delta$ is the logarithmic Laplacian, and $G_{\ln}(u)=\ln(1/|x|^4)*u^2$. We construct explicit solutions as limits of critical fractional Choquard bubbles and prove that every positive classical solution in the prescribed class has the form \[ u_{\sigma,t}(x) = e^{\frac{N}{4}(\sigma-B_{N,\mathcal{L}})} B_{N,0}\left(\frac{t}{t^2+|x-x_0|^2}\right)^{N/2}, \qquad t>0,\quad x_0\in\mathbb{R}^N, \] where \[ B_{N,0} =\left(\frac{\Gamma(N)}{\pi^{N/2}\Gamma(N/2)}\right)^{1/2}, \qquad B_{N,\mathcal{L}} =2\ln 2+4\psi(N/2)-2\psi(N)+\frac{4}{N}\ln B_{N,0}. \]

We study the sharp-interface limit of the fractional Allen–Cahn equation in $\R^n$, $n\geq 2$, in the strongly nonlocal regime $s\in(0,\frac12)$, for initial data consisting of finitely many nested transition layers. We identify a coupled geometric law for the motion of the resulting fronts: each velocity contains fractional mean curvature and a nonlocal interaction potential generated by the other fronts. These interactions persist while the fronts remain separated, in contrast to the independent motion in the critical regime $s=\frac12$. Assuming that the coupled law admits a smooth evolution with strictly nested sets on a given time interval, we prove that the Allen–Cahn solutions converge locally uniformly away from the moving fronts to the corresponding integer-valued phases.

Interior-point methods (IPMs) are among the most widely used algorithms for constrained optimization, yet their Newton-based search directions require costly second-order information and large linear-system solves. Learning to optimize offers cheaper updates learned from data, but the singular behavior of logarithmic barriers near constraint boundaries makes IPMs highly sensitive to perturbations, complicating both warm starting and learning reliable updates. We introduce pdLIP, an IPM for smooth nonlinear programs that integrates learned preconditioning with pdProj, an all-shifted primal-dual projected-search IPM. A shared coordinate-wise recurrent network predicts a positive diagonal preconditioner that scales the right-hand side of the reduced Newton system for the primal step, and the remaining slack and multiplier directions are recovered analytically. The learned iterations avoid Hessian evaluations and Newton-system solves, using only first-order and coordinate-wise operations amenable to GPU parallelization. Training is self-supervised, with a loss based on a penalty-barrier merit function and the residual of perturbed optimality conditions, requiring neither target directions nor precomputed solutions. Primal and dual shifts mitigate the barrier's sensitivity to perturbations near constraint boundaries, enabling effective warm starting. Across four classes of 200-dimensional convex and nonconvex constrained problems, pdLIP warm starts reduce pdProj refinement iterations by 63-67% compared with cold starts at the same KKT residual tolerance of $10^{-8}$, with negligible warm-start generation cost relative to the subsequent pdProj solve. Improvements persist on box-constrained QPs with 1000 variables and extend to applications including portfolio optimization, support vector machines, and a nonlinear control example.

We study the problem of learning a sparse quantum state, an $n$-qubit quantum state whose density matrix has at most $s$ nonzero matrix entries in an unknown product basis. While such states admit compact classical descriptions, they can carry long-range entanglement that prevents reconstruction from local reduced density matrices alone. Therefore, previous learning approaches addressed such long-range-entangled states using many entangling gates to extract the necessary information. In this work, we show that sparse states can nevertheless be efficiently learned using only single-qubit measurements. Specifically, when the sparsity $s$ is constant, our algorithm can learn sparse states from single-qubit measurements with polynomial sample complexity and classical computational complexity. When $s$ grows polynomially with $n$, sparse states can still be learned from single-qubit measurements with polynomial sample complexity, although efficient classical computation is not guaranteed in general. In this regime, however, the classical computational complexity becomes quasipolynomial when the state is sparse in an unknown basis that is a product of a known fixed finite set of single-qubit bases (e.g., eigenbases of Pauli operators). These results establish efficient learning of sparse states with long-range entanglement without entangling gates, and the single-qubit measurement requirements make our algorithms compatible with current quantum devices.

While structure-preserving methods for the forward simulation of Hamiltonian systems are well established, the mathematical foundations of their data assimilation and filtering counterparts remain comparatively less developed, particularly regarding rigorous accuracy guarantees. To address this gap, we propose an online filtering algorithm to reconstruct an unknown function $u^\dagger$ from finitely many measurements, assuming that $u^\dagger$ solves a parametric Hamiltonian PDE with unknown inputs. The method uses low-dimensional symplectic approximation spaces that evolve in time according to the PDE model and informed by the measurement data. The method can also be coupled with a dynamical sensor-placement strategy designed to optimize reconstruction stability. We derive error bounds in terms of stability and best approximation, and show that the reconstruction remains in a symplectic space and preserves energy up to the approximation error. Numerical experiments demonstrate the effectiveness of the method and the benefits of dynamic over static sensor placement.

The study of heavenly abelian varieties is motivated by a question of Ihara. When an elliptic curve $E/K$ is heavenly at $\ell$, the extension $K(E[\ell^\infty])/K(\mu_\ell^\infty)$ is pro-$\ell$ and unramified away from $\ell$. These are the same arithmetic conditions as the fixed field of the kernel attached to pro-$\ell$ étale covers of the projective line over $K$ minus three points. In this paper we study heavenly elliptic curves defined over cubic number fields. Following the work on McLeman and Rasmussen in the quadratic case, we find that there is a wider range of possible behaviors for the trace of a balanced elliptic curve in the cubic case. In this setting, we introduce a further distinction between balanced and totally balanced curves. With this, we show that trace of the representation on the $\ell$-torsion for totally balanced elliptic curves is non-surjective. We also compute a bound on primes $\ell$ after which any heavenly elliptic curve defined over a cubic number field must be balanced. Finally we compare the trace behavior of totally balanced elliptic curves with CM elliptic curves.

We extend Gualtieri's deformation theorem for generalized complex structures on exact Courant algebroids to the more general class of $\mathcal{G}$-flat transitive Courant algebroids. Our approach relies on the framework of tame Fréchet spaces and Hamilton's Nash-Moser (implicit function) theorem. As an important step of the proof of our deformation theorem, we endow the group of autoequivalences of a $\mathcal{G}$-flat transitive Courant algebroid with a tame Fréchet Lie group structure and show that there exists a tame subgroup of exact autoequivalences, whose infinitesimal action is by inner derivations.

Imagine there are $n$ cars lined up along a one-way street containing $n$ spots. Each car contains a group of friends, including a reluctant driver. Each car has a preferred spot and cars enter one by one. The cars drive to their preferred spot and if it is empty park there. If it is not empty, a friend in the back yells out “Hey! You should have driven faster!". Frustrated by this, the driver continues down the road until they find the last unoccupied spot (if one exists) and parks there. We say a sequence $(a_1,a_2,\dots, a_n)$ of preferred spots is a frustrated parking function if all cars can park under this rule. In this paper, we study the enumerative properties of frustrated parking functions. In particular, we show that the number of frustrated parking functions of length $n$ is $(2n-1)!!$. This is done by associating frustrated parking functions with height labeled Dyck paths. Using this association, we are then able to better understand the sets of lucky cars and lucky spots for frustrated parking functions. We show that the frustrated parking functions of length $n$ where the first $k$ cars (or first $k$ spots) are lucky is given by $k!S(n,k)$ where $S(n,k)$ is the Stirling number of the second kind. This in turn implies that the number of frustrated parking functions where once a car (or spot) is unlucky, the remaining cars (or spots) are unlucky is counted by the $n^{th}$ Fubini number. We also show that the number of frustrated parking functions with $k$ lucky cars (or spots) is given by the second order Eulerian number.

We build upon recent developments in high-order spline-based geometric methods for the three-dimensional initial boundary value problem of Maxwell's equations. Previous schemes were limited to single-patch geometries. To address the computational challenges associated with inverting mass matrices in multi-patch settings, we extend existing techniques for 0-forms mass and stiffness matrices to 1-forms mass matrices. Our approach leverages the tensor-product structure of spline spaces to construct a spectrally equivalent preconditioner for the 1-forms mass matrices. Specifically, we design an efficient preconditioner for single-patch domains that is robust with respect to both mesh size and spline degree. In the multi-patch case, this methodology is extended by integrating the single-patch preconditioner with an additive Schwarz approach, ensuring robustness and scalability with respect to the number of patches. We analyze the computational complexity of the proposed preconditioner and validate its robustness and efficiency through comprehensive numerical experiments.

We prove that for every choice of four positive masses and every cyclic ordering of the bodies there is exactly one strictly convex planar central configuration with that ordering, up to similarity. This answers Problem 10 in the list of Albouy, Cabral and Santos, which Santoprete calls the Simó-Yoccoz conjecture. The main step is a uniform lower bound for the Hessian at convex central configurations: it is at least one quarter of its radial part, which vanishes only on translations and rotations. Dziobek's relations turn the indefinite part of the Hessian into a negative multiple of a square, and a Cauchy-Schwarz argument bounds this term by the radial part times the trace of an explicit $2\times 2$ matrix in which the masses do not appear. We prove that this trace is less than 3/4 by interval arithmetic on the three-dimensional set of normalized convex central configurations, in the coordinates of Corbera, Cors and Roberts. Uniqueness then follows by a covering argument from the case of four equal masses. The computation has been repeated with a second, independently written program. The Hessian bound and the uniqueness theorem, including the computation, have been formalized in the Lean proof assistant and checked by its kernel, using only the standard axioms. As consequences, every degenerate four-body central configuration is concave, the convex central configuration depends analytically on the masses, and the known symmetry theorems for kites, isosceles trapezoids and rhombi follow in a few lines. The analytic dependence and the symmetry theorems are also formalized.

We study acceleration of stochastic first-order methods for monotone Lipschitz inclusions with a fixed number of oracle queries per iteration, measured by the expected squared residual. Existing methods either have suboptimal oracle complexity, require an increasing number of oracle queries per iteration, or both. Under same-sample oracle access and mean-square Lipschitz stochastic noise, we develop variance-reduced anchored forward-backward (VRAF), an anytime composite method that makes two oracle queries per iteration. VRAF attains the first log-free $O(1/\epsilon)$ complexity under these oracle assumptions and hence the optimal $O(\sigma^2/\epsilon)$ variance dependence. This, however, leaves open whether the optimal $O(1/\sqrt{\epsilon})$ deterministic term can also be attained. We establish an impossibility result by extending the lower bound of Foster et al. (2019) to stochastic oracles permitting repeated queries to sampled stochastic operators, showing that $O(LD/\sqrt{\epsilon}+\sigma^2/\epsilon)$ oracle complexity is unattainable in general. We therefore develop recentered regularized stochastic extragradient (RRSEG), which attains the near-optimal oracle complexity previously achievable only with an increasing number of queries per iteration, while using a fixed number of queries.