Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A learner who minimizes a regularized population risk
usually has access to only through an i.i.d. sample , and so works with the empirical risk instead. The question this mission formalizes is how well the first-order behaviour of reflects that of when the loss is neither smooth nor convex. This matters because the algorithms used in practice for such problems (stochastic subgradient, proximal point and Gauss–Newton methods) find only approximately stationary points, and a uniform estimate of the gap between empirical and population stationarity tells one when further optimization of the empirical problem stops improving the population one.
For convex losses with strongly convex regularization, Shalev-Shwartz, Shamir, Srebro and Sridharan (COLT 2009) showed that the regularized empirical minimizer is stable and generalizes at a dimension-free rate. For smooth nonconvex losses, Mei, Bai and Montanari (Ann. Statist. 2018) and Foster, Sekhari and Sridharan (NeurIPS 2018) proved uniform convergence of gradients. For nonsmooth nonconvex losses, pointwise convergence of the stationarity measure was known, but uniform results were asymptotic and needed extra structure, because is highly discontinuous. Davis and Drusvyatskiy (arXiv:1810.07590, Mathematics of Operations Research 2022) replace it by a smoothed measure, the gradient of a Moreau-type envelope, and prove finite-sample uniform bounds for it. The losses covered are the weakly convex ones: phase retrieval, blind deconvolution, robust PCA, censored block models, conditional value-at-risk and sparse dictionary learning all fit (Table 1 of the paper).
Fix a finite-dimensional real normed space with norm and dual norm . Extended-valued functions are described by their domain and their values there.
A Legendre function is proper, closed and strictly convex, differentiable on the nonempty interior of its domain, and its gradient norm blows up at the boundary of the domain. It induces the Bregman divergence
and its symmetrization . For , . A function is -weakly convex relative to if is convex, and compatible with if . For the Φ-proximal map and Φ-envelope are
The standing assumptions are: (A1) is Legendre, compatible with , and on ; (A2) for a.e. , is -weakly convex relative to and bounded below; (A3) with and . Finally for an independent Rademacher sign , and is its Fenchel conjugate.
For every , , and , with probability at least ,
where is the covering number of in the metric . If is twice differentiable, the same probability bounds the event in the local dual norm.
The result gives a sample size beyond which approximate stationarity of the empirical problem certifies approximate stationarity of the population problem, uniformly over a region, with an explicit dependence on the sample size and on the covering number of the region. Because the graph of the proximal map is linearly isomorphic to the graph of the subdifferential, it also bounds the Hausdorff distance between and (Theorem 4.5 of the paper, not part of this mission). The Bregman setting covers non-Euclidean geometries (an -setup) and losses that are only locally Lipschitz with polynomial growth. Theorem 4.2 is reusable on its own: it is a McDiarmid inequality for unbounded, light-tailed differences.
The paper's proofs are complete; nothing here is open. None of the statements has been formalized before. Mathlib has the Fréchet derivative, product measures, cumulant generating functions and convexity, but no Legendre functions, Bregman proximal maps or envelopes, and no McDiarmid inequality with data-dependent differences; the platform has McDiarmid only with constant differences.
The naive route, McDiarmid's inequality applied to , needs a bounded difference constant, and the stability estimate (4.1) gives only , which is unbounded unless the data are. The concentration step therefore needs a version of McDiarmid's inequality whose differences are random. A second obstacle is that the empirical objects are random sets: proving that the proximal points are single-valued, interior, and measurable in the sample is a step the paper takes for granted. Third, uniformity over comes through Lemma 4.3 in the mirror metric , not in the norm of .
The space is a finite-dimensional real normed space ; gradients are Fréchet derivatives, the dual norm is the operator norm, and is the second Fréchet derivative, a map . Extended-valued functions are pairs (domain, real values), so no extended-real arithmetic occurs. Proximal maps are sets of minimizers; envelopes are real infima, used only where Theorem 3.1 guarantees attainment. "With probability " is an outer-measure bound on the failure set under . The covering number is replaced by the size of an arbitrary finite -net fixed before the sample, and by for an arbitrary with integrable; both replacements are equivalent to the page. Hypotheses the paper uses without stating are explicit: , , nonempty and convex, measurable and integrable, closedness of and of , bounded below; the second display of the goal assumes and an invertible Hessian on . Theorem 4.1 is read, as its proof is, with and the proximal points at .
A pointwise version (fixed ), a version where the net may depend on the sample, a bound for one fixed , or the Euclidean case alone would each be a strictly weaker theorem and does not close the goal.
A complete development needs: Legendre-function theory (coercivity of , interiority of Bregman proximal points), Danskin-type differentiation of the envelope, measurability of argmin maps, the extended McDiarmid inequality, and a covering/union bound. The McDiarmid extension and the Bregman proximal-point lemmas are reusable well beyond this paper. Proofs of the milestones, sanity instances of (A1)–(A3), and intermediate lemmas from the paper's proofs are all welcome.
The state of a finite-dimensional quantum system is a density: a positive semidefinite matrix of trace one. Under coherent (Hamiltonian) control the evolution is unitary, , and preserves the eigenvalues of . Even with full unitary control, a state can therefore only be moved within its unitary orbit. A mixed state cannot be purified, and a pure state cannot be made mixed. Dissipation, modelled by Lindblad generators (Gorini–Kossakowski–Sudarshan 1976, Lindblad 1976), is what breaks these spectral invariants. Engineered dissipation is a standard tool for state preparation (Verstraete–Wolf–Cirac 2009).
This raises a basic control question: how much dissipation must be added to full unitary control before every state can be steered to every other state? Cai, Govindarajan and Junge (arXiv:2504.04883v2) answer it for qubits. One amplitude-damping jump and one dephasing operator, both acting on a single qubit, suffice.
Timeline.
Let be the space of qubits, with computational basis , . A superoperator is a linear map on -qubit matrices. Densities form the set .
For an operator , the Lindblad generator with rate is
For every , is a quantum channel.
Fix a resource set of operators with . The closed class is the smallest closed set of superoperators with three properties:
generates a Hörmander system if the real Lie algebra generated by the anti-Hermitian part of contains , the traceless anti-Hermitian matrices. A set of superoperators is transitive if for all some satisfies . The range of is .
On one qubit, , is the amplitude-damping jump, and keeps the diagonal of a matrix and deletes the rest. The replacer channel is , and .
If generates a Hörmander system on and
then
The goal asserts reachability only. It places no bound on time or on the number of compositions.
The result. Full unitary control alone cannot change the spectrum of a state. Theorem 2.12 shows that two dissipative resources acting on one qubit already remove every obstruction. This is close to optimal: Proposition 2.7 of the paper shows that self-adjoint jumps alone produce only unital channels, which fix the maximally mixed state, so at least one non-self-adjoint resource is necessary. The result also needs no convexity. The class contains genuine Markovian semigroups, their compositions and their limits, but no mixtures. The surrounding statements are reusable on their own:
Formalizing it. The paper's proof is short, but several steps are stated without detail: "by assumption", "using the conjugation trick and products", and Chow's theorem cited for a semigroup rather than a group. A formal proof fixes exactly what the closure (CL) contributes. It supplies the negative-time unitaries (milestone 1) and the conditional expectations and (milestones 4–6), none of which is of the form . No machine-checked proof of these statements is known (a search of the Prove2Me library in October 2026 found none). Mathlib has the matrix exponential, the operator norm on superoperators and Lie subalgebras. It has neither Chow's theorem nor the correspondence between Lie subalgebras and connected subgroups of .
The one hard step is milestone 1. (UN) supplies only the forward flows , , of the directions in the span of . The Hörmander condition is a statement about the Lie algebra they generate, while the class is a semigroup closed under limits. The naive argument applies the Lie-algebra/Lie-group correspondence directly, but that correspondence speaks about the group generated by the flows , . The class contains only nonnegative times and their compositions and limits, so the step from the generated group to the closed semigroup is exactly what has to be supplied.
The remaining milestones are explicit matrix analysis: exponentials of explicit superoperators on one qubit and their limits as , and register swaps. Milestone 7 has two halves. The inclusion is the construction. The inclusion requires every element of the closed class, limits included, to be positive and trace-preserving.
Carrier. The basis of is indexed by bit strings Fin k → Bool, with false . Operators are complex matrices on this index set. Superoperators are continuous -linear maps with the operator norm over the -operator norm on matrices. In finite dimension every norm gives the same topology, so closedness and limits do not depend on this choice. Exponentials are NormedSpace.exp on matrices and on superoperators. Milestones 3 and 4 are stated on matrices indexed by Fin 2, with basis order .
The class. is the intersection of all closed sets with (UN), (JU) and (CO). A formalization in which some class with these properties is merely assumed to exist would make the goal trivial (take all superoperators), and is ruled out. Likewise, the Hörmander hypothesis is containment of in the generated real Lie algebra, not in the span of .
Conventions committed to.
Infrastructure needed.
The first two are reusable well beyond this mission. Proofs of individual milestones, and of general lemmas on Lindblad semigroups, are welcome.
A permutation of in the sense of Erdős and Graham is a one-sided arrangement in which every integer appears exactly once. Erdős Problem 195 (erdosproblems.com/195) asks for the largest such that every such arrangement contains a monotone -term arithmetic progression: indices for which is an increasing or a decreasing arithmetic progression. The question sits in the Ramsey-type study of how much arithmetic structure an ordering is forced to preserve, alongside its companion Problem 196 for permutations of .
Timeline of the known results:
The answer to Problem 195 is therefore or , and it is exactly when some permutation of avoids monotone 4-term progressions.
A permutation of is a bijection . A list of values is an arithmetic progression of length if it equals or the same list reversed. The function has a monotone -AP if there are indices such that is an arithmetic progression of length . For a bijection the common difference is automatically nonzero when .
Auxiliary objects used by the milestones:
Together with the known bounds this is equivalent to the answer to Problem 195 being . A disproof would show that the answer is .
and the reduction: the supremum in the formal-conjectures statement equals iff the goal holds.
The -orders are strict total orders with no monotone 3-term progression that satisfy (Star). They have no endpoints when is not eventually constant. In every -order, a word listed in reverse order is safe. Conversely, a least element blocks every exhaustive chain of safe words, and the two's-complement order has least element .
A proof of the goal resolves Problem 195, determines the answer as , and completes the classification of monotone progressions in one-sided permutations of and . A disproof gives the answer and is the first known statement separating the two problems. The formal-conjectures repository (195.lean) records the problem as open with an unspecified answer. The literature milestones have pen-and-paper proofs. Among them, only Ho's theorem for has a machine-checked proof, in an external repository, so porting it is part of the work.
The natural first attempt transfers Ho's construction for to . Ho's argument builds the permutation as a limit of finite safe words. Each extension step uses that all values are nonnegative: for a progression with and not yet placed, the bound controls which elements are forced. On this bound is lost. With the two's-complement completion order the obstruction is concrete: is the least element, and once it is placed no later element can be the maximum or minimum of a safe word, so no chain of safe words can exhaust . Any approach along these lines must therefore change the completion order between stages, for example through orders without endpoints, or use a different construction entirely.
Permutations are f : ℕ ≃ ℤ. HasMonotoneAP, ListIsAPOfLength and ListIsAPOfLengthWith copy the formal-conjectures definitions verbatim, so the goal and the reduction milestone use the same objects as Erdos195.erdos_195. Progressions may be listed forwards or backwards, which covers increasing and decreasing ones. A zero common difference never arises because f is injective. Digits are two's-complement digits x / 2^k % 2 with floor division, and ν₂ is padicValInt 2. Safe quantifies over all integers a and all nonzero r of either sign. Everything lives in the namespace Erdos195.
The development needs only Mathlib's integers, lists and -adic valuations. The -order lemmas and the completion lemmas are reusable for related arrangement problems, including Problem 196 and doubly infinite variants. Contributions are welcome on the literature milestones (in particular a port of Ho's Lean proof), on new orders with no endpoints, and on the goal in either direction.
ErdosProblems/195.lean.In multi-agent reinforcement learning several agents act in a shared, changing environment, each pursuing its own reward. The standard model is the Markov game (stochastic game), going back to Shapley (1953). When agents learn from experience rather than from a known model, the natural target is an equilibrium of the game, and the natural question is how many episodes of play are needed to find one.
Before V-learning, sample-efficient algorithms for general-sum Markov games were centralized and model-based: they estimated quantities indexed by the joint action, so their sample complexity grew with , exponentially in the number of players . This is the curse of multiagents. Jin, Liu, Wang and Yu (arXiv:2110.14555, journal version in Mathematics of Operations Research, 2024) introduced V-learning, in which every agent runs its own simple algorithm, sees only its own reward and the states, and never needs the other agents' actions. Theorem 6 of the paper shows that the agents' combined output is an approximate coarse correlated equilibrium (CCE) after a number of episodes polynomial in , and only.
Timeline:
A tabular episodic -player Markov game has states, episodes of steps, and actions for player ; . At step in state the players choose actions simultaneously, forming a joint action ; player receives the deterministic reward , and the next state is drawn from . Every episode starts at a fixed state .
A joint policy may be correlated: the players share a random seed. is player 's expected total reward. The best response value is the largest value player can obtain by switching to a policy of its own, independent of the shared seed, while the others keep playing . A joint policy is an -CCE if .
V-learning (Algorithm 1). Each player keeps, for every state and step , a visit count , a value estimate and an adversarial bandit algorithm. After visiting at step for the -th time it updates
with and a bonus , and feeds the loss of its own action to the -th bandit, whose next strategy becomes the policy at . The weights express as a weighted average of past updates.
The bandit subroutine must satisfy Assumption 1: against any adaptive adversary with noisy, conditionally unbiased feedback, with probability at least the -weighted regret after rounds is at most , where is non-decreasing in the number of arms and has a partial-sum upper bound concave in .
The output policy (Algorithm 3) samples an episode index uniformly from ; at each step, in state with earlier visits in episodes , it samples with probability , sets , and plays the policies the players held at the beginning of episode . For the CCE all players use the same sample (shared seed, §5.1).
With and bonuses satisfying for , with probability at least
The goal leaves the bandit algorithm abstract: it holds for every subroutine satisfying Assumption 1.
Two further steps of the proof of Theorem 6 are included as items without milestone status: the one-step recursion of (p. 23) and the pigeonhole bound on the summed bonus terms (pp. 23–24).
With the FTRL subroutine of the paper (Corollary 19: ), Theorem 6 gives an -CCE after episodes, against for the earlier centralized method. The same analysis, with a swap-regret subroutine, gives correlated equilibria (Theorem 7) and, specialized to two players with opposite rewards, Nash equilibria of zero-sum games (Theorem 5). The algorithm is decentralized: each agent's computation depends only on the visited states and its own actions and rewards.
The result is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization adds a precise statement of what "independent learning finds a CCE" means for non-Markov, history-dependent output policies, and of the adversary class Assumption 1 must cover for the reduction from the Markov game to the bandits to go through. It also makes explicit the boundary cases the paper leaves implicit (first visits, the last step, the initialization of ).
The deterministic steps (Lemmas 10–11, the recursion and the pigeonhole bound) are algebra on weighted sums. The difficulty is probabilistic. Lemma 12 must view each -bandit as playing against an adversary formed by the rest of the run: the other players, the transitions and the player's own other bandits, all adapted to the past. Lemmas 13 and 14 need concentration of -weighted martingale sums over random visit times, uniformly over all states, steps, episodes and players.
The best response is the other obstacle. The output policy is not Markov: it carries a latent episode index. The opponent of may use the whole history of states and joint actions, and the best response to a non-Markov policy is not given by a Bellman equation. Lemma 13's step (v) handles this; the obvious per-state argument does not apply.
Everything is finite and real-valued. States, players, actions, steps and episodes are Fin types; steps and episodes are 0-based, so the cap is H - h. The bandit rule is a deterministic function from the feedback history to a probability vector, starting uniform. The adversaries of Assumption 1 range over a finitary class: private randomness in an arbitrary finite type, losses chosen from the past before the learner's action, and conditionally unbiased feedback in . The training law is a finite product of policy and transition probabilities, and every probability is a finite sum over episode sequences. The best response is a supremum over deterministic history-dependent deviations, taken outside the average over the output policy's initial index. and are read with a universal lower constant before every instance and an -constant depending only on the upper constant .
Added hypotheses, each disclosed in its item: nonnegative bonuses; ; per-player bandit rules sharing one ; in the pigeonhole step and the summed-gap milestone; in milestone 6, whose printed form is false without it. The output policy's convention at a first visit () keeps the current index and plays the uniform initial policy.
Two formalizations would trivialize the goal and are ruled out: an Assumption 1 that no algorithm satisfies (a sorry-free check shows every valid rule satisfies it with ), and a best response averaged per latent index or restricted to Markov deviations.
Needed infrastructure: weighted martingale concentration (Azuma–Hoeffding is on the platform), finite-sum manipulation of the training law, and Jensen's inequality for concave functions. Contributions to any milestone are welcome; the deterministic milestones 1, 2 and 6, and the recursion and pigeonhole steps, are independent of the probabilistic ones.
Several problems in machine learning and game theory are optimization problems over probability measures. Training a wide two-layer neural network can be viewed as minimizing a functional of the distribution of the network's parameters (Mei, Montanari, Nguyen, PNAS 2018; Hu, Ren, Šiška, Szpruch, arXiv:1905.07769). Adding a relative-entropy penalty makes the problem strictly convex in the density and connects its minimizers to the invariant measures of Langevin-type diffusions, the mean-field Langevin dynamics. The first-order condition for the unconstrained problem is Hu et al., Proposition 2.4.
Conforti, Kazeykina and Ren (arXiv:2004.02457v2) add a random environment: a variable with a fixed law that every player observes, such as the time index in a dynamic game or a shared signal. The strategies are then probability measures on whose -marginal is prescribed. Their Theorem 3.1 extends the first-order condition to this constrained problem. The introduction names it "one of our main contributions": it gives the necessary condition for Nash equilibria of games on a random environment (Corollary 3.3), and it identifies the invariant measure of the mean-field Langevin system studied in the rest of the paper.
Let be a Polish space with a probability measure , and let . Write and . The strategy set is
the probability measures on with finite -th moment and -marginal . By disintegration, .
A function has a linear functional derivative if for all
Assumption 2.1 asks that have such a derivative, that and be continuous for the -Wasserstein distance , that be continuously differentiable in , and that .
The regularizer is the relative entropy with respect to : if has density with respect to , then , and otherwise. For the objective is
If , then has a density which, for -a.e. , is positive with differentiable and
Conversely, if is also convex on , every satisfying (3.1) minimizes over . The goal states both directions, as printed.
Theorem 3.1 says that each fibre of an entropy-regularized minimizer is a Gibbs measure, . In the paper this yields the Nash-equilibrium condition (3.2) for -player games on a random environment, the uniqueness of equilibria under a monotonicity condition (Corollary 3.4), and the identification of the stationary measures of the mean-field Langevin system (2.2) with these equilibria, the basis of the convergence results (Theorems 3.8–3.12). For a one-player problem it is the optimality condition behind gradient-descent training of mean-field neural networks with an environment variable.
The result is proved in the paper; it is not formalized anywhere known. The mission produces the first machine-checked first-order condition for optimization over probability measures, with or without a marginal constraint, and the supporting objects: the strategy set , the linear functional derivative, and relative entropy with respect to the infinite reference measure . The unconstrained case ( a point) is a special case.
The sufficiency direction is two convexity inequalities and a cancellation of the -dependent constants, which uses the common marginal . The necessity direction is harder. The first variation of at gives only an inequality (5.1) in the directions with , and the entropy's difference quotient is not dominated where is small, so the limit requires a one-sided Fatou argument. The inequality (5.1) is not yet a pointwise equation. Converting it into " is constant" needs admissible competitors with bounded density relative to , built fibre by fibre in , and these only reach the support of . Ruling out zeros of (Step 3) needs a separate competitor that charges a set where vanishes. Finally (3.1) concerns a smooth version of the density, which has to be produced from an almost-everywhere identity. The obvious idea of differentiating along for a signed perturbation fails: such perturbations leave unless they preserve positivity and the -marginal.
is EuclideanSpace ℝ (Fin d) with Lebesgue measure; is a complete separable metric space with its Borel -algebra (a Polish space with a fixed compatible metric, needed to state moments and ); carries the max product metric, and in the growth bound is the distance to a base point , with and fixed once for all . is the coupling infimum over this metric, valued in , and continuity is the – notion on . and are functions on all measures of which only the values on matter; is part of the data and the theorem holds for every derivative satisfying (2.1). The definition of the derivative makes explicit what (2.1) presupposes: joint measurability in and integrability in . Mixtures are for , and convexity of is along these mixtures. and take values in , with off absolute continuity. (3.1) is required of some measurable version of the density, for -a.e. and every , together with positivity and differentiability of .
The Lean logarithm satisfies , a non-integrable Bochner integral is , and the gradient of a non-differentiable function is . These would trivialize the statements, so (3.1) demands differentiability, and the milestones that integrate assert integrability and that does not charge , which is what the paper's convention encodes.
A complete development needs: mixtures and moments of measures in ; -convergence of mixtures; dominated convergence along mixtures; the entropy of a mixture and its one-sided derivative; disintegration with respect to the -marginal; and the passage from an a.e. identity to a smooth version of the density. The mixture, moment and entropy lemmas are reusable for any mean-field optimization problem. Contributions of any of these intermediate results, and of proofs of the milestones in any order, are welcome.
Temporal-difference (TD) learning estimates the value of a policy in a Markov decision process from sampled transitions, by repeatedly moving a parametrized value function towards a one-step bootstrapped target (Sutton, 1988). With a linear parametrization its behaviour is well understood: TD converges to the fixed point of the projected Bellman equation (Tsitsiklis and Van Roy, 1997), with finite-sample rates for projected and stochastic variants (Bhandari, Russo and Singal, 2018). With a nonlinear parametrization the same update can diverge: Tsitsiklis and Van Roy (1997) give an example, and the TD direction is not the gradient of any objective. Deep reinforcement learning nonetheless runs TD with neural networks as a matter of course.
Cai, Yang, Lee and Wang (arXiv:1905.10027v2, Mathematics of Operations Research, 2024) prove that TD with an overparametrized two-layer ReLU network, projected onto a ball around its random initialization, converges at rate to the global optimum of the mean-squared projected Bellman error (MSPBE) over a function class that becomes richer as the width grows. This mission formalizes that theorem for the stochastic-semigradient algorithm (Theorem 4.6 of the paper).
Transitions are tuples drawn i.i.d. from a sampling law : are feature vectors of the current and next state–action pair, with , the reward satisfies , and and have the same distribution (they are drawn from the stationary distribution of the policy). The discount factor is and .
The value function is the two-layer network
of width , with hidden weights and output weights . At initialization and , all independent; only is trained. The training set is the ball .
Algorithm 1 (neural TD) samples a tuple at each step , forms the Bellman residual , takes the semigradient step , projects it onto , and outputs with .
The linearization of the network at initialization is
a linear function of with random features. Writing for the Bellman residual of , an approximate stationary point is a with
The function solves the projected Bellman equation over the class . The regularity condition (Assumption 4.3) asks for with for every unit vector and every .
With and under Assumption 4.3, there is a constant such that for all , , and every approximate stationary point ,
where and the expectation is over the initialization, the samples of the run and a fresh .
The theorem gives a non-asymptotic guarantee for TD with a nonlinear function class, a setting in which the algorithm can diverge without further structure. The limit object is a projected Bellman fixed point over a class that, as , approaches a ball in the reproducing kernel Hilbert space of the neural tangent kernel; the paper uses this to bound the distance to the true value function (Proposition 4.7) and to analyze neural Q-learning and policy gradient methods (Section 6). The argument is an instance of the "lazy training" or neural-tangent-kernel regime, in which an overparametrized network trained from a random initialization stays close to its linearization.
The result is proved in the paper and, to our knowledge, has no machine-checked proof. A formalization would also produce reusable components: Gaussian anti-concentration of random ReLU activation patterns (Lemmas H.1–H.2), the linearization error of wide two-layer networks (Lemma 5.1), and a projected stochastic-approximation template with averaged iterates. The appendix proofs are short and pass over several measure-theoretic steps (conditioning on the current iterate, independence of the samples from the initialization, Jensen for the averaged iterate), which a formal proof has to supply.
The TD update is not a gradient, so the convergence proof cannot be a descent argument on an objective. The paper's route is to compare the update with that of the linear TD problem defined by , whose population semigradient is monotone, and to control the difference by overparametrization. The obvious first approach, linearizing the network in a deterministic neighbourhood of , fails: the ReLU activation pattern can change for some units whatever is. The comparison holds only in expectation over the random initialization and a fresh input, through Assumption 4.3 and the finiteness of for , which is where enters. The iterates and depend on the initialization, so these bounds are needed for random parameters that are correlated with but independent of the evaluation point.
Lean represents points as EuclideanSpace ℝ (Fin d) and parameters as PiLp 2 over Fin m, so all norms on are . The MDP, the policy and the feature map are not modelled; the statements see only the sampling law on tuples with the properties listed above. The run's samples form an -indexed i.i.d. sequence (product measure) independent of the initialization, and the evaluation tuple is a fresh draw. Expectations of nonnegative quantities are lower Lebesgue integrals, so non-integrability cannot make a bound hold vacuously. The ReLU semigradient uses the strict convention and keeps the factor of (3.2).
Conventions and readings fixed by the formalization, all disclosed in the item statements:
A formalization in which the comparison point may lie outside , the expectation is a Bochner integral of a possibly non-integrable function, or the constant may depend on , or , would not express the theorem and is excluded. Approximate stationary points are compared through , never through .
A complete development needs Gaussian measures on with the integrability of for , product and infinite-product probability measures with conditioning on the past of a sequence, existence of solutions to variational inequalities on compact convex sets, and nonexpansiveness of Euclidean projection onto a ball. Proofs of individual milestones are welcome independently; Lemmas H.1, 5.1 and (C.16) are self-contained.
We establish several upper bounds on the energy-constrained quantum and private capacities of all single-mode phase-insensitive bosonic Gaussian channels. The first upper bound, which we call the "data-processing bound," is the simplest and is obtained by decomposing a phase-insensitive channel as a pure-loss channel followed by a quantum-limited amplifier channel. We prove that the data-processing bound can be at most 1.45 bits larger than a known lower bound on these capacities of the phase-insensitive Gaussian channel. We discuss another data-processing upper bound as well. Two other upper bounds, which we call the "-degradable bound" and the "-close-degradable bound," are established using the notion of approximate degradability along with energy constraints. We find a strong limitation on any potential superadditivity of the coherent information of any phase-insensitive Gaussian channel in the low-noise regime, as the data-processing bound is very near to a known lower bound in such cases. We also find improved achievable rates of private communication through bosonic thermal channels, by employing coding schemes that make use of displaced thermal states. We end by proving that an optimal Gaussian input state for the energy-constrained, generalized channel divergence of two particular Gaussian channels is the two-mode squeezed vacuum state that saturates the energy constraint. What remains open for several interesting channel divergences, such as the diamond norm or the Renyi channel divergence, is to determine whether, among all input states, a Gaussian state is optimal.
This mission is the statement-level formalization of Bounding the energy-constrained quantum and private capacities of phase-insensitive bosonic Gaussian channels (arXiv:1708.07257v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 26: thermal gap bound (Theorem 26, PDF p. 34). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
51 results of the paper are not stated yet, because the library lacks an interface they need:
We derive a simple relation between a quantum channel's capacity to convey coherent (quantum) information and its usefulness for quantum cryptography.
This mission is the statement-level formalization of Quantum privacy and quantum coherence (arXiv:quant-ph/9709058v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fixed-strategy guaranteed privacy is bounded below by Bob information minus environment Holevo information (Equation (8): fixed-strategy guaranteed privacy lower bound, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We establish the classical capacity of optical quantum channels as a sharp transition between two regimes---one which is an error-free regime for communication rates below the capacity, and the other in which the probability of correctly decoding a classical message converges exponentially fast to zero if the communication rate exceeds the classical capacity. This result is obtained by proving a strong converse theorem for the classical capacity of all phase-insensitive bosonic Gaussian channels, a well-established model of optical quantum communication channels, such as lossy optical fibers, amplifier and free-space communication. The theorem holds under a particular photon-number occupation constraint, which we describe in detail in the paper. Our result bolsters the understanding of the classical capacity of these channels and opens the path to applications, such as proving the security of noisy quantum storage models of cryptography with optical links.
This mission is the statement-level formalization of Strong converse for the classical capacity of optical quantum communication channels (arXiv:1401.4161v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Operational strong converse above the optical classical-capacity threshold (Introduction and Corollary 1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
The long-standing conjectures of the optimality of Gaussian inputs for Gaussian channel and Gaussian additivity are solved for a broad class of covariant or contravariant Bosonic Gaussian channels (which includes in particular thermal, additive classical noise, and amplifier channels) restricting to the class of states with finite second moments. We show that the vacuum is the input state which minimizes the entropy at the output of such channels. This allows us to show also that the classical capacity of these channels (under the input energy constraint) is additive and is achieved by Gaussian encodings.
This mission is the statement-level formalization of A solution of the Gaussian optimizer conjecture (arXiv:1312.2251v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main result: vacuum optimizer and unconditional Gaussian minimum-output additivity (Main result: vacuum optimizer and unconditional Gaussian minimum-output additivity, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Optical channels, such as fibers or free-space links, are ubiquitous in today's telecommunication networks. They rely on the electromagnetic field associated with photons to carry information from one point to another in space. As a result, a complete physical model of these channels must necessarily take quantum effects into account in order to determine their ultimate performances. Specifically, Gaussian photonic (or bosonic) quantum channels have been extensively studied over the past decades given their importance for practical purposes. In spite of this, a longstanding conjecture on the optimality of Gaussian encodings has yet prevented finding their communication capacity. Here, this conjecture is solved by proving that the vacuum state achieves the minimum output entropy of a generic Gaussian bosonic channel. This establishes the ultimate achievable bit rate under an energy constraint, as well as the long awaited proof that the single-letter classical capacity of these channels is additive. Beyond capacities, it also has broad consequences in quantum information sciences.
This mission is the statement-level formalization of Ultimate communication capacity of quantum optical channels by solving the Gaussian minimum-entropy conjecture (arXiv:1312.6225v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-energy Gaussian minimum output entropy (Eq. (2), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Many estimation problems in statistics, signal processing and machine learning ask for a low-rank positive semidefinite matrix: phase retrieval, matrix sensing, PCA-type problems and the Burer–Monteiro approach to semidefinite programs. A standard formulation is
and Riemannian optimization solves it by treating the feasible set as a smooth manifold. Two geometries are in common use. In the embedded geometry the set of rank- PSD matrices is a submanifold of with the Euclidean metric. In the quotient geometry one writes with a full-column-rank factor and optimizes over equivalence classes . Algorithms built on the two geometries behave similarly in experiments, and landscape results (absence of spurious local minima, strict saddles) have been proved separately for each. Luo, Li and Zhang (arXiv:2110.12121, Mathematics of Operations Research 2024) explain this by an explicit dictionary between the Riemannian gradients and Hessians of the two geometries. This mission formalizes their first main result, Theorem 3, for the full-rank factorization of PSD matrices.
Matrices carry the Frobenius inner product . The objective is twice continuously differentiable and symmetric, (the paper's standing assumptions); and are its Euclidean gradient and Hessian.
Embedded geometry. , viewed as . Its tangent space is the span of the tangent cone. The Riemannian gradient is the orthogonal projection of onto , and the Riemannian Hessian quadratic form is the derivative at along any curve in with , .
Quotient geometry. The total space is , the matrices of full column rank, with the objective (18a). A weight , smooth and symmetric positive definite, defines the metric . The vertical space is tangent to the orbit , and the horizontal space is its -orthogonal complement. Tangent vectors of the quotient are represented by horizontal vectors: is the horizontal part of the total-space gradient , and for horizontal , where is the Levi-Civita connection of (Koszul formula).
Comparison data. ; spans the top eigenspace of , , . For a quadratic form on a -dimensional space with inner product , is its -th largest eigenvalue relative to (). are the extreme singular values of an matrix.
If in addition for all orthogonal , then for every and ,
and if is a Riemannian first-order stationary point of (18a),
both Hessians have eigenvalues, and lies between and .
Theorem 3 says that at stationary points the two geometries see the same second-order landscape: the Hessians are congruent through , so their eigenvalues have the same signs and comparable magnitudes, with explicit factors depending on and the spectrum of . The paper derives from it (Corollary 1) that first-order stationary points, second-order stationary points and strict saddles correspond between the embedded and quotient formulations, so a landscape result proved in one geometry transfers to the other. The choice of weight (flat , right-invariant , or ) changes the comparison constants, which is how the paper relates the conditioning of the two approaches.
The result is proved in the paper; it is not formalized anywhere. A formal development adds machine-checked Riemannian gradients and Hessians on a concrete embedded submanifold and on a concrete quotient, a checked horizontal-space computation, and a reusable abstract sandwich theorem for max–min eigenvalues. Corollary 1 and the parallel results for the polar factorization and for general rank- matrices (Theorems 4–7) are natural follow-up missions on the same definitions.
The identities (19), (20) and (34) are matrix calculus once the geometric objects are pinned down; the difficulty is that the definitions are intrinsic. The embedded Hessian requires differentiating the tangent projection along the manifold, which produces the curvature term ; the obvious computation that ignores the moving tangent space gives the wrong Hessian. The quotient Hessian involves the derivative of the weight and needs the horizontal-space description of Lemma 4 to see that the projection in (5) can be dropped. Identifying of the tangent cone with the block form (14) needs an explicit chart of the rank- PSD set. The final sandwich requires a max–min (Courant–Fischer) argument relative to two different inner products, and the order of the bounds flips for negative eigenvalues.
EuclideanSpace ℝ (Fin a × Fin b) (Frobenius inner product) with matrix views toMat/ofMat. The weight takes values in in the same form so that is defined.ProjLikeRetr.Retractor.tangentSpace (span of the tangent cone) and ZORiem.RGD.rgrad (projected Euclidean gradient); "smooth embedded submanifold of dimension " is the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold k d, for every .Useful contributions include Mathlib-level lemmas on the tangent cone of the rank- PSD set, Courant–Fischer for a form relative to a non-standard inner product, and matrix-calculus lemmas for .
The small-step subgradient method is the basic algorithm for minimizing a nonsmooth, nonconvex, locally Lipschitz function . It is also the scheme behind stochastic gradient training of neural networks with nonsmooth activations. From a starting point it iterates
with step sizes and . The basic question is whether a bounded run converges. For smooth , and for continuous-time subgradient flows, convergence follows from a Kurdyka–Łojasiewicz (KŁ) inequality together with tame geometry such as Whitney stratifiability (Bolte, Daniilidis, Lewis, Shiota 2007; Absil, Mahony, Andrews 2005). Whether the same hypotheses suffice for the discrete nonsmooth method was open.
R. Ríos-Zertuche (arXiv:2007.11699, published in Math. Oper. Res. 2022) is a companion to the work of Bolte, Pauwels and Ríos-Zertuche on the long-term dynamics of the subgradient method for path-differentiable functions (arXiv:2006.00098). That work proves positive results, such as slowdown near limit points and convergence of the values under the weak Sard condition. The examples paper shows that these results cannot be improved to convergence of the iterates. Its first example (Section 2) lives on and is the subject of this mission.
For a locally Lipschitz , the Clarke subdifferential is the convex envelope of all limits along sequences of points where is differentiable. The critical set is .
A subgradient sequence (Definition 1) is a sequence obeying the recursion above with positive steps , . The function is path-differentiable (Definition 2) if for every Lipschitz curve and almost every , for all . It satisfies the weak Sard condition (Definition 3) if it is constant on each connected component of . It is Whitney -stratifiable (Definition 5) if its graph in is a locally finite union of disjoint connected submanifolds. These pieces must satisfy the frontier condition and Whitney's condition A: limits of tangent spaces of a stratum contain the tangent spaces of the strata in its boundary.
The example works on . For let
and . Let be the distance to the unit circle . Let be a smooth radial bump with values in , equal to on , vanishing for and non-increasing along rays. Set and . For ,
There are , steps and a sequence such that is a bounded, non-convergent subgradient sequence of , and has all of the following properties:
This is the paper's negative answer to its question Q9, combined with its remarks in Q1 and Q12. The witness is left existential.
The milestones are the properties of the explicit witness (4):
The example is a counterexample: the standard toolbox of tame geometry plus a KŁ inequality does not give convergence of the discrete small-step subgradient method, even with a uniform gradient lower bound away from the critical set and the weak Sard condition. In continuous time the same hypotheses give convergence. The gap therefore comes from discretization. Any convergence proof for nonsmooth subgradient methods needs further structure, such as definability in an o-minimal structure or a stronger KŁ inequality near the critical set. Q12 adds that requiring the iterates to stay in the full-measure set of differentiability points does not help.
The result is proved in the paper; to our knowledge none of it is formalized. Formalizing it gives the first machine-checked Clarke-subdifferential, path-differentiability and Whitney-stratification counterexample. It also gives reusable estimates for an explicit sequence spiralling onto a circle.
Most of the steps are explicit estimates, but three of them are delicate.
Everything lives in EuclideanSpace ℝ (Fin n). The definitions follow these conventions:
ShorNonsmooth.AlmostDiff.almostGradients, which uses cluster points of the gradients rather than limits; the two sets are the same.ProjLikeRetr.Retractor.IsSubmanifold) for every . Tangent spaces are spans of tangent cones, and Grassmannian convergence is convergence of the subspace gap to .BumpProfile with exactly the properties listed on p. 6, and the series in (4) are tsums. The indices , where and in Lean, are never used.Four statements are adjusted, and each adjustment is disclosed in its item:
gradient is at non-differentiable points.The goal cannot be met trivially. Boundedness of the sequence and the conditions , are part of it, and they rule out an affine . Every regularity property is a separate conjunct. Contributions that develop the geometry of Whitney stratifications and path differentiability in Lean are reusable well beyond this example.
Banking and insurance regulation measures capital requirements with risk measures that look only at the tail of a loss distribution. The Basel framework moved from Value-at-Risk (VaR) to Expected Shortfall (ES) for market risk (BCBS, Minimum capital requirements for market risk, 2016), and both VaR and ES at level depend on a loss only through its distribution beyond the -quantile. Liu and Wang (SSRN 2841909; Mathematics of Operations Research 46(3), 2021, doi:10.1287/moor.2020.1072) isolate this feature as a definition. A tail risk measure is any risk measure that depends only on the tail, and every such measure is generated by an ordinary law-invariant risk measure applied to the tail. The paper then asks which of the classical properties of risk measures (Artzner et al. 1999; Föllmer and Schied 2002) survive this construction.
The answer to that question is a practical design rule. A regulator or risk manager who wants a coherent tail risk measure can choose any coherent law-invariant risk measure and apply it to the tail. The theorem guarantees that the result is again coherent, and that nothing is lost by working only with generators.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. A random variable is a loss when positive and a profit when negative. Its distribution function is . The space of risks is , the measurable, essentially bounded random variables. A risk measure is a real-valued functional on .
For , the -tail of is a random variable with distribution function
the conditional law of beyond its -quantile. A risk measure is a -tail risk measure if whenever and have the same law. A pair is a -tail pair if is law-invariant and
in which case is a -generator of . For example, is generated by the expectation. The mixture has distribution function : it adds mass at the essential infimum of .
The classical properties are those of Appendix A of the paper:
A monetary risk measure satisfies (A1)–(A2), a convex one (A1)–(A3), and a coherent one (A1)–(A4) (Definition A.1).
For and a -tail pair on ,
All three equivalences are part of the goal. No normalization such as is assumed.
where is the set of sums with (resp. , the law of the -tail).
The result. Theorem 1 (iii) makes the generator a complete parametrization of coherent and convex tail risk measures. Coherent tail risk measures are exactly with coherent and law-invariant, so representation results for law-invariant coherent risk measures (Kusuoka 2001) transfer to tail risk measures. The paper uses this for dual representations (Appendix G) and for the bound of Theorem 2. Theorem 3 reduces worst-case risk aggregation for a tail risk measure to the same problem for its generator on tail marginals. It contains classical results on worst-case VaR (Bernard et al. 2014, Lemma 4.3) and the subadditivity of ES as special cases.
Formalizing it. The results are proved in the paper; none of them is machine-checked. The mission produces a Lean statement of tail risk measures and their generators that later missions on tail risk can import. It also produces formal versions of the distributional identities (Lemma B.1, eq. (14)) on which the paper's proofs rest, and a statement of worst-case aggregation in extended-real suprema. A complete development would also be the first formal proof that ES-type constructions preserve coherence through a general generator, rather than for one specific measure.
Several directions are routine. Monotonicity, translation invariance and positive homogeneity pass from to because commutes with shifts and positive scalings and preserves . The converse directions go through .
Convexity is the obstruction. The obvious argument would compare with , but the tail of a sum is not the sum of the tails. The event "beyond the -quantile" for the sum differs from the corresponding events for and , so no pointwise or comonotone coupling identifies them. Example 1 makes this concrete: the tail standard deviation is generated by a convex measure and is not convex. Convexity of therefore needs monotonicity of together with the worst-case aggregation identity of Theorem 3. That identity is a statement about all dependence structures with given marginals, and it requires constructing, on an atomless space, couplings whose tails dominate a given sum.
TailRiskSharing.TailConv.Linf), as the paper suggests on p. 5. Then , every risk measure is a real-valued function on , and every property quantifies over only. The general cone with -valued risk measures is not stated.TailRiskSharing.VaRConv.IsAtomless), not Mathlib's NoAtoms, which only says that singletons are null.A formalization in which is a fixed Classical.choose of the tail, in which coherence omits monotonicity, or in which atomlessness is replaced by NoAtoms is not this theorem.
A complete development needs the quantile transform on an atomless space, couplings with a prescribed joint law, the elementary identities of Lemma B.1 and eq. (14), and the worst-case aggregation argument of Appendix C. The distributional lemmas, quantile couplings and aggregation sets can be reused in any later mission on law-invariant risk measures. Contributions to any milestone, and to general infrastructure for quantile couplings on atomless spaces, are welcome.
Exploratory data analysis often summarizes a large data set by a small number of representative regions: histogram bins, the leaves of a density estimation tree, balls around cluster centres, or the regions chosen by a covering or -center optimization. Estes, Ball and Lovell (SSRN 3005997; Mathematics of Operations Research, 2021, doi:10.1287/moor.2020.1115) treat all of these as instances of one abstraction, the representative region selection (RRS) method, motivated by summarizing air-traffic ground-delay programs at Newark airport. The first half of their paper proposes axioms for the quality of such summaries. The second half (§6) asks a statistical question: when the data are an i.i.d. sample, do the summaries converge to the population they describe? This mission formalizes that convergence theory, culminating in the consistency of the density estimate that any RRS method induces.
Let be a set. An RRS method on is a pair : is a class of allowed regions, and maps every finite set to a finite set . The coverage region is . The method is sample-covering if , and sample-intersecting if every contains a point of .
Now let be a metric space with a σ-algebra containing every closed ball, and let be i.i.d. -valued random variables with law . Write , , and for the fraction of the first observations lying in . The support of is the set of points all of whose closed balls of positive radius have positive probability.
Regularity is imposed on the class, not on the method. A scalable class writes every region as with a shape parameter and a scale , non-decreasing in . It is uniform-scale if increasing the scale by swells every region by a closed ball of a radius that does not depend on the region, and uniformly continuous with respect to if changing the scale by changes the probability of every region by at most .
A family is arbitrarily precise if, for every , all methods far enough along the family eventually (almost surely, as grows) output regions of diameter at most . A method is uniformly positive with respect to a reference measure if its regions have -measure bounded below, and has asymptotically-bounded cardinality if it eventually outputs at most regions. When has a density with respect to , the RRS density estimate at averages over the chosen regions that contain :
and when no chosen region covers .
If the support of is compact with , is continuous, some closed neighbourhood of has finite -measure, and is an arbitrarily precise family over a uniform-scale class that is uniformly continuous with respect to , with each sample-covering, sample-intersecting, of asymptotically-bounded cardinality and uniformly positive, then almost surely
The goal shows that one estimator, defined uniformly from any RRS method, is -consistent under conditions that are checked once for the class of regions and once for the method. Histograms, density estimation trees, and the paper's own minimum-dominating-set and -center summaries (Corollaries 7.1 and 7.2) all become consistent density estimators as soon as they satisfy those conditions. Theorem 6.1 is of independent interest: it is a Glivenko–Cantelli theorem whose hypotheses are geometric and measure-theoretic rather than combinatorial, applying to classes for which no finite VC dimension is known.
The results are proved on paper; none is machine-checked. The mission produces a formal layer for region-based empirical processes (RRS methods, uniform-scale classes, the region-average density estimate) and machine-checked versions of the convergence chain. The formal statements also repair two places where the printed hypotheses are too weak (see Formalization scope), so a completed development certifies corrected theorems, not merely transcribed ones.
The regions an RRS method selects depend on the sample, so the law of large numbers cannot be applied region by region: there are uncountably many candidate regions and no fixed finite family to which the strong law applies. The uniform convergence of Theorem 6.1 must instead come from a finite approximation of the whole class, combining compactness of the support with the uniform-scale and uniform-continuity hypotheses, and the approximation has to work at every scale, including scales smaller than the approximation step. The goal adds a second limit: the error splits into a part on the coverage region, governed by the uniform estimate of Theorem 6.4, and a part on the uncovered portion of the support where the estimate is zero, governed by Corollary 6.2. The two limits ( inside, outside) and the almost-sure quantifier must be interleaved correctly, with countably many null sets collected over .
All statements live in the namespace RepRegion.Density, with one definitions file RepRegion.Density.Model. is a metric space with an arbitrary σ-algebra in which every closed ball is measurable (no Borel assumption); is a probability space; the observations are X : ℕ → Ω → M, measurable, mutually independent (iIndepFun) and identically distributed, indexed from . is P.map (X 0). The reference measure is an arbitrary measure on . Regions are Set M, a method is Finset M → Finset (Set M), and the scale map is R : Θ → ℝ → Set M, read only at positive scales.
Committed conventions:
A formalization in which the error is a Bochner integral, a supremum is a real sSup, or a diameter is Metric.diam would make the conclusions hold for junk reasons on non-integrable or unbounded inputs; those encodings are ruled out.
A complete development needs the strong law of large numbers for indicators (in Mathlib), finite nets of compact metric sets, and almost-sure hitting arguments for balls of positive probability. The region-based Glivenko–Cantelli theorem and the coverage results are reusable for any later mission on partition-based estimators. Proofs of the individual milestones, alternative arguments, and a version of the goal under continuity of on alone are all welcome.
Schur–Weyl duality says that on the tensor power of the natural representation of , the symmetric group acting by place permutations generates the full commutant of . It is the bridge between representations of general linear groups and of symmetric groups. Two extensions matter in representation theory and in the theory of tensor categories:
Brundan and Stroppel (arXiv:1107.0999) prove the combination: mixed Schur–Weyl duality for . It is the first step towards their main result, a Morita equivalence between and an idempotent truncation of Khovanov's generalized arc algebra , from which they derive that is Koszul for . Comes and Wilson obtained the same duality independently (arXiv:1108.0652); Shader and Moon had a partial result earlier (Commun. Algebra 30, 2002).
Timeline:
Fix integers and put . Let , with parity for and for . Let have basis with of parity , and the dual basis . The Lie superalgebra is , spanned by matrix units of parity , acting by
It acts on , with basis for , through and the sign rule . The super-commutant is the space of all linear maps , not necessarily homogeneous, annihilated by the action of every .
A walled Brauer diagram pairs the vertices on the top and bottom edges of a rectangle, with a wall after position : a vertical strand joins vertices on the same side of the wall and a horizontal strand joins vertices on opposite sides. These diagrams are a basis of ; the product puts under and multiplies by for removed circles. Colouring the bottom vertices by and the top vertices by , the weight is unless every strand has equally coloured ends, and otherwise raised to the sum of over the crossings of strands of colours plus over the bottom horizontal strands of colour (7.5). The right action
defines (7.12). For the permutation diagrams give (7.11).
For all ,
Theorem 7.8 identifies with the full super-commutant of mixed tensor space. Brundan and Stroppel use this to compare with a graded algebra built from Khovanov's arc algebra (Corollary 8.2, Theorem 8.10), which yields a grading on , its Koszulity for , and descriptions of the indecomposable summands of . The injectivity range says exactly when the walled Brauer algebra is faithfully realized on tensor space.
All statements are proved in the literature; none has a machine-checked proof that we are aware of. A complete formalization would need classical and super Schur–Weyl duality (Theorem 7.5 is the deep input, proved in the paper only by citation), the weight calculus of diagrams, and the sign bookkeeping of Lemma 7.7, which the authors call tricky.
Surjectivity onto a commutant is a double-centralizer statement, and the obvious route through semisimplicity fails: for the tensor space is in general not semisimple as a -supermodule. Theorem 7.5 instead rests on Berele and Regev's analysis of hook Young diagrams. Mixed tensor space adds a second obstacle: enters with signs both in its -action and in the dualities , and the reduction to via works only when every sign convention (crossings, bottom caps, the sign rule, the dual map) is matched exactly.
Fin (m + n), odd iff . A tensor space is given by a slot pattern Fin N → Bool (true = ); operators are complex matrices indexed by Fin N → Fin (m + n), with column = input basis vector.Fin N ⊕ Fin N (Sum.inl = top), reusing the published WalledBrauer.Blocks.WalledDiagram, its composition comp and its loop count loops. Crossings are counted by interleaving of endpoints along the boundary, which is the crossing set of a reduced drawing; Lemma 7.2 (isotopy invariance) is thereby absorbed.The following would trivialize or falsify the statement and are ruled out: a commutant of only, or one that drops the odd part or the signs; an unsigned slotwise action; a range statement with only one inclusion; an injectivity statement with only one direction. Not formalized: the paper's general Lemma 7.6 for arbitrary supermodules (no supermodule category in Mathlib), and everything involving . Contributions of a reusable Lie-superalgebra tensor layer and of Berele–Regev's hook-partition theory are welcome.
A routing decision can have a known immediate cost while its consequences depend on uncertain weather. A controller observes the current state, chooses an action, and then faces a random next state. A policy optimized for one estimated transition model may perform poorly when those estimates change. Chapter 13 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization studies this issue through finite-state control problems and illustrates it with aircraft routing. The mathematical target here is the finite-horizon theorem that evaluates and optimizes policies against admissible changes in transition probabilities.
The uncertainty model matters. Requiring nature to use one fixed transition matrix throughout the horizon couples its choices across time. Allowing each time, state and action to have its own admissible probability row gives a different problem. The latter is the setting of this mission and of the chapter's robust Bellman recursion. No assertion of exact solution of the stationary-uncertainty problem is included.
Let the state space be a finite nonempty set , and let the action space be a finite nonempty set , available in every state. The decision times are , with terminal time . A deterministic Markov policy assigns an action to every time and state . The stage cost and terminal cost are real numbers; they need not be nonnegative. The initial state has a given probability distribution .
A transition row gives the probabilities of the next state, conditional on time , current state , and action . For fixed policies, distributions evolve according to
The expected total cost is defined from these forward distributions:
For robust control, every row belongs to a nonempty closed set in the probability simplex. Rectangular uncertainty means that nature's admissible policies are the entire product of these sets: choices at different times, states and actions are independent constraints. The sets themselves may depend on time and need not be convex. These are the standing assumptions of Sections 13.2–13.3 of the book.
The first supporting target is Theorem 13.1.2. For a fixed controller and fixed transition rows, the expected cost equals the attained maximum of the linear program with terminal vector and inequalities
whose objective is . The second target, Theorem 13.1.4, is the nominal Bellman theorem: the recursion that minimizes the corresponding one-step expression over actions gives the optimal remaining cost at every time and state, and greedy policies for its values are optimal.
The goal is the full Theorem 13.3.1. With , define
Then is the minimum worst-case remaining expected cost starting at state at time , and
The target includes existence of controller policies choosing the displayed minimizing actions and nature policies choosing maximizing rows. Every such controller is optimal, and corresponding maximizing rows realize its worst cost. For any fixed controller , the separate evaluation recursion
must give its attained worst expected remaining cost, including the total value .
These statements connect three different objects: a forward stochastic evolution, optimization over complete policies, and backward value calculations. The robust theorem supplies both an optimal decision rule and an evaluation of uncertainty for a prescribed rule. Keeping the initial distribution arbitrary retains the distinction between statewise values and the value of the original control problem.
The results are established mathematics in the source; the work requested is their formal verification. A related proved robust-DP theorem uses time-independent uncertainty sets, nonnegative stage costs and a fixed initial state. This mission preserves the book's different data and attainment conclusions. Its local statements are open proof targets, not completed Lean proofs.
The central issue is relating the independent forward cost to the policy optimization and preserving all attainments. Choosing an individually favorable action does not by itself establish optimality over complete policies. Likewise, replacing a maximum by a real supremum leaves the existence of a maximizing nature policy unresolved. Closedness of the row sets and their probability constraints are substantive assumptions here. The fixed-policy and optimizing recursions must also be distinguished: nature's worst choices for an arbitrary controller need not be the rows selected from the optimal value function.
States, actions and decision times use finite index types, with nonempty state and action spaces. All costs and probabilities are real. Probability vectors have nonnegative coordinates summing to one. The model retains arbitrary initial distributions, time-dependent uncertainty sets and terminal costs. A zero horizon has no decisions and yields terminal expected cost.
The definition bundle includes forward distributions, expected costs, both Bellman recursions, the independent worst-cost function, and the policy-selection predicates. The theorems compare these independently defined quantities, rather than defining expected cost to be the desired Bellman value. Extrema use attained order predicates, with internal suprema restricted to the admissible nature policies. Full-horizon policies encode suffix policies by ignoring coordinates before the starting time.
Formalization Note Each theorem carries its needed concrete definitions in a separate namespace so it compiles without importing unpublished drafts. The definition item records the common reusable interface. Equation (13.1.3) supplies the forward-distribution definition rather than a tautological milestone. The nominal LP Theorem 13.1.3 is not a dependency in this selected route; its printed index and arbitrary-optimizer issues are recorded locally. No corrected or strengthened variant is posed.
A quantum circuit normally applies a sequence of gates to a prepared state. Verstraete, Wolf and Cirac proposed a different physical route: couple a quantum system to a memoryless environment so that dissipation drives it toward a state recording the circuit's computation. Their dissipative quantum computation construction places a clock beside the computational qubits and makes the circuit history a stationary state of a time independent master equation. A useful process must have a well identified stationary state and a rate of relaxation that does not collapse with the number of qubits or with the chosen gates. The paper argues for these properties in its DQC section and its efficiency appendix (Verstraete, Wolf and Cirac, 2008, pp. 1–2, 4–5).
The printed spectral gap formula and part of its supporting clock block do not describe the slowest decay of the stated generator. Direct finite dimensional calculations reveal a slower coherence sector. This mission therefore targets the stated stationary state and a corrected, explicitly ranged version of the paper's lower bound. The discrepancies and boundary cases are recorded in the formalization scope so that the target is a mathematical claim about the displayed Lindblad operators rather than an unchecked transcription.
Fix qubits and circuit steps. A computational basis string is a function from the qubit positions to . The clock register has basis for . A family of unitary gates acts on the qubit register. Its history vectors are and .
A jump operator resets qubit only when the clock is at zero: . For each neighboring clock pair, another jump operator moves in both directions, applying the relevant gate on the forward move and its adjoint on the reverse move. The Lindblad generator is the linear map on matrices
There is no Hamiltonian term. The proposed history state is the normalized density matrix
These are equations (1)–(4) of the paper, with the clock step index repaired as described below. The appendix introduces a gate removal unitary , a connected clock path matrix , and clock blocks with a penalty at time zero. Their spectra lead to the uniqueness and decay claims (paper, pp. 2, 4–5).
For every , , and family of unitary gates, prove that , that is positive semidefinite with trace one, and that the full kernel of consists of scalar multiples of . For , prove additionally that every nonzero eigenvalue satisfies
The bound applies uniformly across the number of qubits and the circuit gates. It is the corrected form of the efficiency conclusion on p. 5. The goal does not assert the printed formula , which is contradicted by the slowest coherence sector (paper, pp. 2, 5).
The milestones first establish stationarity and removal of the circuit gates by . They then target the one dimensional fixed space for identity gates, the first nonzero eigenvalue of the connected clock path, the penalized clock blocks, and the full generator's bound for identity gates. This follows the sequence of reductions described in the efficiency appendix while retaining the paper's exact clock constants where they are valid (paper, pp. 4–5).
The kernel statement identifies every stationary matrix, a stronger assertion than merely finding one stationary density matrix. The eigenvalue bound supplies a uniform spectral scale for the finite dimensional generator, independent of the circuit content. Together these make precise the part of dissipative computation that says the intended history is singled out and spectrally separated from other modes. A convergence time theorem would also have to control Jordan blocks or the operator semigroup and is outside this target; the paper itself notes this separate issue on p. 5 (paper, p. 5).
Formalizing the corrected claim creates a reusable finite matrix representation of a Lindblad generator and a circuit clock, plus independently usable path and boundary penalty spectral statements. The paper result is known in physics prose; these exact Lean statements are open proof goals in this proposal. The correction also prevents later arguments from importing a spectral equality that does not hold for the displayed process.
The gate operators couple the qubit register to the clock, so diagonalizing a clock matrix alone does not describe the generator. Even after the gates are removed, the Liouvillian acts on matrices, including coherences between two qubit states and two clock times. The decay of a one sided coherence at clock zero carries half the penalty of a population term. Reading every nonzero sector as if it had the population penalty produces the printed gap value and misses the slowest mode. The clock path also has to retain the first edge and its endpoint diagonal entries; omitting that edge changes the spectrum.
Lean uses matrices indexed by bit strings paired with the finite clock , and a complex linear endomorphism on those matrices. Gates are quantified as unitary matrices; they may act on all qubits, whereas the paper starts with nearest neighbor gates. The appendix's spectral argument is independent of that locality, so this is a disclosed generalization. The model also permits . Gates use zero based indexing: Lean's is the paper's and acts on the step . This repairs equation (3), which otherwise calls for both an undefined and an out of range clock state .
Uniqueness is restricted to : at an additional clock coherence is stationary. The strict bound is restricted to : direct diagonalization shows it fails for . The paper's printed corner coefficient is correct for a population sector, but a one sided coherence has coefficient . A milestone states the valid printed matrix fact and the corrected bound for all clock zero penalties . The connected path matrix follows the displayed spectral formula rather than the printed tridiagonal sum whose range omits the first edge.
The generator is defined from the jump operators by equation (1). It is not defined from the desired block decomposition or eigenvalues. The spectral assertion quantifies over actual nonzero complex eigenvalues and compares their real parts directly; no default valued infimum defines a gap. Work toward the mission may supply matrix identities, unitary covariance, tridiagonal spectra, or a direct finite dimensional analysis of the generator. The generic finite matrix Lindblad definition can be reused independently of this circuit model.
Many constructions in differential topology and infinite-dimensional Lie theory start from a continuous object and need a smooth one: a continuous section of a smooth bundle, a continuous map into a manifold, a continuous homotopy between smooth maps. Steenrod's approximation theorem (Steenrod 1951, §6.7) says that, for finite-dimensional bundles, a continuous section can be smoothed by a small homotopy through sections, without changing it where it is already smooth. Hirsch's textbook (Hirsch 1976, Ch. 2) gives the relative version for maps between finite-dimensional manifolds.
Gauge theory and the study of principal bundles whose structure group is an infinite-dimensional Lie group (current groups, diffeomorphism groups, gauge groups) need the same statement when the typical fibre is infinite-dimensional. C. Wockel (arXiv:math/0610252, 2006) proves it for a finite-dimensional base with corners and a fibre that is a manifold modelled on a locally convex space, combining Steenrod's argument with Neeb's approximation results for maps into locally convex spaces (Neeb 2002, App. A.3). The consequences in the paper are that smooth and continuous homotopy classes of sections, and of maps from a finite-dimensional manifold into a locally convex manifold, coincide; this is used in bundle theory for infinite-dimensional structure groups (Müller–Wockel 2006, cited as [MW06] in the paper).
A manifold with corners is a Hausdorff paracompact space with charts onto open subsets of the quadrant and smooth coordinate changes. A locally convex manifold is a Hausdorff space with charts onto open subsets of a locally convex space and smooth coordinate changes, where smoothness of means that all iterated directional derivatives exist and are continuous (Definition 0.1 of the paper).
A map is a locally trivial smooth bundle with typical fibre if every point of has an open neighbourhood and a diffeomorphism with . A section is a continuous map with . A map is smooth on a neighbourhood of a set if it is smooth on some open set containing .
For spaces , is the space of continuous maps with the compact-open topology, generated by the sets with compact and open.
Let be finite-dimensional and connected, a locally trivial smooth bundle with typical fibre , a continuous section, closed, open, and smooth on a neighbourhood of . Then for every open there are a section and a homotopy with
The result. The theorem turns continuous sections into smooth ones by homotopies that are small (they stay in any prescribed open set around the section) and relative (fixed where nothing needs changing). It yields that is dense in for the graph and compact-open topologies (Corollary 0.12), that every continuous section is homotopic to a smooth one and continuously homotopic smooth sections are smoothly homotopic (Proposition 0.13), and that smooth and continuous homotopy classes agree (Corollary 0.14). These are the statements needed to compare smooth and topological classification of bundles with infinite-dimensional structure groups.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. Mathlib has smooth partitions of unity on finite-dimensional manifolds with corners and local-to-global smoothing for maps into convex sets, but no density of in for the compact-open topology, no relative smoothing lemma, and no smoothing of sections of non-vector bundles. A formalization would supply these as reusable statements about Mathlib's ContMDiff, Bundle.Trivialization and C(M, Y).
The obvious argument glues local smoothings with a partition of unity, as for real-valued functions. This fails for sections of a non-linear bundle: convex combinations of points of , or of , are meaningless, so a partition-of-unity average of local smoothings is not a section, and the smoothing cannot be done in one global step. Any stepwise replacement must keep the section inside the prescribed open set , must not destroy smoothness already achieved near earlier parts of , and must avoid convergence arguments, since infinitely many steps are needed on a non-compact . The homotopy has to be continuous at the end where infinitely many steps accumulate. Finally, an infinite-dimensional is not locally compact, so all compactness must come from ; this is why the base is finite-dimensional while the fibre is not.
ContMDiff … ∞ (not the analytic ω). This is the one specialisation of the paper; non-normable locally convex fibres are out of scope.[T2Space M], and [ParacompactSpace M] (Theorem 0.11, Remark 0.4, milestone 6) or [SigmaCompactSpace M] (Proposition 0.7, Corollary 0.8, Lemmas 0.9, 0.10), as Definition 0.3 and the statements require; Theorem 0.11 adds [ConnectedSpace M]. is [T2Space N].SmoothNear), not smoothness on itself. Spaces for or are maps into the subtype with the compact-open topology, so neighbourhoods are taken in . A bundle is given by smooth Bundle.Trivializations covering ; " diffeomorphic to an open convex subset of " is a partial diffeomorphism with source and convex target. The homotopy is indexed by unitInterval and runs from at to at . "Support" is the closed support tsupport.The Lie superalgebra , a central extension of the Lie superalgebra of infinite matrices of finite support, appears in the representation theory of the vertex algebra and in Howe-type dualities with (Kac–Radul; Cheng–Lam). Its irreducible quasi-finite highest weight modules of positive integral level are indexed by generalized partitions , and their characters had been computed by Cheng and Lam in terms of hook Schur functions and Littlewood–Richardson coefficients.
J.-H. Kwon (arXiv:math/0605005) gave these characters a tableau model. He introduced A/B-semistandard tableaux, pairs of super-semistandard tableaux attached to a generalized partition, showed that their generating function is the character in question (Theorem 5.2), and developed an insertion scheme that yields an RSK correspondence, a Littlewood–Richardson rule, and a Jacobi–Trudi type determinant formula (Theorem 4.5). The paper notes that this determinant formula for the characters of -modules had not been observed before. The combinatorics rests on Stembridge's rational semistandard tableaux (1987), which model the rational representations of , and on Berele–Regev's hook Schur functions (1987).
Let and be linearly ordered, at most countable sets, each split into even and odd letters, .
A filling of a skew Young diagram with letters of is -semistandard if its entries weakly increase along rows and down columns, even letters strictly increase down columns, and odd letters strictly increase along rows. The weight of records how many times each letter occurs, and .
A generalized partition of level is . It is drawn against a vertical line: row has boxes to the right of the line if and boxes to the left if .
An A/B-semistandard tableau of shape is a pair with and for some and partition , . Both tableaux are drawn against the line of , so enlarging by one and by a full column gives the same pair. The character is
a power series in the symbols and . At level one, is defined for every , negative included.
A rational -semistandard tableau of shape fills the diagram of with right of the line and left of it, rows weakly and columns strictly increasing, subject to Stembridge's compatibility condition between columns and . Its content has , and counts the tableaux of shape and content .
For infinite , and every , ,
The entries are level-one A/B-characters, not complete symmetric functions. Unlike , they do not vanish for .
The result. Theorem 4.5 is the super, rational analogue of the Jacobi–Trudi identity. Through Theorem 5.2 it becomes a determinant formula for the characters of the irreducible quasi-finite -modules of positive level (Corollary 5.4). Specialising and recovers formulas for and for the Howe duality. Milestones 2–6 develop the rational Kostka theory along the way: its shift invariance, its triangularity, and its role in an RSK correspondence for A/B-tableaux.
Formalizing it. The theorem is proved in the paper; nothing in it has a machine-checked proof. Mathlib has semistandard Young tableaux and symmetric polynomials, but no Schur polynomials as tableau generating functions, no Kostka numbers, no RSK, and no classical Jacobi–Trudi identity. Milestone 6 is therefore new to formal mathematics in its own right, and it is a prerequisite for the goal's proof.
The obvious attack proves the classical Jacobi–Trudi identity once and then transfers it. That fails here for two reasons. The entries with are nonzero, so the classical vanishing that truncates the determinant is unavailable. And the expansion is an infinite sum over generalized partitions, so the comparison with (4.5) leaves an error term supported on . Killing it requires both the shift invariance of the rational Kostka numbers and the uniqueness of coefficients in infinite combinations (Corollary 3.23). The combinatorial input, Corollary 4.4, is a weight-preserving insertion bijection for pairs of super tableaux, built from row and column insertion, rectangular complements and Stroomer's theorem. Each of these is substantial to formalize.
SuperTableaux.JacobiTrudi, with one definitions item.LinearOrder and Countable; the grading is a function odd : A → Bool, where true means odd.MvPowerSeries (A ⊕ B) ℤ. The variable Sum.inl a is and Sum.inr b is the symbol , which is literally the ring . The coefficient at a monomial is Nat.card of the set of tableaux of that weight; milestone 1 proves that set finite.toLex, which is the paper's "reverse lexicographic ordering" of p. 23.HasSum/Summable in the coefficientwise topology, never tsum.A formalization that defines by a determinant or product formula, sums over without the identification (every coefficient becomes Nat.card of an infinite set, i.e. ), or drops the parity conditions trivializes the goal; the definitions here are the tableau generating functions of (3.13)–(3.14).
A complete development needs Kostka numbers, Schur polynomials as tableau generating functions, the classical Jacobi–Trudi identity, RSK for super tableaux, and coefficientwise convergence in multivariate power series. All of these are reusable beyond this mission. Contributions are welcome on any milestone, and on intermediate lemmas such as the classical Jacobi–Trudi identity.
We give an overview of relative tensor products (RTPs) for von Neumann algebra modules. For background, we start with the categorical definition and go on to examine its algebraic formulation, which is applied to Morita equivalence and index. Then we consider the analytic construction, with particular emphasis on explaining why the RTP is not generally defined for every pair of vectors. We also look at recent work justifying a representation of RTPs as composition of unbounded operators, noting that these ideas work equally well for L^p modules. Finally, we prove some new results characterizing preclosedness of the map (ξ, η) \mapsto ξ\otimes_φη.
This mission is the statement-level formalization of Relative tensor products for modules over von Neumann algebras (arXiv:math/0301061v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Density of the intrinsic bounded-vector domain (§5, bounded-vector density, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
23 results of the paper are not stated yet, because the library lacks an interface they need:
Linearised Einstein–Maxwell equations around charged black-hole backgrounds are the starting point of perturbation theory for the Reissner–Nordström and Kerr–Newman families (Newman et al., 1965; see e.g. Giorgi, arXiv:2002.07228). Every such analysis silently uses two facts: that the backgrounds solve the coupled equations, and that the linearised operator is the derivative of the nonlinear residual. In a proof assistant neither is free. This mission records machine-checked certificates for the two backgrounds and an off-shell theorem identifying explicit linearised operators with true derivatives.
Coordinates on an open set are . A metric field and an inverse field are arrays of real functions with on ; a two-form field is an array . With the coordinate partial derivatives , Christoffel symbols and Ricci tensor built from and the given , the three residuals are
An Einstein–Maxwell certificate on records: open and nonempty, symmetric, a true inverse, all components , antisymmetric, Lorentzian, and , , on . A family on an open is admissible (FamilyData) when are jointly and on ; no symmetry, signature, antisymmetry or field equation is assumed. Its tangent is the -derivative at .
For every admissible family with tangent and every with ,
and likewise , , where , , are explicit finite expressions in the background, , and their first and second coordinate derivatives. The statement is off shell.
The twelve milestones above: the two background certificates and two parameter specialisations; realisation of arbitrary directions and linearity; covariance and certificate transport; parameter tangents of both families; coordinate and potential gauge directions; and one direction on which does not vanish.
The goal makes the linearised operators usable without trusting a hand derivation: any statement about is a statement about true derivatives of the registered residuals. The background certificates cover every real parameter in the stated domains (Kerr–Newman for and all real ), and the parameter-tangent and gauge milestones check the operator against the expected zero directions, while milestone 12 rules out a trivially vanishing operator. The background solutions are classical; what is new here is their machine-checked form and the off-shell derivative theorem in this coordinate setting.
The residuals involve the inverse metric and second derivatives of the metric. Differentiating in requires interchanging with coordinate derivatives and differentiating the inverse family; pointwise differentiability in is not enough, and an operator merely named "derivative" would make the goal vacuous.
Lean 4 with Mathlib (0df444a3…), autoImplicit off; smoothness is ContDiffOn ℝ ∞ (, not analytic). The pinned Mathlib has no Lorentzian Levi-Civita connection or Ricci tensor, so the coordinate definitions (partial derivative, Christoffel symbols, Ricci tensor, residuals) are a registered local definition layer from the earlier Atlas releases, reused unchanged. The operators are independently specified using finite sums and coordinate derivatives; they are not defined as parameter derivatives of the nonlinear residuals. The goal proves that these expressions equal the genuine parameter derivatives. Not included: nonlinear integrability of tangents, new exact solutions, Newman–Penrose reductions, stability, gauge classification, horizons or global structure. The coordinate family used for the gauge milestone is a local family of coordinate maps, not a flow of .
The walled Brauer algebra organizes the linear operators that commute with a general linear group acting on a tensor product of vector spaces and their duals. Its diagrams mix crossings and contractions, with a wall distinguishing the two tensor factors. This makes it useful in mixed tensor representation theory, where the ordinary symmetric group algebra no longer records every commuting operator. Sartori and Stroppel compare this diagram algebra with a level-two cyclotomic quotient of a degenerate affine walled Brauer algebra. Their comparison identifies a concrete part of the larger algebra by an explicit change of generators Sartori–Stroppel, Theorem 6.2.
The paper's result is a proved theorem. This mission asks for a machine-checked proof of its algebraic statement. The source builds the cyclotomic quotient using parameters arising from parabolic category , but the target here is the resulting algebra isomorphism. The dimension comparison that the authors obtain through category is included as a separate milestone, in the exact numerical form used in their injectivity argument Sartori–Stroppel, Theorem 5.2, Corollary 5.8, and Lemma 5.9.
Fix . An orientation is a word of length containing exactly upward arrows and downward arrows. The walled Brauer algebra is a complex algebra with an idempotent for each orientation. At an adjacent pair of positions , equal arrows admit a crossing . Unequal arrows admit a changed-orientation crossing , an orientation-preserving contraction , and a changed-orientation contraction . The relations (Br1)–(Br6) specify orthogonal idempotents, sources and targets, quadratic and braid relations, and interactions among crossings and contractions Sartori–Stroppel, Definition 2.1.
The degenerate affine walled Brauer algebra adds commuting elements and their relations with the oriented generators. Its level-two cyclotomic quotient imposes a quadratic relation on in each first-arrow component Sartori–Stroppel, Definitions 2.5 and 2.8. Write this quotient as . It uses positive integers and an integer , with
The later follow the quadratic recurrence determined by the upward cyclotomic polynomial; they are fixed by these parameters. These are the paper's parameters (5.4), with values in Sartori–Stroppel, Definition 5.1 and Lemma 2.9.
For each position and orientation , let project away from the generalized eigenspace of with eigenvalue . The spectral truncation is , with . The intermediate products are and . This gives the corner algebra Sartori–Stroppel, Definition 5.6. The elements , polynomial square roots, and resulting images are defined by (6.1)–(6.4) Sartori–Stroppel, Definition 6.1.
The goal is the full form of the paper's isomorphism theorem:
Here , , and satisfy Assumption 5.5: and . The inequalities separate the relevant eigenvalues. The explicit condition is needed for Theorem 5.2 in the paper's dimension argument; Assumption 5.5 alone does not imply it Sartori–Stroppel, Assumption 5.5 and Theorem 5.2.
The milestone list records the finite-dimensional inverse and square-root result (Proposition 4.2), the inverse sandwich identity (Lemma 8.7), the changed contraction parameter (Lemma 8.4), the equal-orientation involution (Lemma 8.5), the Jucys–Murphy image identity (Lemma 6.6), and the dimension of the spectral corner (Corollary 5.8 with Lemma 5.9). The last two are stated in algebraic forms that avoid taking the sought map or category as extra hypotheses.
The theorem gives an explicit dictionary between diagram generators and operators in a cyclotomic quotient, including the change from the quotient's loop parameter to the source parameter Sartori–Stroppel, Remark 6.3. It also identifies the whole corner, rather than merely producing a homomorphism into it. This lets properties of the larger algebra be transported to the diagram algebra when their hypotheses are met. The paper discusses graded cellular and Koszul consequences, and an oriented-category extension, separately Sartori–Stroppel, Remarks 6.4–6.5.
A formal development must establish that the presentations do not collapse, that every required oriented relation survives the generator assignment, and that the image fills precisely . The milestone statements isolate several of the authors' central identities, while the final theorem retains injectivity and surjectivity. A proof would also create reusable infrastructure for quotient presentations with source and target idempotents and for inverses in idempotent corners.
The formulas for the images involve inverses and square roots after a spectral truncation, and the quotient need not be semisimple. Substituting a scalar directly into a formal power-series identity does not justify the key contraction identity in that setting; the authors explicitly point out this obstruction Sartori–Stroppel, Remark 6.3. The oriented relations also contain dotted symbols that stand for several local choices, so a single equation between global sums does not fully state every relation. Finally, proving that the map exists is only one part of the theorem: its image and kernel require separate control.
Lean represents both algebras as quotients of free complex algebras by the paper's generators and relations. An orientation is a Boolean sequence with exactly true entries; true denotes an upward arrow. Positions start at zero in Lean, so a paper index corresponds to Lean index . Relations involving dotted generators are imposed for every composable choice with the same source and target. Invalid orientation choices are zero. The affine quotient uses ; the source of the theorem uses . The recurrence fixes every rather than leaving later parameters free.
The , intermediate , and are defined from the polynomial spectral-idempotent characterization, rather than supplied as arbitrary hypotheses. An inverse of is selected by its two inverse equations in the corner . Square roots are not unique in the source, so each theorem holds for every family of polynomial square roots satisfying ; the factorized form is used. A vacuous hypothesis, a collapsed or under-related presentation, a freely chosen , or a merely linear map does not express this target. The conclusion requires multiplication, the specified generator values, injectivity, and range exactly .
The category construction and the paper's later applications are outside this mission. The needed reusable pieces are the finite-dimensional algebra lemma, oriented presentation machinery, polynomial spectral idempotents, and corner algebra operations. Contributions that strengthen the supporting algebraic library or close any of the stated milestones are within scope.
The Birman–Murakami–Wenzl (BMW) algebras were introduced by Birman and Wenzl and by Murakami to study the Kauffman link polynomial; they are deformations of the Brauer algebras and act as centralizer algebras of quantum groups of orthogonal and symplectic type on tensor powers of the natural module. Their cyclotomic generalization was introduced by Häring-Oldenburg (J. Pure Appl. Algebra 161 (2001)) as the BMW analogue of the Ariki–Koike algebras, the cyclotomic Hecke algebras of type . Representation theorists care about when such an algebra is semisimple: in the semisimple case its representation theory is governed by a combinatorial index set (multipartitions with extra data), and outside it one needs decomposition numbers.
For the Ariki–Koike algebra the answer is Ariki's criterion (J. Algebra 169 (1994)). For the ordinary BMW algebra () it is due to Rui and Si (J. Reine Angew. Math., [17] in the paper). Rui and Xu proved that the cyclotomic BMW algebra is free and cellular for odd under their u-admissibility conditions (arXiv:0801.0465), and Goodman and Hauschild Mosley (arXiv:math/0612064) and Yu (PhD thesis, Sydney, 2007) obtained freeness by other routes. Rui and Si (arXiv:0807.4149, 2008) extended cellularity to even and, by computing Gram determinants of cell modules, gave a semisimplicity criterion for all . That criterion is the goal of this mission.
Let be a field and positive integers. Fix non-zero with and the pairwise distinct, and a sign . Put if is odd and if is even, , ( odd), ( even), and
These are the u-admissible parameters of Assumption 2.2. The cyclotomic Birman–Wenzl algebra is the unital associative -algebra generated by () and () subject to the relations a)–k) of Definition 2.1: among them the Kauffman skein relation , the braid relations, , the skein relations between and , the unwrapping relations for all , the tangle and untwisting relations, , and the cyclotomic relation . The Ariki–Koike algebra is generated by with , the braid relations, , commuting and .
Write for " for ", and set
For and :
(a) if for some , or for some , then is not semisimple;
(b) if for all and no lies in , then
and for , is semisimple if and only if (a) ; (b) whenever , ; (c) for all ; (d) for all . For the goal states that semisimplicity implies (a)–(d).
The page states (b)(2) as an equivalence for all . The goal keeps only necessity at : Proposition 6.2 and Lemma 6.3 describe the same cell module of and list different exclusions ( against for odd ), and at contains neither.
The rank (Theorem 2.14); the corner identities (Lemma 3.1) and (Corollary 3.2), corrected at the two-strand boundary by requiring some ; Proposition 6.1, which says that is non-zero exactly when () and no lies in ; Proposition 6.5(b), non-semisimplicity when that determinant vanishes; and the reduction " not semisimple not semisimple" from the proof of Theorem 6.8.
The criterion gives a closed list of parameter values at which the cyclotomic BMW algebra fails to be semisimple, and so, by Graham–Lehrer theory, the parameters at which all cell modules are simple and pairwise non-isomorphic. Outside that list the algebra's simple modules, their dimensions and the decomposition of tensor-type modules are given by the combinatorics of up-down tableaux; inside it, the list says which Gram determinants vanish and where decomposition numbers begin. For it specializes to the semisimplicity criterion for BMW algebras, and its conditions (a)–(b) are Ariki's conditions for .
As far as is known, none of this is machine-checked: Mathlib has no BMW, Brauer, Ariki–Koike or Iwahori–Hecke algebras and no cellular algebras. The mission formalizes the statements of the paper on a presentation of by generators and relations; a solver must supply a basis (or at least a dimension count), the cellular structure and the Gram-determinant computations. The paper leaves several of its proofs to the reader ("by arguments in the proof of [19, 5.41]"), so the formal proofs would also close gaps in the published argument.
Non-semisimplicity in part (a) needs only one degenerate bilinear form on a non-zero cell module, but showing that the module is non-zero, or that does not collapse, already needs a lower bound on the dimension of a presented algebra, which no rewriting argument provides: the rank is proved in the literature through seminormal representations. Sufficiency in part (b) requires the Gram determinants of all cell modules , which the paper obtains by a recursion over up-down tableaux; vanishing of a single factor must be traced through branching and Morita-type functors between levels , and . Ariki's criterion for is itself an external input.
and are RingQuot quotients of FreeAlgebra F on finite generator types; indices are 0-based (the Lean T i is the paper's ), and is a separate generator tied to by relation a). The sign is the free parameter and are computed from , so the parameters are u-admissible by construction. The are pairwise distinct (Assumption 2.2(1) divides by ; the paper extends 2.2 to coincident through [19, 3.11]). "Semisimple" is Mathlib's IsSemisimpleRing. The condition is written as for , not through orderOf, which is for elements of infinite order. Relations d) and g) both use , which equals the paper's for these parameters; were they different, the presentation would collapse. The corrected corner milestones require or some in Lemma 3.1, and or some in Corollary 3.2. At , , , , and , every vanishes, exposing the missing condition. is expressed as the Hankel determinant of the , and is the subalgebra generated by the first generators.
A presentation that collapses to the zero algebra would make the goal false in part (a) but trivially true elsewhere; the rank milestone rules this out. Replacing semisimplicity by non-vanishing of Gram determinants would turn the goal into a different theorem and is not acceptable.
A complete development needs a basis theorem for , cellular algebras and Graham–Lehrer's semisimplicity criterion, the Ariki–Koike algebra and Ariki's criterion, and Gram-determinant computations. The cellular-algebra layer and the Ariki–Koike algebra are reusable beyond this mission; contributions of any of these, or of the milestones on their own, are welcome.
Sending classical messages through a quantum device requires choosing input states that remain distinguishable after noise. The one-shot classical capacity measures the best information rate when each channel use is signaled with a separate input state. For many channels the optimization is difficult because it ranges over all ensembles of quantum states. Fermionic systems provide a finite-dimensional setting in which the noise has a direct description on elementary operators, but the optimal signaling states still need not be obvious. Bravyi's 2005 paper isolates a family of fermionic product channels, computes the best rate from Gaussian input states for any number of qubits, and proves that this restricted rate is the full one-shot rate for one or two qubits.
The system has qubits, with computational basis indexed by bit strings . The Jordan–Wigner Majorana operators are tensor products of Pauli matrices: has on qubits before , on qubit , and identity afterwards; replaces with . Their ordered monomials , , form a basis of all operators on the qubits. The paper gives these operators and their monomials in Eq. (3).
A fermionic product channel is determined by attenuation coefficients . On each monomial it acts by , and linearity defines it on every operator. A state is a positive semidefinite matrix of trace one. For a finite ensemble of output states , with nonnegative weights summing to one, its Holevo quantity in bits is
The supremum of over all finite ensembles of outputs of is . A Gaussian state has the specific form of Definition 1: , each , and for Hermitian quadratic and linear combinations of Majorana operators. Requiring Gaussian input states gives . Setting gives an even Gaussian state. These are separate classes; the even class supplies an intermediate entropy minimum. Definition 1 and Eq. (13) are on page 4.
Write for the coefficients in decreasing order, and let . The main formula, Theorem 1 and Eq. (6), is
It holds for every and every unsorted . The milestones identify the covariance and Gaussian-preservation facts, the exact even and general Gaussian minimum-output entropies, and an ensemble attaining the capacity.
The second clause of Theorem 1 states
Thus restricting the input ensemble to Gaussian states loses no one-shot capacity in these dimensions. The paper does not prove this equality for arbitrary .
The formula replaces an optimization over arbitrary finite Gaussian ensembles with binary entropies of sorted attenuation coefficients. In the one- and two-qubit cases it also settles the unrestricted one-shot optimization for this channel family. The intermediate result relates signaling directly to minimum output entropy; the even-Gaussian and Gaussian minima make the distinction between the two state classes explicit. These relationships are established in Sections II–IV of the paper.
The mathematical results are proved in the 2005 paper. This mission asks for machine-checked proofs of their exact finite-dimensional statements. The definitions of bit-valued von Neumann entropy, finite output ensembles, ordered Majorana monomials, Gaussian-state predicates, and covariance matrices can support later work on fermionic channels. The submitted goal and milestones are presently proof obligations rather than claims of existing Lean proofs.
The channel is simple on each Majorana monomial, but the entropy of a general output state is not determined by its one- and two-point correlations. Even within the Gaussian class, optimizing only the even Gaussian states gives a different formula from optimizing all Gaussian states: linear Majorana terms change the optimum. A direct search over density matrices therefore does not expose the closed expression in Theorem 1. For the unrestricted two-qubit clause, one must also relate arbitrary states to the Gaussian class; the paper invokes a three-qubit parity result for that step. The distinctions and parity result appear in Sections III–IV.
Lean represents qubit basis vectors by Fin n → Fin 2 and operators by complex matrices on that finite type. Majorana indices start at zero in Lean, so the paper's correspond to consecutive indices . The Jordan–Wigner tensor factor at coordinate acts on qubit ; the monomial product follows increasing Majorana index. The channel is defined on all matrices by the trace-orthogonal monomial expansion of Eq. (4), not merely on covariance matrices. Attenuations may equal zero or one. Entropies use logarithms to base two, with .
Every capacity uses a real supremum over all finite normalized ensembles, with arbitrary ensemble size. The inputs are density matrices, and their channel outputs must be density matrices. The Gaussian capacity requires every input to satisfy Definition 1; Lemma 2 ensures these outputs are Gaussian too. The minimum-output quantities are real infima over their stated input classes, and the corresponding milestone theorems assert attainment. For the actual channels the relevant sets are nonempty and bounded: the maximally mixed state supplies an output state, while every Holevo quantity lies between zero and . This representation rules out restricting the Gaussian ensemble to the displayed optimizing family, assuming the goal's coefficients are initially sorted, or replacing bit entropy with natural-log entropy.
The development needs finite-matrix functional calculus, positivity, matrix exponentials, permutation and singular-value reasoning, and finite ensemble entropy bounds. Contributions to those reusable layers and to the paper's covariance, Gaussian-preservation, and minimum-output results are within scope. Lemma 3 is stated in its even-Gaussian form, which its proof establishes; the displayed lemma says only “Gaussian.”