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.
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?
Social networks exhibit triadic closure: two people with many friends in common tend to be friends themselves. Fox, Roughgarden, Seshadhri, Wei and Wein (arXiv:1804.07431, SIAM J. Comput. 2020, doi:10.1137/18m1210459) turn this empirical regularity into a distribution-free graph class and ask which algorithmic problems that are hard on worst-case graphs become tractable on it. Their test case is the enumeration of maximal cliques, a standard primitive of community detection. On a general -vertex graph the number of maximal cliques can be (Moon and Moser, 1965), so no enumeration algorithm can be polynomial. The question is how far triadic closure alone pushes this count down.
Timeline:
All graphs are finite, simple and undirected; is the set of neighbours of a vertex , and for , is the subgraph induced by .
For a positive integer , is -closed if any two distinct vertices with are adjacent. A 1-closed graph is a disjoint union of cliques, and every graph on vertices is -closed, so interpolates between the two. Being -closed passes to induced subgraphs, with common neighbours counted inside the subgraph.
A clique is a set of pairwise adjacent vertices; it is maximal if no further vertex can be added. Write for the number of maximal cliques of , and
The proof uses four further objects, computed in the current induced subgraph: the maximum degree ; for a non-empty set of vertices, ; the set of vertices at distance exactly from ; and the function
For all positive integers and every -closed graph on vertices,
For fixed the exponent is , strictly below , which is what the improvement over Theorem 2.1 consists of. The constant is the one printed in the theorem.
The milestones follow the proof on pp. 9–11:
Together with Theorem 2.1, Theorem 3.1 gives Theorem 1.4 of the paper: a -closed graph on vertices has at most maximal cliques. For constant the count is polynomial with exponent below , so all maximal cliques can be listed in polynomial time, and the problem is fixed-parameter tractable in . Theorem 4.1 shows the exponent cannot drop below for , so the bound is polynomially tight for .
The result is proved in the paper; it has not been formalized. This mission produces a machine-checked proof of Theorem 3.1 together with the steps of the paper's argument. The printed argument has gaps that a formal proof must close: the base of the exponential factor changes from to in the middle of the proof, Claim 3.3 is applied with that may exceed , the induction meets the empty graph (one maximal clique, while ), and the recursion deletes vertices where the recurrence writes . A proof that also closes the stronger base- bound, which the arithmetic suggests, would be a welcome addition.
The count of maximal cliques through a vertex reduces to , which is -closed, so a naive induction on gives . When the maximum degree is large this is no better than . The high-degree case needs a separate count of the cliques that meet without containing , grouped by their trace on ; bounding the sum over these traces requires the convexity of in its first argument and the constraint coming from -closedness. The resulting recurrence then has to be solved with explicit real exponents of the form , for all simultaneously, with the induction on and arranged so that the empty graph never enters the inductive hypothesis.
SimpleGraph (Fin n). The general statements are over a finite vertex type with decidable equality.Set.ncard and reads "at least " as c ≤ ncard, not c < ncard. The relative notion IsCClosedOn c G W counts common neighbours inside and is equivalent to -closedness of G.induce W.Finset that is maximal under inclusion among cliques contained in ; the empty graph has exactly one maximal clique. Neither all cliques nor maximal cliques of a different graph are counted.Everything is built from Mathlib's SimpleGraph, commonNeighbors, IsClique, Maximal and Real.rpow. The definitions of -closedness and of the maximal-clique count come from the reviewed shared module CClosedGraphs.Peeling.Setting. Contributions welcome: proofs of the milestones, a proof of the goal by a different route, and the base- strengthening.
Stochastic optimization methods often see only noisy gradients. For a nonconvex objective, a useful guarantee is that an output point has a small gradient: this is a first-order stationarity certificate, even when there is no claim that the point is globally optimal. A guarantee on the expected squared gradient leaves open how often one particular run succeeds. The two-phase randomized stochastic gradient method of Ghadimi and Lan (2013) addresses that question by generating several candidates and using further oracle calls to select one. The paper gives an explicit bound on the probability of failure and on the number of oracle calls needed for a prescribed accuracy and confidence.
The work sits within stochastic approximation, where the objective may be a population expectation or another function accessible through noisy observations. The 2013 paper develops first- and zeroth-order methods for smooth nonconvex problems. This mission concerns its two-phase first-order result, Theorem 2.4, rather than the Gaussian smoothing results in its later section. The source for every index here is the arXiv v1 preprint; the printed page and PDF page coincide.
The objective is a differentiable function bounded below, with true optimal value . Its gradient map is -Lipschitz: for all . The mission uses . No convexity is assumed.
A stochastic first-order oracle returns a vector when called at the current iterate . Assumption A1 says that the oracle is unbiased at that iterate and has squared error of expectation at most . The noise may depend on earlier calls. In the formal model, the mean is conditional on the past, and the oracle and squared-error random variables are integrable. This makes explicit the probabilistic assumptions used when the paper takes expectations. The model takes because the paper's displayed stepsize and post-optimization sample size otherwise degenerate under Lean's total division convention.
A randomized stochastic gradient run starts at and uses . It chooses an output index with the probability mass function in equation (2.3), independently of that run's oracle noise, and outputs . For a parameter , the constant stepsize in equation (2.13) is . The paper writes and
The two-phase method makes independent RSG runs, yielding . For each candidate it averages fresh oracle outputs into an estimated gradient . It selects a candidate whose estimated-gradient norm is minimal. The post-optimization samples for different candidates may be recycled; the paper explicitly permits this. The candidate itself is known when its post-optimization samples are taken, so the conditional oracle assumption is stated relative to a filtration that contains it at time zero.
The first target is the one-run mean bound of Corollary 2.2, , followed by the one-run tail bound (2.19). Lemma 2.3(a) controls the squared norm of a sum of vector martingale differences. Equation (2.28) relates a selected candidate's true gradient to the best candidate and the estimation errors. Equation (2.29) factors the probability of simultaneous failure across independent runs and bounds it, while (2.30) bounds the other source of failure: every optimization run performing poorly, and at least one estimated gradient being inaccurate.
For arbitrary positive , Theorem 2.4(a) states the stronger quantitative tail bound
The goal, Theorem 2.4(b), specializes those parameters to an accuracy and failure probability . It sets
An -solution is a point satisfying . With those parameter values, the method computes such a point using at most stochastic first-order oracle calls. The formulas and constants above are those of equations (2.24)–(2.27) of the preprint.
The result turns a mean stationarity bound into a confidence guarantee for one returned point, with an explicit accounting of both candidate generation and candidate assessment. It identifies how the number of independent runs, iterations per run, and gradient estimates scale with the requested accuracy and failure probability. Without the post-optimization phase, the paper's direct Markov estimate (2.19) gives a less favorable dependence on the failure probability for a single run.
The mathematical theorem is proved in the 2013 paper; the Lean declarations in this proposal are statements awaiting machine-checked proofs. A completed formalization would give reusable definitions for a dependent-noise gradient oracle, a random-output stochastic-gradient run, and a post-optimization selection procedure. The vector martingale estimate and finite-candidate inequality could also serve later stochastic-optimization developments. Contributions to the probability and measurability infrastructure, as well as the final rate proof, are within scope.
Selecting the candidate with the smallest estimated gradient need not select the one with the smallest true gradient. The estimates are random and are evaluated at candidates that are themselves random outputs of earlier oracle runs. A bound for a fixed point does not address this dependence. The argument needs a conditional oracle contract at each candidate and a separate guarantee that the optimization runs supply a sufficiently good candidate. The paper's intermediate display (2.31) applies a fixed-candidate tail estimate to the selected candidate even though the selection examines the same estimates; that step is not justified by the stated assumptions. The final bound can be phrased without treating (2.31) as a separate target.
The space is EuclideanSpace ℝ (Fin n). Iterations and oracle samples retain the paper's one-based indexing; candidate runs use Fin S, which reindexes the paper's . The objective's true infimum is carried by IsGLB (Set.range f) fstar, so cannot be weakened by substituting an arbitrary lower bound. Each candidate is generated by the RSG recursion and the mass function (2.3); the one-run performance bound is a theorem, not a hypothesis of the two-phase model. Independent candidate outputs are required for (2.29). The selected candidate may be any minimizer of the estimated-gradient norm, with any tie rule; no measurability of the selection is assumed.
All expectations are Bochner integrals, with integrability included in the oracle assumptions and in the one-run conclusion. Probabilities are ℝ≥0∞ values. The noise carrier is generalized from the paper's Borel subsets of Euclidean space to a measurable type. The general vector martingale lemma omits the paper's Polish-space and trivial-time-zero conditions; neither is needed for its squared-norm bound, and the latter would conflict with a candidate known at time zero. Its non-strict tail statement is restricted to a positive sum of variance bounds, because the printed version is false when every bound is zero. The goal reads the logarithm in (2.24) as base two, matching the paper's final comparison. Positive and avoid zero steps and an empty post-optimization average.
The formal goal states the probability guarantee. The oracle-call bound follows directly from the algorithm's two loops and is recorded in the theorem's prose rather than in a separate operational semantics for calls. A complete proof may use Mathlib's conditional expectations, independent random variables, finite sums, and real logarithm and ceiling libraries. No assumption may simply postulate the one-run gradient bound or the final success probability.
Mobile devices run applications whose computational demand often exceeds what a battery-powered processor can serve with acceptable delay. Computation offloading sends part of the work elsewhere: to a cloudlet, a small cluster of servers one wireless hop away, or to a distant cloud reached through the wide-area network. When many users share one cloudlet, each user's response time depends on how much the others offload, and selfish users interact strategically. Cardellini, De Nitto Personé, Di Valerio, Facchinei, Grassi, Lo Presti and Piccialli (Math. Program., 2016) model this interaction as a generalized Nash equilibrium problem (GNEP): every user minimises its own expected cost, and all users share a coupling constraint that caps the cloudlet's utilisation.
The paper computes equilibria through a variational inequality (VI) reformulation and, for distributed computation, through an extended game with a price player. The convergence of the methods it relies on (proximal-point and best-response schemes for monotone VIs, see Facchinei and Pang, 2003) requires the VI map to be monotone. This mission formalizes the paper's Theorem 1, which gives an explicit, checkable condition on the model's parameters under which that map is monotone.
There are users . Each user splits its task stream over three tiers (own device, cloudlet, cloud) and chooses fractions ; a strategy profile is . The data are positive rates combined into (the traffic intensities a user generates on its device, the wireless link, the cloud path and the cloudlet), power parameters , the number of cloudlet servers, the offloadable fraction and the utilisation cap .
The cloudlet load is and . User 's private feasible set consists of the with , and the power budget . The shared constraint is , and the joint feasible set is . User minimises
Assumption A requires and all to lie in .
The VI map stacks each user's gradient in its own variables:
is monotone on if for all . Finally .
Under Assumption A, if
then is monotone on . The condition involves only the data of the game, so the goal is the paper's statement with no constant changed.
The milestones follow the paper's argument in order.
Theorem 1 is the hypothesis under which the rest of the paper operates. The extended game of §5.2 inherits the monotonicity properties of (p. 14), and the distributed solution methods of §6 are designed for that monotone setting. Condition (18) translates monotonicity into a statement about the system: the largest per-user cloudlet traffic intensity must stay below a threshold that grows with the number of servers and shrinks with , and . Remark 1 (p. 14) stresses that (18) is only sufficient.
The result is proved in the paper; this mission produces a machine-checked proof. On the way it yields statements reusable outside this model: the Jacobian criterion for monotonicity of a differentiable map on a convex set, and the spectrum of the symmetric rank-two matrix . None of these statements is on the platform; the Schur product theorem, which the proof also uses, is referenced as a published platform theorem.
The Jacobian is not symmetric: carries the row user's own term , so in general, and the eigenvalues of say nothing directly about its quadratic form. The quadratic form must be controlled uniformly over the whole feasible set , whose shape (simplices cut by the cap , the power budgets and the shared constraint) enters the final bound, and the condition must come out in the paper's exact constants. In Lean, the main costs are the coordinatewise Fréchet derivative of on , the characteristic polynomial of a rank-two matrix of arbitrary size, and the passage from a characteristic polynomial to positive semidefiniteness.
Users are Fin N (0-based); tiers are a three-element type Tier; a profile is Fin N → Tier → ℝ. The inner product on is written out as , and the norm on in (21)–(23) is the Euclidean norm written as , because Mathlib's norm on function types is the sup norm. is defined by the closed form of p. 11, not as a derivative, so milestone 2 has content. is the real supremum of the , which is the maximum for .
Standing hypotheses carried by every statement: Assumption A, and . Disclosed choices relative to the page:
The formulas for , , and divide by and , and Lean sets . Every statement is therefore restricted to or to a region where these denominators are nonzero; monotonicity on the larger set , where can vanish, is a different and false-by-junk claim and is not posed. is nonempty for admissible data (e.g. all users computing locally), so the goal is not vacuous.
Contributions welcome: proofs of any milestone, especially the generic ones (1 and 6), which belong in a general library.
Twin-width was introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021) as a graph parameter under which first-order model checking is fixed-parameter tractable when a contraction sequence is given. Its interest lies in the classes it covers at once: planar and, more generally, -minor-free graphs, bounded-degree grids, unit ball graphs of bounded clique number, and the classes of bounded rank-width or clique-width. These are the classical dense-graph width measures, for which FO (indeed MSO) model checking was already known to be tractable through Courcelle–Makowsky–Rotics.
This mission formalizes the link to the dense width measures, stated in the paper through boolean-width (Bui-Xuan, Telle and Vatshelle, Theor. Comput. Sci. 412(39), 2011). It is known that (Vatshelle's PhD thesis, Chapter 4), so a bound on twin-width in terms of boolean-width shows that bounded twin-width captures bounded rank-width, clique-width, module-width and boolean-width simultaneously.
Let be a finite simple graph on a vertex set .
Two vertex sets are homogeneous if either all pairs are edges or none is. For a partition of , a part has red degree equal to the number of other parts that are not homogeneous to ; is a -partition if every part has red degree at most . The graph has twin-width at most , written , if there are partitions of with the partition into singletons, having at most one part, each obtained from by merging two parts, and every a -partition. This is the paper's partition form (p. 3:32) of its definition through trigraphs and red edges (pp. 3:11–3:12).
A decomposition tree of is a rooted binary tree , every internal node having exactly two children, whose leaves are in one-to-one correspondence with . Each edge of lies above exactly one rooted subtree and induces a cut of : is the set of leaf labels of that subtree and . For disjoint write
the number of different neighbourhoods in of subsets of , the empty subset included. The boolean-width of the cut is , the boolean-width of is its maximum over the edges of , and is the minimum over all decomposition trees. In Lean, nbhdCount G A B is , and BoolWidthLE G N states that some decomposition tree has on every edge, so is BoolWidthLE G (2^k).
Every graph with boolean-width has twin-width at most . With , the integer neighbourhood count,
The theorem places the classes of bounded boolean-width, and therefore of bounded clique-width and rank-width, inside the classes of bounded twin-width, with a single-exponential bound. Combined with the paper's model-checking algorithm, it recovers tractability of FO model checking on these classes once a contraction sequence is computed, and it situates twin-width as a common generalization of the dense width measures and of sparse classes such as -minor-free graphs.
No machine-checked version of twin-width or boolean-width is known to exist; neither notion is in Mathlib. The mission produces Lean definitions of twin-width in partition form, of decomposition trees and of the neighbourhood count behind boolean-width, together with the four combinatorial steps the paper's proof states explicitly. The definitions are shared, in identical form, with the other missions of this series on the same paper.
The first three milestones are elementary: a counting bound on contraction sequences, a walk down a binary tree, and a pigeonhole argument. The fourth is a direct count of non-homogeneous parts.
The difficulty is the iteration. After the first contraction the leaves of the updated tree are contracted vertices, so "the same neighbourhood in " must be read as homogeneity to all of for a set of vertices, and the boolean-width bound of the cuts must be re-established for sets rather than single vertices. The paper asserts the invariant that the contractions never create a red component of more than vertices without proving it. A complete proof of the goal therefore has to supply an invariant, carried through all contractions, that keeps every part's red degree below . The naive repetition of the first step does not by itself control red edges between previously contracted parts.
Twin-width is the predicate TwinWidthLE G d, never a numerical infimum, so a junk value of an empty or unbounded infimum cannot make the goal trivial. A contraction sequence must merge exactly two parts at each step and start from singletons; it cannot jump to one part. Homogeneity counts all pairs between two parts, in both of its alternatives. Boolean-width is bounded on every edge of the decomposition tree, not only at the root, and the count runs over neighbourhoods of all subsets of , not only of single vertices. The bound depends only on , not on the graph.
Boolean-width is kept as the integer count ; since means that the least admissible count is , the Lean goal for this is exactly the printed theorem. Subtractions are in and exact where used. Graphs live on a Fintype vertex type with decidable equality and decidable adjacency. A graph on the empty vertex set has no decomposition tree; the goal is silent about it, and it has twin-width . No hypothesis is added to any statement relative to the page except in milestone 2, which the page has implicitly () and without which the conclusion is impossible.
The definitions needed are the setting module TwinWidthI.BoolWidth.Setting: merge steps, homogeneity, -partitions, twin-width, decomposition trees (DTree), the count and BoolWidthLE. Proofs of the milestones, a proof of the goal, and lemmas towards the iteration invariant are welcome.
The Yukawa potential (or screened Coulomb potential)
was introduced by Hideki Yukawa in 1935 to model the short-range nuclear force as the exchange of a massive particle, later identified with the pion. The same profile reappears as the Debye–Hückel screened interaction in plasmas and electrolytes, as the static Green's function of the massive Klein–Gordon (screened Poisson) operator, and as the Newtonian correction in massive-graviton models. The mathematical facts behind these uses are classical, short, and stated in every textbook treatment — which makes them a natural, self-contained target for formalization: each one is an explicit identity of real analysis in three dimensions.
Timeline. Heisenberg (1932–33) proposed a short-range exchange interaction between nucleons; Fermi (1934) introduced exchange of light particles in beta decay; Yukawa (1935, Proc. Phys.-Math. Soc. Japan 17, 48) combined the two ideas, derived the potential above, and predicted a mediating particle of mass about 200 electron masses; the pion was observed in 1947.
Throughout, is the coupling (amplitude) constant, a scaling constant, the mass of the exchanged particle and the radial distance; is the range. The potential is the function
Points of space are with Euclidean norm , and the potential of a point source at the origin is . The Laplacian is the usual sum of unmixed second partial derivatives on . For a uniform, infinitesimally thin spherical shell of radius with total scaling constant , the potential felt by a point of scaling constant located at is
the average over the unit sphere (uniform surface measure ) of the pair interaction.
For and every ,
This is the identity the article's sections Fourier transform and Feynman amplitude rest on: the momentum-space Yukawa potential is the massive propagator times .
The results. The Fourier identity is what makes the Yukawa potential the non-relativistic limit of single-meson exchange; milestone 3 identifies it as the Green's function of the screened Poisson operator ; milestones 5–7 give the Born-approximation scattering amplitude and the closed-form total cross section quoted in quantum mechanics textbooks (e.g. Griffiths); milestones 8–9 are the Yukawa analogue of Newton's shell theorem, whose failure to reduce to a point source of the same strength is the reason massive-graviton models violate the weak equivalence principle.
Formalizing them. All statements are classical and proved on paper. The mission produces machine-checked versions together with reusable infrastructure: three-dimensional Fourier integrals of radial functions, Laplacians of radial functions, spherical averages with respect to the surface measure, and conditionally convergent oscillatory integrals.
The individual computations are short on paper but each crosses a gap in the library. The goal requires reducing a three-dimensional Lebesgue integral of a radial function to a one-dimensional integral (polar coordinates in ), then evaluating . The inverse transform is not absolutely convergent — is not integrable on — so the naive Lebesgue statement is false (it would assign the value ); only the ball-truncated limit is meaningful, and its evaluation needs the improper integral . The shell theorem needs the surface measure on and the Archimedes-type change of variables .
All quantities are real numbers; space is EuclideanSpace ℝ (Fin 3) with Lebesgue measure. The potential is a single definition YukawaPotential.yukawaPotential g α m r; at Lean's division convention gives the junk value , so every statement either restricts to / or integrates (where a single point is null). The physical conventions , (and where the article divides by ) are explicit hypotheses. The Fourier transform uses the convention , ; the inverse is stated as a limit over balls. The shell potential averages over the unit sphere with Mathlib's Measure.toSphere (uniform surface measure); since it is an average, its normalisation is irrelevant. The Laplacian is Mathlib's Laplacian.laplacian on inner-product spaces. Physical constants in milestones 5 and 7 are arbitrary reals: the identities hold without sign assumptions on them.
Out of scope: the historical mass estimate of the pion, the heuristic wave-equation derivation of the photon/pion dispersion relations, the perturbative asymptotic expansions of Schrödinger eigenvalues and Regge trajectories (stated in the source only up to unspecified and "" terms), and the limits of the shell formulas.
Contributions welcome: polar-coordinate integration for radial functions on , spherical-average lemmas, and the improper integrals above as standalone lemmas.
In the usual textbook presentation, quantum theory starts from postulates that have no obvious operational meaning: states are density operators on a complex Hilbert space, measurements are positive operators, and probabilities are given by the trace formula . In Quantum Theory From Five Reasonable Axioms (Hardy 2001), Lucien Hardy asks whether this structure can instead be derived from simple statements about preparations, transformations and measurements, in the same way that classical probability theory can be set up by pure thought. He proposes five axioms (probabilities, simplicity, subspaces, composite systems, continuity) and argues that they single out finite- and countably-infinite-dimensional quantum theory. Dropping a single word, "continuous" in Axiom 5, leaves classical probability theory instead.
The paper is one of the starting points of the operational or generalized probabilistic theory (GPT) approach to the foundations of quantum mechanics. It was followed by reconstructions that replace the simplicity axiom, e.g. Dakić–Brukner 2009, Masanes–Müller 2011 and Chiribella–D'Ariano–Perinotti 2011.
A system is described by two integers. The dimension is the maximum number of states that can be distinguished in a single-shot measurement. The number of degrees of freedom is the minimum number of probability measurements needed to determine the state. The state is the vector of the probabilities of fiducial measurements. States are not assumed normalized: the null state (no system present) is allowed. The set of allowed states is convex, and its pure states are its extremal points other than .
The five axioms are:
A probability theory can be summarized by its signature , defined through
Classical probability theory has and . Complex quantum theory has and . Real and quaternionic quantum theory have and .
Section 8.1 shows that Axiom 3 forces , and Axiom 4 forces . The goal theorem is the purely arithmetic consequence (Eq. (57)):
The milestones follow the paper's own steps, in the paper's numbering:
The goal is the step at which the two structural axioms (subspaces and composites) cut the space of possible theories down to a single integer parameter . Combined with Section 8.5, which rules out by continuity, and with the simplicity axiom, it gives . Everything after that in the paper (the Bloch sphere, general , the trace formula, complete positivity) is carried out inside the case. The milestones on signatures make precise in which sense real and quaternionic quantum theory are excluded: their degree-of-freedom counts are not multiplicative under composition.
The paper's argument is informal physics. This mission isolates the mathematically precise statements that the argument relies on, so that they can be proved independently of the physical interpretation. It does not formalize the axioms themselves as a single Lean structure.
The arithmetic goal is an instance of a classical question about monotone completely multiplicative functions. Complete multiplicativity alone fixes only through its values at the primes, which are a priori unrelated to one another, and monotonicity is the only link between different primes. The step from a real exponent to an integer exponent is a separate integrality argument that the paper does not spell out. The linearity milestones need care because the hypotheses hold only on a convex set containing , not on all of . The milestones are explicit but delicate algebra with square roots and boundary cases .
HardyFiveAxioms. State vectors are functions Fin K → ℝ. Indices are -based, so the paper's fiducial vector is index .ℕ → ℕ (goal) or ℕ → ℝ (Appendix 2), constrained only at arguments . The value at is irrelevant.[x₁, …, x_L], and is written as the binomial coefficient .Set.extremePoints ℝ S \ {0}. The classical state space is .vecMulVec v (star v) over ℂ, and the qubit matrices , , and the roots are explicit definitions.unitInterval → ℝᴺ that stays inside the pure states.Contributions are welcome on any milestone. The linearity, extreme-point and positive-definiteness lemmas are reusable beyond this mission.
Whether the gravitational field must be quantized is a long-standing foundational question. One family of arguments, due to DeWitt (1962) and Eppley and Hannah (1977), claims that consistency alone forces quantization: a classical field coupled to a quantum system would supposedly violate momentum conservation, the uncertainty relations, or the impossibility of superluminal signalling. Albers, Kiefer and Reginatto (Phys. Rev. D 78, 064051 (2008)) dispute this claim. In their Sec. IV they give an explicit counterexample: a hybrid model in which a classical gravitational wave interacts with a quantized massive scalar field. The model is the two-dimensional scalar theory of gravity of Nordström, written in the formalism of ensembles in configuration space.
This mission is the second one on this paper. The first, Albers–Kiefer–Reginatto 2008: Measurement Analysis and Quantum Gravity, formalizes Sec. II (the reduced state of photon 2), Sec. III B and Sec. V, and lists Sec. IV and the appendices as out of scope. This mission covers the explicit non-interacting solution of Sec. IV A and the harmonic-oscillator analogy of Appendix A, which the authors use to interpret it.
Timeline.
Ensembles in configuration space. The state of the gravitational field together with the scalar field is a probability functional and a conjugate functional . They obey a modified Hamilton–Jacobi equation (37) and a continuity equation (38). The coupling constant is . For the authors use the ansatz and , with Gaussian functionals
and a one-particle Gaussian with kernel . Substituting the ansatz yields the kernel equations (43)–(48).
Mode representation. Every kernel is expanded in real orthonormal eigenfunctions of with eigenvalue . A kernel is then represented by its mode coefficient . Under this expansion , , and . The paper's solution is
Eqs. (49)–(51), (54), (55), where and are arbitrary constants.
Oscillator ensemble (Appendix A). For a unit-mass oscillator of frequency , a state is a pair . It satisfies and . The paper takes , and the Gaussian
For every finite family of modes and every time with , the coefficients (49)–(51), (54), (55) satisfy the mode forms of Eqs. (44), (45), (46), (47) and (48).
The goal is the precise content of the paper's explicit solution. It is the base point of the first-order hybrid solution in Sec. IV B, and it underlies the paper's counterexample to DeWitt's claim that "the quantization of a given system implies also the quantization of any other system to which it can be coupled". Appendix A provides the interpretation of that solution: the classical sector behaves like an oscillator ensemble prepared with zero momentum and no momentum uncertainty but localized in space.
Formalization adds exact hypotheses: where the cosines must be non-zero, the regularity under which the paper's "most general solution" claim holds, and a correction to the printed energy formula. The paper prints , which is correct only for ; Milestone 11 targets the corrected value. None of these statements has a machine-checked proof on the platform.
The Sec. IV A identities are trigonometric computations once they are reduced to modes, so their difficulty lies mainly in the side conditions. Milestone 7 is a uniqueness statement for a first-order linear PDE on a strip. It requires an argument along characteristics: exhibiting a solution is not enough. Milestones 9–11 are Gaussian integrals, and Milestone 10 is a weak limit of Gaussians whose variance tends to while the centre tends to .
tan, division, and deriv at degenerate points, so every statement assumes where it is needed.In the holographic correspondence (AdS/CFT), a strongly coupled quantum field theory in spacetime dimensions is described by classical gravity on an -dimensional anti-de Sitter spacetime. The first entry of the dictionary relates a scalar field of mass in the bulk to a scalar operator of scaling dimension in the boundary theory. This relation is used throughout applications to condensed matter ("AdS/CMT"): it fixes which operators are relevant, how sources and expectation values are read off from bulk solutions, and when a bulk field signals an instability towards an ordered phase (Hartnoll–Lucas–Sachdev, §1.6.2 and §6.2; see also Natsuume, AdS/CFT Duality User Guide).
This mission formalizes the elementary ODE facts behind that entry of the dictionary, as stated in the review of Hartnoll, Lucas and Sachdev.
The boundary theory has spatial dimensions. The bulk is Poincaré of radius ,
with the conformal boundary at . A scalar of mass squared (possibly negative) obeys . Writing gives the radial equation (27)
Near the boundary, solutions behave as powers with the mass–dimension relation (29)
whose roots are
For , a function on solves the radial equation with if and only if
for some constants . These are the two constants of integration (source) and (response) of (28); at the expansion (28) is exact.
The result itself. The goal says the space of zero-momentum solutions is two-dimensional and spanned by the two power laws, which is why a bulk scalar carries exactly one source and one response and why the source term scales as . The Breitenlohner–Freedman bound identifies the masses for which becomes complex, the criterion used in §6.2 to detect infrared instabilities.
Formalizing it. These facts are standard and proved in the physics literature at the level of rigor of a textbook computation. No machine-checked version is known to the drafter. The mission produces a small reusable layer (radial operator, solution predicate, exponents ) on which later statements of the review can build.
The milestones about are algebra. The goal needs uniqueness for a second-order linear ODE with a regular singular point at , on the open half-line: the naive "guess the power laws" argument only shows that are solutions, not that every solution is of this form. Mathlib's ODE uniqueness results are stated for Lipschitz vector fields, so an Euler-type equation has to be reduced to that setting (or handled by a change of variables) on .
Fields are real-valued functions ; only values on matter. Derivatives are Mathlib's deriv, and solutions are required to be on . The mass squared is a real parameter msq of any sign; is a natural number and is allowed. use the real square root, which is on negative input, so every statement that relies on being roots carries the Breitenlohner–Freedman hypothesis. The goal uses the strict bound, which excludes the saturating case where a logarithmic solution appears. Only is formalized; the general- asymptotic expansion (28), with Bessel-function solutions (37) and resonant logarithms, is out of scope.
The discrete optimal transport problem between two histograms is a linear program, and much of the algorithmic theory of optimal transport is the theory of solving that linear program well. Chapter 3 of Peyré and Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019) surveys the classical combinatorial solvers: the network simplex, dual ascent methods, and the auction algorithm. Dual ascent methods work entirely with the dual variables, the Kantorovich potentials : they keep a feasible pair of potentials and improve it step by step until it is optimal. The specialisation of this idea to assignment problems is the Hungarian algorithm of Kuhn (1955), and its general form is the primal-dual method for network flow problems presented in Bertsimas and Tsitsiklis, Introduction to Linear Optimization (1997, §7.7), on which §3.6 of the book is modelled.
The mathematical engine of every dual ascent method is one alternative: a feasible pair of potentials is either already optimal, or it can be improved along a direction of a very special, combinatorial form. This mission formalizes that alternative (Proposition 3.6 of the book) together with the results it rests on.
Fix integers , a cost matrix , and two histograms , , where is the probability simplex. Write for the row indices and, following the book, for the column indices.
The couplings between and form the transportation polytope
and the primal problem is with . A pair of vectors is dual feasible, written , when for all . The dual problem (3.4) is
For a feasible pair , a pair of indices is balanced if and inactive if . A matrix and a pair are complementary if implies , that is, is supported on balanced pairs. For the vector has ones at the indices in and zeros elsewhere; likewise for .
For , and : either is optimal for (3.4), or there exist , and such that for every ,
The result. Proposition 3.6 says that non-optimality of a feasible dual pair is always witnessed by a direction with entries in , determined by two index sets, which keeps the pair feasible for a positive step and strictly improves the objective. This is what makes dual ascent a finite combinatorial method rather than a generic linear-programming iteration: the search for an ascent direction reduces to a maximum-flow computation on the bipartite graph of balanced pairs. Combined with the step length of Proposition 3.5, it is the primal-dual method, which reduces to the Hungarian algorithm on assignment problems. Milestone 1 is the optimality certificate of complementary slackness, used throughout the book's chapter 3.
Formalizing it. These results are classical and proved in the book and in Bertsimas and Tsitsiklis; no machine-checked proof of them is known to exist. The mission produces a formal statement and proof of the optimality-or-ascent alternative for the discrete Kantorovich dual, together with the complementary-slackness certificate in the transport setting. Milestone 4 is a Hall-type statement (a supply–demand theorem on a bipartite graph) whose formal proof is reusable for other matching and transportation results.
Milestones 1–3 are short computations. The content of the goal is in milestone 4. The obvious argument is linear-programming duality: if is not optimal, some feasible direction improves the objective. But LP duality only produces an arbitrary real direction; the claim that a direction of the form suffices is a combinatorial statement. The book obtains as the labeled nodes of a maximal flow (Ford–Fulkerson) and argues through max-flow/min-cut; the flow bookkeeping printed on p. 417 is garbled, so the step from "no complementary coupling exists" to " for a set closed under balanced edges" has to be supplied carefully. Separately, connecting "not optimal" to "no complementary coupling exists" needs the converse direction of complementary slackness or strong duality for the transport problem.
Row and column indices are Fin n and Fin m (0-based); the primed column set is just Fin m. Cost matrices and couplings are Matrix (Fin n) (Fin m) ℝ; histograms and potentials are real functions on Fin n, Fin m; is Mathlib's stdSimplex ℝ (Fin n). Index sets are Finsets and is indicatorVec S. "Optimal for Problem (3.4)" is the predicate IsDualOptimal: feasible, and no feasible pair has a larger objective (no real infimum or supremum is used, so no junk value can enter). The book's "for a small enough " is stated as "for every ", which is equivalent because is convex and the objective is linear.
Standing assumptions, all from the book: is dual feasible (p. 415, "In what follows, is a feasible dual pair in "); are histograms in the simplex (used for the goal and milestone 4; without equal masses the dual is unbounded and optimality fails for every pair). Milestone 4 replaces the book's flow hypothesis "the throughput is strictly smaller than 1" by the equivalent flow-free statement "no coupling in is complementary to "; flows, capacities and the labeling algorithm appear in no statement.
The goal admits a trivializing formalization: allowing an arbitrary direction instead of turns Proposition 3.6 into plain non-optimality of a linear program. The statement here fixes the direction to exactly as the book does.
A complete development needs finite LP duality or complementary slackness for the transportation problem, and a max-flow/min-cut or Hall-type theorem on bipartite graphs with vertex capacities. Both are reusable well beyond this mission. Contributions welcome: proofs of the milestones, a self-contained proof of milestone 4 by induction or by a max-flow argument, and alternative proofs of the goal through LP duality plus a vertex argument.
Optimal transport compares two probability distributions by the least cost of moving one onto the other. When the ground cost is itself a distance, , the resulting quantity is the 1-Wasserstein distance , also called the earth mover's distance. It is the transport distance most used in practice for comparing histograms, images and point clouds, and it is the setting of Chapter 6 of G. Peyré and M. Cuturi, Computational Optimal Transport (FnT ML 2019).
For general costs the dual problem has two potentials coupled by the constraint . For a metric cost the dual collapses to a single potential constrained to be 1-Lipschitz. This is the Kantorovich–Rubinstein formula (Kantorovich and Rubinstein, 1958, cited by the book on p. 473), the basis of dual computations of : network-flow algorithms, the discrete linear programs of §6.1, and Wasserstein GANs, whose critics are 1-Lipschitz networks (Arjovsky, Chintala and Bottou, 2017). Proposition 6.1 of the book is the step that makes the collapse happen. It describes exactly which functions arise as -transforms when .
Let be a metric space and take with ground cost . For a real function on its -transform (the book's (5.1)) is
The infimum can be when the family is unbounded below. A function of the form is called -concave. The Lipschitz constant of is
and is 1-Lipschitz when , i.e. for all .
For the discrete companion, fix points and probability histograms (nonnegative entries summing to one). Let . The couplings are the nonnegative matrices with row sums and column sums . The optimal transport cost is with .
For every real function on :
with the minimum on the left and the maximum on the right both attained.
The mission also references the measure-theoretic Kantorovich–Rubinstein theorem already proved on the platform (WassersteinDRO.Duality.kantorovich_rubinstein). It is the book's (6.1) on a normed space.
The result. Proposition 6.1 identifies the -concave functions for a metric cost with the 1-Lipschitz functions, and shows that the -transform of such a function is . Starting from the dual problem in a single potential, the book then replaces by . This yields (6.1), . Consequently is a norm on measures of zero total mass. In the discrete case the dual is the finite program (6.2), whose constraints only involve pairs of support points. The min-cost-flow formulations and the Lipschitz-critic methods built on all start from this characterization.
Formalizing it. The proposition and (6.2) are classical, with complete proofs in the book. The mission produces machine-checked versions in a form that later chapters of this series can reuse. (6.2) is the discrete, linear-programming form of Kantorovich–Rubinstein duality, and the referenced platform theorem does not imply it without further work. To the best of this mission's search of the platform, neither Proposition 6.1 nor (6.2) has been formalized there. Villani's double-conjugate theorem for -concave is published, but it is a different statement.
Proposition 6.1 is short; its content is the characterization, not a long argument. One point needs care: an infimum over an arbitrary metric space can be . The statement "" therefore carries the information that the infimum is finite at every point. An encoding in which the infimum of an unbounded family silently becomes would make the forward direction false, or decide it by a default value. The discrete companion (6.2) is a genuine duality theorem. It needs both the attainment of the transport minimum and a strong-duality argument specialised to a metric cost matrix. Ordinary LP duality yields two potentials, and the reduction to a single 1-Lipschitz potential is exactly Proposition 6.1 on the finite set .
MetricSpace; no compactness, completeness or separability is assumed, since the book's §6.1 assumes only that is a distance.MongeKantorovichYao.cConjugate, applied to the cost . Its infimum is taken in EReal over all , so it never takes a default value. "" is an equality in EReal with real valued.LipschitzWith 1 f, which is equivalent to the book's supremum formula.Nonempty assumption: for empty every claim holds trivially, and for nonempty the infimum ranges over a nonempty family.Fin N. The two measures are written on common points , which need not be distinct, and is the discrete cost of (2.11).Contributions welcome: proofs of the milestones and goal, and a proof of (6.2), via finite LP duality and the milestones or via the referenced measure-theoretic theorem.
Distributionally robust optimization (DRO) chooses a decision that minimizes the expected loss under the worst distribution in an ambiguity set of plausible distributions, . It sits between stochastic optimization, which trusts a single distribution, and worst-case robust optimization, which trusts none. The inner supremum is a problem of moments, studied since Stieltjes and made computable by duality (Isii 1962; Shapiro 2001; Bertsimas and Popescu 2005). Existing tractable reformulations require the ambiguity set to be described by finitely many moments, a -divergence or a Wasserstein ball, and they usually require a structural property of the loss: affine or quadratic form, or a known Lipschitz constant.
Zhu, Jitkrittum, Diehl and Schölkopf (AISTATS 2021; arXiv:2006.06981) describe the ambiguity set through kernel mean embeddings: a distribution is represented by its mean in a reproducing kernel Hilbert space, and the ambiguity set is the set of distributions whose embedding lies in a convex set of that space. Moment sets, MMD balls, scenario polytopes and the whole space (worst-case RO) all arise for suitable kernels and sets . Their Generalized Duality Theorem (Theorem 3.1) turns the inner worst-case problem into a minimization over a function of the RKHS that majorizes the loss, with no assumption on the loss beyond upper semicontinuity.
Let be a compact metric space (in the paper, a compact ) with its Borel -algebra, and the set of Borel probability measures on . Let be a real Hilbert space and a continuous feature map; is then a continuous positive definite kernel, and an element acts on by the reproducing property (rkhsEval).
meanEmbedding).ambiguitySet).supportFun).For fixed (written ), the primal inner problem (11) and the dual inner problem (12) are
(primalValue, dualValue, with the constraint IsDualFeasible). Assumption 3.1 of the paper asks that each be proper (not identically ) and upper semicontinuous, that be closed and convex, and that .
The PDF prints no page numbers; every page cited in this mission is the PDF page of arXiv:2006.06981v3.
Under the hypotheses above, with ,
and consequently , the equality of the Kernel DRO problem (2) and its dual (4).
Lemma A.2 (complementarity (19)), Corollary 3.1.3 (the optimal majorant interpolates -a.e.), the support function of the RKHS norm ball (Table 1), and the weak-duality content of Corollary 3.1.1 for integral probability metrics.
The theorem replaces an optimization over probability measures by a semi-infinite program over , whose objective is explicit for the common choices of (Table 1). The majorant needs no Lipschitz constant and no parametric form of the loss, and the dual variable doubles as a witness function for the MMD. This is the basis of the paper's batch and stochastic functional gradient algorithms, and it places moment-based DRO, scenario optimization, MMD-ball DRO and worst-case RO in one framework.
The result is proved on paper; it has no machine-checked proof that we know of. Formalizing it builds the duality theory of moment problems with infinitely many moment constraints, on top of Mathlib's Hilbert spaces, Bochner integrals and the weak topology on probability measures. The formal statements also fix points the paper leaves loose: the infimum in place of the printed "min", the reading of the Slater condition, and the role of the continuity of the kernel.
Weak duality is a two-line computation. The work is strong duality. The paper's route separates the cone from in . A Hahn–Banach strict separation needs one set compact or the two at positive distance, and is neither obviously closed nor bounded. The step goes through only because is compact in the weak topology and is upper semicontinuous, which also gives primal attainment and the sign . The loss may take the value , so every expectation lives in . The infinite primal case also needs an argument of its own.
ProbabilityMeasure X with its topology of weak convergence; the paper's MMD topology agrees with it for a universal continuous kernel.X → EReal, upper semicontinuous, never , and not identically . Expectations use the published definition WassersteinDRO.Duality.erealExpectation, which for such losses is the usual .Reusable pieces: the kernel mean embedding and its continuity on ProbabilityMeasure X, compactness of RKHS ambiguity sets, and the upper semicontinuity of for upper semicontinuous (a portmanteau-type fact not yet in Mathlib). Proofs of any milestone are welcome. So are support-function computations for the other rows of Tables 1 and 3.
A learning algorithm trained on a finite sample generalizes when its empirical risk on that sample is close to its risk on fresh data. Classical guarantees come from uniform convergence over the hypothesis class (VC dimension, Rademacher complexity) or from algorithmic stability, such as uniform stability (Bousquet and Elisseeff, 2002) and on-average stability (Shalev-Shwartz et al., 2010). Both families look at the class or at the algorithm's worst-case sensitivity, not at how much the trained hypothesis actually depends on the data it was trained on.
Russo and Zou (arXiv:1511.05219, 2016) bounded the bias of adaptive data analysis by mutual information, and Xu and Raginsky (arXiv:1705.07809, NIPS 2017) turned this into a generalization bound for learning algorithms: the expected generalization error is at most , where is the mutual information between the training sample and the output hypothesis. This bound started the line of information-theoretic generalization bounds, later refined to individual-sample mutual information (Bu, Zou and Veeravalli, 2020), conditional mutual information (Steinke and Zakynthinou, 2020) and chaining variants (Asadi, Abbe and Verdú, 2018).
Timeline:
There is an instance space , a hypothesis space and a nonnegative loss , written ℓ : W → Z → ℝ in Lean. Data are drawn from an unknown probability measure on ; a dataset of size is an i.i.d. sample (sampleLaw μ n).
A learning algorithm is a Markov kernel (κ : Kernel (Fin n → Z) W): given the dataset, it outputs a random hypothesis . The pair has joint law (sampleLaw μ n ⊗ₘ κ), with marginals and .
The population risk and the empirical risk of a hypothesis are
(risk ℓ μ w, empRisk ℓ s w). The expected generalization error is
the expectation taken under (genError ℓ μ κ).
The mutual information of a pair with joint law is the relative entropy (mutualInfo). A real random variable is -subgaussian if for all .
If is -subgaussian under for every , then
The statement fixes no structure on (it may be uncountable) and no bound on the loss beyond subgaussianity.
The result. Theorem 1 makes generalization a property of the dependence between data and output rather than of the size of the hypothesis class. It applies to randomized algorithms on uncountable or infinite-dimensional hypothesis spaces, where uniform convergence gives nothing, and to unbounded subgaussian losses. Any mechanism that limits , such as noise injection, differential privacy, compression or relative-entropy regularization, inherits a generalization guarantee. A loss with values in is -subgaussian for every , so the theorem covers all bounded losses. The bound is also the template for the later refinements listed above, which share Lemma 1's decoupling argument.
Formalizing it. The result is proved on paper; no machine-checked proof is known. A formalization supplies a reusable statement of mutual information as a relative entropy of a joint law on general measurable spaces, a decoupling lemma for subgaussian functions, and the mixture argument for subgaussian families, all of which recur in the later literature. It also settles a point the paper leaves loose: the printed proof applies Lemma 1 to the uncentred empirical risk, which is not subgaussian in general; the milestones state the corrected step.
The two halves of the proof are short on paper, but each step that "follows" uses a fact the page does not state. The decoupling estimate needs to be finite, which holds only because finite relative entropy and exponential integrability under the product together force integrability under the joint law. The mixture step needs the moment-generating-function bound of each section to integrate over , which requires joint measurability and the centring of every section at its own mean: the uncentred empirical risk mixes laws with different means and is not subgaussian.
A natural first attempt applies Lemma 1 directly to as printed; it fails on the example with uniform on and independent of .
LearnStability.Characterization.Setting. This mission defines mutualInfo P := klDiv P (P.fst.prod P.snd) (values in ) and genError, the integral of the pointwise difference under sampleLaw μ n ⊗ₘ κ. Samples are Fin n → Z; the algorithm is a Markov kernel.HasSubgaussianMGF of the centred variable, whose parameter is the variance proxy: for the loss, for the empirical risk.genError and the mutual information of the algorithm's own joint law; a version through Lemma 1's abstract pair , through (Theorem 2, out of scope), or with truncated to a real number would not be this theorem.Measure.pi (Mathlib has HasSubgaussianMGF.sum_of_iIndepFun); mixtures of mean-zero subgaussian families under a product measure. These are reusable beyond this mission, and contributions of each are welcome.Data-driven decision making with side information ("prescriptive analytics") chooses a decision after observing a context , using a training set of past pairs . A common recipe estimates the conditional expected cost with a local learning method, such as Nadaraya–Watson kernel regression or nearest neighbours, and then minimizes the estimate over (Ban and Rudin 2019; Bertsimas and Kallus 2020). Such estimate-then-optimize decisions are known to be optimistically biased: the minimized estimate tends to understate the cost that the decision incurs on new data.
Bertsimas and Van Parys (arXiv:1711.09974v2) robustify these formulations against distributions near the empirical one, measured by a relative-entropy bootstrap distance. They show that this choice protects the decision against disappointment on resampled (bootstrap) data at an exponential rate. A robust formulation is only usable if it can be computed. This mission concerns the paper's computational result for the Nadaraya–Watson case: the robust budget, a supremum over a set of distributions, equals a two-variable convex dual program.
The training data have finitely many distinct points, the support . A distribution on is a vector with and ; their set is . Fix a context and a decision . Each support point carries a weight and a loss .
The Nadaraya–Watson estimate at (equation (19)) is the weighted average
The bootstrap distance (Definition 6, equation (27)) is the relative entropy
with and when puts mass on a point where vanishes. For a reference distribution and a radius , the bootstrap robust Nadaraya–Watson budget (equation (24) with and ) is
For the nearest-neighbours variant, nested neighbourhoods define a partial robust budget (equation (25)), with two extra linear constraints tying the mass of and to and .
For every and every radius ,
No hypothesis on is imposed. For both sides are , and for both equal .
The milestones follow the proof in Appendices B.3 and B.8:
The robust budget is a supremum over a -dimensional set of distributions, and the decision minimizes it over , which is a min–max problem. Lemma 2 replaces the inner supremum by an infimum over two scalars , so the robust prescription becomes a single minimization over . When is convex in , that minimization is an exponential-cone program. The paper's numerical section (§5) solves its robust formulations in exactly this form. Lemma 1 plays the same role for the nearest-neighbours formulation, with one dual program per neighbourhood.
The results are proved in the paper (Appendices B.3, B.7, B.8) by a Lagrangian computation. As far as we know, none of them has been machine-checked. A formalization adds three things. It handles reference distributions with zeros, which the page's computation divides by. It covers the full range of radii, including , where Slater's condition fails. And it records the corrected sign of the minimizing multiplier . The linear-objective special case without the ratio and with a strictly positive reference, , is already proved on the platform (Nilim–El Ghaoui, RobustMDP.EntropyInner.kl_ball_inner_problem_dual, with its multiplier elimination RobustMDP.EntropyInner.mu_elimination). Both are included as supporting references.
The obvious route is to apply the known entropic duality formula to the robust budget directly. That route fails because the objective is a ratio of two linear functions of , not a linear function. The ratio is quasi-linear, and Lagrangian duality does not apply to it as it stands. The paper first lifts it to a linear objective over the cone (Corollary 1). The entropy constraint then becomes the perspective , and duality is applied to this lifted program. A second difficulty is that the reference may vanish on part of the support. The ball then lives on a face of the simplex, and every step must respect the convention off the support of . Finally, strong duality needs a Slater point, which exists only for . The cases of the goal have to be handled separately.
The support is a finite type ι, and is stdSimplex ℝ ι. Covariates, responses and the distance of Definition 2 do not appear: only the weights w : ι → ℝ (positive) and the losses L z : ι → ℝ of a fixed decision enter. Losses are real-valued, a restriction of the paper's , while nonnegativity is not required. The conventions are the following.
EReal-valued: it is when the first argument charges a zero of the second, and .EReal: the supremum of the empty set is and the infimum of the empty set is .Several formalizations would make the statements trivial, and each is ruled out:
sSup/sInf, which return on empty or unbounded sets;A complete development needs the following:
The duality and conjugate lemmas are reusable for any KL-ball robust program. Contributions are welcome on each milestone, on bridges from the published RobustMDP.EntropyInner theorems to the setting here (they agree with when the reference is positive), and on the cases of the goal.
Many convex optimization problems combine a smooth loss with a term that is easy to handle through minimization but awkward to differentiate. A constraint can be represented by an indicator function that is zero on the feasible set and outside it. A norm penalty can be finite yet nonsmooth. The proximal gradient method handles such objectives by applying a gradient step to the smooth term and a proximal step to the other term. Parikh and Boyd present this method in §4.2 of Proximal Algorithms, after developing the proximal operator, its fixed points, and its connection to the subdifferential.
The mission concerns the method's optimality interpretation. A fixed point of the forward-backward update is a minimizer of the composite objective, for every positive step size. That is a statement about which points solve the problem. The separate claim that repeated updates converge requires further control of the gradient and the step size; the paper discusses that condition after the fixed-point identity on p. 151. This mission captures the fixed-point identity itself and the paper's stated convex-analytic results that support it.
Work in with the Euclidean inner product and norm . Let be convex and differentiable everywhere. Let be closed, proper and convex: its epigraph is nonempty, closed and convex. The effective domain consists of the points where is finite. The composite problem, equation (4.5), is to minimize over all . An indicator expresses the constraint within the same notation. These conventions are those of §1.1 and §4.2 of the monograph.
For a closed proper convex function , the proximal operator sends to the unique minimizer of . For , the operator equivalently minimizes . The paper assumes closed proper convexity whenever it uses a proximal operator, including one applied to . This assumption gives a unique proximal point at every input, even when is infinite outside a strict subset of the space.
The subdifferential is the set of vectors such that for every , as in (2.3). Unlike the gradient of , it can be empty or contain several vectors. The resolvent of the subdifferential with parameter is the inverse relation . Equation (3.4) says that this relation is the everywhere-defined, single-valued map . Both descriptions of the proximal point appear in the milestone list.
For any and , the target from §4.2.1, pp. 150–151, is
The quantifier covers every positive ; it is independent of any Lipschitz bound. The equation describes a fixed point of the forward-backward operator, which first evaluates and then applies the proximal operator of .
The milestones follow statements printed in the same monograph: existence and uniqueness of a proximal minimizer from (1.1)–(1.2); the subdifferential optimality condition for a proximal minimizer in §2.3; the fixed-point characterization of minimizers in §2.3; the full-domain, single-valued resolvent identity (3.4); and the condition for minimizing in §4.2.1. The resolvent milestone includes its domain and uniqueness claims because the paper states both, rather than only an equality of partially defined relations. These targets retain the authors' constants , and .
The equivalence identifies the solutions of a composite convex problem using an update rule that treats the smooth and nonsmooth terms differently. It applies when encodes constraints or a nonsmooth penalty and still characterizes the exact minimizers. It also says what a converged proximal gradient iteration must solve. The characterization by itself makes no claim that an iteration converges, a distinction made in the paper's discussion on p. 151. Parikh and Boyd, §4.2.1, give the fixed-point view of the algorithm in precisely this setting.
The formalization connects an existing machine-checked proximal-point definition from the Moreau 1965 series to a new Euclidean subdifferential defined by the supporting inequality (2.3). It leaves reusable statements about proximal optimality and resolvents alongside the composite result. A related published theorem, ProxNewton.Inexact.compGradStep_eq_zero_iff, characterizes minimizers through a composite-gradient step at unit step length under stronger smoothness assumptions and a different proximal representation. The present target preserves the monograph's arbitrary positive , its extended-real , and its particular proximal operator.
The two sides of the goal compare different minimization problems. The left side minimizes globally; the right side minimizes a quadratic centered at plus . Merely expanding the definition of the proximal operator does not make these objectives identical. The needed first-order conditions must also remain valid when is infinite outside its domain and its subdifferential is set-valued. In (3.4), an inverse relation is asserted to have a value at every point and only one value there; an equality that overlooks either property would be weaker than the paper's statement.
The Lean carrier is EuclideanSpace ℝ (Fin n) for arbitrary . Its norm and inner product are the paper's Euclidean ones. No positive-dimension hypothesis is imposed: the zero-dimensional case is a singleton space and does not invalidate these identities. Values of are in EReal; the imported MoreauProx.Decomposition.GammaZero records that never equals , is finite somewhere, has a convex epigraph, and is lower semicontinuous. For real-valued convex on all of , closedness and properness follow from finiteness and convexity. Differentiability is explicit so Mathlib's gradient f x represents the intended .
The imported MoreauProx.Decomposition.IsProx is a predicate saying that a point minimizes . Positive makes its minimizers those of the paper's (1.2), including at points where . Uniqueness is supplied by the referenced Moreau strict-minimum theorem. The local subdifferential follows (2.3): it is empty when its argument lies outside the effective domain, and it tests the supporting inequality over all . Outside the right side is , so those tests add no restriction. The composite minimization condition ranges over every and compares extended-real values.
The goal must relate these two genuinely different minimization problems through the gradient and convexity; defining the forward-backward operator to minimize would empty the theorem of its content. Contributions on extended-real subgradient calculus, the full-domain resolvent relation, and the composite optimality condition are welcome. The imported Moreau definitions and the local supporting-inequality subdifferential are reusable in further convex optimization developments.
This source PDF is the authors' Foundations and Trends formatted copy of the published monograph. Printed page numbers throughout this mission refer to that copy; its body begins on PDF page 5 at printed p. 123.
Learning with expert advice and online linear optimization over the probability simplex are the basic models behind boosting, multiplicative-weights methods for linear programming and zero-sum games, and adversarial bandit algorithms. The algorithm that solves them, under the names Weighted Majority, Hedge and Exponentiated Gradient (EG), keeps a probability vector over coordinates and multiplies each weight by after observing the loss vector .
The local-norm form is the one needed when loss vectors are large on coordinates of small weight, which is the situation of importance-weighted loss estimates in adversarial bandits.
Fix a dimension and a learning rate . In round the learner plays a vector in the probability simplex , then observes a loss vector and suffers the linear loss . Write .
Normalized EG starts from and updates
Its regret against a comparator after rounds is .
The analysis is phrased for general Online Mirror Descent (OMD): given a link function , predict . For a regularizer on a set (equal to off ), the Fenchel conjugate is , and the Bregman divergence of a differentiable is . Normalized EG is OMD with for the normalized entropy on , whose conjugate is and whose gradient is the softmax.
If for all and , then for every and every ,
The comparator is unquantified on the page; it ranges over the simplex , the competing set of the normalized-entropy regularizer. The bound fails for outside .
with equality for a minimizer of over . 2. (2.16)–(2.18) (p. 153). For , the gradient is the softmax, , and
The result. Since , Theorem 2.22 improves the standard bound of normalized EG. The improvement matters when a coordinate with tiny weight carries a huge loss: the local norm weights that loss by its probability. This is what gives the regret of Exp3-type bandit algorithms, whose loss estimates are of order . The theorem allows negative losses down to , so it also applies to gains and to centred or shifted losses.
Formalizing it. The theorem is proved in the survey; no machine-checked proof of it is known. The platform has a proved Hedge bound for non-negative losses compared with a single expert (Hazan, Introduction to Online Convex Optimization, Theorem 1.5). It does not imply Theorem 2.22: the latter allows negative losses, and its local-norm term is not invariant under shifting by a constant vector, so the shift that reduces signed losses to non-negative ones changes the bound. Lemma 2.20 is a general duality identity for OMD and is reusable for every OMD instance (Euclidean, -norm, unnormalized entropy).
The obvious argument for Hedge tracks the potential and bounds the one-step increase using for . With negative losses that inequality fails. The weaker form is valid only for , which is where the hypothesis comes from. The bound is also stated against the whole simplex, not against single experts, so the potential argument has to be combined with an entropy bound for a general comparator.
Fin d → ℝ, with 0 < d and 0 < η. Rounds are numbered from in Lean, so index is the paper's round and sums over rounds run over Finset.range T.UnderstandingML.wmWeights η z t (reference item UnderstandingML_Online), which is exactly the closed form of normalized EG for arbitrary real loss vectors; wmWeights η z 0 is the uniform vector .0 ≤ u i, ∑ i, u i = 1). A statement over all is false, and a statement over vertices only would be the weaker expert bound; both are ruled out.Fin d → ℝ carries the sup norm in Mathlib.Welcome contributions: proofs of the three milestones and of the goal, and general Mathlib-style lemmas on the gradient of log-sum-exp and on the Fenchel–Young inequality for conjugates defined as suprema over a set.
Stochastic gradient descent (SGD) is the default method for minimizing an expected loss when only noisy gradients are available, which is the situation of nearly every large-scale learning problem. When is strongly convex (for instance, any convex loss with an regularizer), information-theoretic lower bounds show that no method using noisy gradients can guarantee an error better than order , and some algorithms achieve this rate.
For plain SGD with step sizes and the standard averaged output, however, the classical analysis gives only . Rakhlin, Shamir and Sridharan (arXiv:1109.5647, ICML 2012) showed that the logarithm is real for full averaging on non-smooth problems, and that a minimal change to the output, averaging only the last fraction of the iterates, restores the optimal rate. This mission formalizes that positive result, the paper's main theorem.
Timeline of the relevant results:
Let be a closed convex set containing , and let . The function is -strongly convex on () if
A point is a minimizer of over .
Information about comes from a stochastic gradient oracle : at a query point , a sample is drawn and is returned. The oracle is unbiased in the sense that its mean is a subgradient of relative to : for all . Its second moment is bounded: at every .
Projected SGD with step sizes runs on an i.i.d. sample :
where is the Euclidean projection onto . For with an integer, the α-suffix average is
In Lean the iterates are UnderstandingML.sgdStrongIterates lam W g S, the oracle mean is oracleMean D g, the suffix average is suffixAverage lam W g S k with , and expectations are integrals against the product law UnderstandingML.iidLaw D T.
together with the finiteness of . The constants are the paper's.
Theorem 5 shows that the suboptimal factor of averaged SGD on non-smooth strongly convex problems is an artifact of which iterates are averaged, not of the gradient steps themselves: the same iterates, averaged over a constant fraction at the end, reach the minimax-optimal rate up to constants. This matches Hazan and Kale's guarantee with an unmodified algorithm, and the same paper's lower bound shows that full averaging cannot match it.
The result is proved in the paper; nothing in it is formalized. The platform holds the Understanding Machine Learning SGD model and its bound for full averaging (UnderstandingML.sgd_strongly_convex), but no rate for SGD on a non-smooth objective. The mission produces a machine-checked proof of Theorem 5 with its explicit constants and, along the way, of Lemma 1 (the mean-square convergence of the last iterate), which is reused by every analysis of SGD with step sizes , including the paper's smooth-case Theorems 1 and 2.
The obvious argument, the online-gradient-descent regret bound summed over all rounds and divided by , produces and so cannot avoid the logarithm. Discarding early iterates does not by itself help: the resulting bound depends on the distance of the iterate at which the suffix starts, at the scale , and the regret analysis says nothing about individual iterates of a non-smooth problem.
The formal difficulties are probabilistic. The iterates are random vectors built by composing a measurable oracle with a projection defined by choice; conditioning on the past to evaluate requires the product structure of the sample; and every expectation must be shown finite, including that of with not assumed measurable.
UnderstandingML.Vec d); the paper allows any Hilbert space.W closed and convex with 0 ∈ W (the paper's ; closedness makes well defined).StrongConvexOn W lam F with modulus , equivalent to the paper's (1) when subgradients relative to exist at every point, which the oracle provides.IsSubgradientOracleOn W F D g: for , is integrable and its mean is a subgradient of relative to . The oracle is jointly measurable and is a probability measure. The subgradient condition is not global: is only assumed convex on .sgdStrongIterates … t is the paper's ; the suffix average runs over indices , , passed as a natural number with , which encodes that and are integers.Real.log, the natural logarithm.Infrastructure a complete development needs: measurability of the projected iterates in the sample, the one-step conditional-expectation identity for the product law, and the integral comparison . The first two are reusable for the companion missions on the same paper and for any SGD analysis built on sgdStrongIterates. Proofs of any milestone, and of reusable lemmas about iidLaw and sgdStrongIterates, are welcome.
In pricing and supply-chain contracting, demand or valuations are random, and the profit functions that arise are unimodal only under a shape condition on the distribution. A firm facing demand at price maximizes revenue ; the first-order condition is , where is the generalized failure rate introduced by Lariviere and Porteus (2001). When is increasing, it crosses at most once and the optimal price is unique. The same condition makes the supplier's problem unimodal in the price-only newsvendor contract (Lariviere and Porteus, 2001) and appears throughout revenue management. The condition is useful but often hard to verify for a given distribution.
Lariviere (2006) gives three equivalent reformulations of the condition (Theorem 1), two sufficient conditions (Corollary 1), and uses them to show that every beta distribution has an increasing generalized failure rate. The parts of the equivalence had appeared separately: Keilson and Sumita (1982) showed the equivalence of parts 2 and 3, and Ma (1999) linked parts 3 and 4.
Let be a nonnegative random variable with distribution function and survival function . Assume has a density , and let the support of be with . The failure rate of is , and its generalized failure rate is
is IFR if is weakly increasing on , and IGFR if is weakly increasing on that set. Every IFR variable is IGFR; many variables with decreasing failure rate are IGFR as well.
Write , with distribution , density , survival and failure rate . Two nonnegative variables with failure rates are ordered in the hazard rate order, , if for all . A function is totally positive of order 2 (TP₂) if
A function is log-concave if its logarithm is concave.
In the Lean development these are survival, failureRate, genFailureRate, IsIFR, IsIGFR, HazardRateLE and IsTP2On in the namespace LariviereIGFR.Char, and log-concavity is the platform predicate ConvexOptimization.LogConcaveOn.
The following are equivalent:
Theorem 1 converts the IGFR condition into conditions with an established theory. Through part 2, every closure and comparison property of IFR distributions transfers to IGFR distributions under the logarithm: the lognormal distribution is IGFR because its logarithm is normal, and inherits IGFR from . Part 3 has a direct operational reading: as a market scales up, a supplier selling to a newsvendor sells more and a service provider charges more. Part 4 places IGFR in the theory of total positivity. Corollary 1 gives density-level tests that need no closed form for , which is what makes the beta family tractable.
The results are proved in the paper; none of them is formalized. A machine-checked development would supply reusable facts about image laws under and scaling with explicit densities, the failure-rate form of the hazard rate order, and the classical Barlow–Proschan characterization of IFR distributions by total positivity, which is used well beyond this paper.
Parts 1 ⇔ 2 and 1 ⇔ 3 are computations once the laws of and and their densities are identified, but that identification is a change of variables for measures, together with a check that the transported density is again the derivative of the distribution function on the support. The substance is the Barlow–Proschan step, part 2 ⇔ 4. Monotonicity of is a pointwise statement about a density, while TP₂ of is an inequality between products of tail probabilities; the bridge is log-concavity of on the support, and its extension across the endpoints of the support, where equals on one side and on the other. A naive reading that differentiates everywhere fails at those endpoints and wherever the density is changed on a null set.
Real.log, and is the image under ; both maps are measurable, so the images are genuine probability laws. The junk value is harmless because has no atom at .IsRegDensity μ φ: , has density , at every point of , and where . The derived densities and are proved to be regular as well (milestones 1 and 4).Contributions welcome: the change-of-variables lemmas for Measure.map with explicit densities, the identification of as an open interval, and the Barlow–Proschan equivalence, which is reusable for any IFR result.
Little's Law, , relates three averages of a queuing system: the average number of items in the system , the average arrival rate , and the average time an item spends in the system . It is used throughout operations management and computer architecture, where two of the three quantities are measured and the third is inferred.
The classical theorems (Little 1961; the sample-path proofs of Stidham 1974 and later work) are stated over the whole time axis and require the three averages to exist as limits. Every observation in practice is made over a finite period: a supermarket over one business day, a wine cellar over one year. In his fiftieth-anniversary survey (Little 2011), Little argues that for such data the right statement is a finite-window one, and proves in §2 that over any window the relation holds exactly, with no limits, no stationarity and no assumption on queue discipline or service.
Timeline:
The object is one deterministic sample path observed over a window with . There are finitely many items . Item arrives at time and leaves at time , and is in the system at time exactly when . An item still present at is given any departure time .
KellyStochasticNetworks.occupancy).Then , , and is the average of over the counted items: the "average incremental age" added to the wines of a cellar during the year.
for every sample path with and every , with items allowed at both ends of the window.
The result. Theorem LL.2 makes Little's Law a measurement identity: for any recorded day, month or year of operation, the three averages computed from the data satisfy exactly, whether or not the system was ever empty (Corollary (1)) and whether or not there is any service operation (Corollary (2)). This is what licenses inferring an unmeasured parameter from two measured ones on finite data, the use Little describes in §4 for supermarkets, factories and computer systems. Corollary (3) extends the identity to market segments and to their aggregate, with the aggregate wait an arrival-weighted average of the class waits.
Formalizing it. The infinite-horizon sample-path law is already proved on the platform (queueing_general_littles_law, by wenxinzhang), but its sample paths have no item present at time and its conclusion is a statement about limits. Only the empty-boundary area identity (milestone 1, from Kelly and Yudovina's Stochastic Networks) exists for finite windows. LL.1 as an identity of the three averages, LL.2, the truncated area identity and Corollary (3) are not formalized anywhere we know of. The mission produces finite-window definitions of and of the time in window that later queueing missions can reuse.
The algebra of the paper's proof is one line once is known. The content is that identity, which is an exchange of an integral over time with a sum over items in which every item's contribution is clipped to the window. An item present at contributes only its time after ; an item present at only its time before ; items that leave before or arrive after contribute nothing and must not be counted in . Getting the boundary conventions right, so that each counted item contributes exactly the length of , is where an informal argument is easiest to get wrong. The naive reading " is divided by the number of items" makes the theorem a tautology and is ruled out below.
Fin M with real epochs a d : Fin M → ℝ. All of , , , , and are defined from the items; none is a free variable.KellyStochasticNetworks.occupancy. An item arriving exactly at is counted in once, as an arrival in ; the paper's remark then holds except for an item that arrives and leaves at the same instant .Contributions welcome: proofs of the milestones and goal, and reusable lemmas computing of indicator functions of intervals.
Volume-preserving box transport supplies geometric operations for a finite computation. The selected goal assembles these into a force and a fixed particle observer. The pinned manuscript supplies the research context.
A finite machine and input determine effective velocity and force coefficients. The force depends affinely on positive viscosity, and after time one the velocity is periodic and depends only on the machine.
The selected goal is OAI.BalancedTransport.balanced_three_stack_realization. Its central assertion is
The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.
The balanced three-stack realization is the main goal; balanced box routing is a separate supporting reference. The exact conclusion permits spatially constant pressure in competing solutions and explicitly states its comparison class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Uniform effectiveness, compact support, periodic behavior and uniqueness must all coexist with exact halting detection.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Metric absorption asks whether adjoining a null-sequence component changes a space up to controlled distances. Linear absorption imposes a different requirement. The pinned manuscript supplies the research context.
The space Z is a separable real Banach space. The product Z×c0 uses the product metric, and equivalent metrics are compared through positive bi-Lipschitz constants.
The selected goal is OAI.C0Absorption.main_result. Its central assertion is
The theorem states that there exists a real normed space Z, in a fixed universe, with the following properties, where C₀ denotes the real Banach space of sequences ℝ-valued on ℕ that tend to zero at infinity, and a map f between metric spaces is bi-Lipschitz if there are constants 0<c≤C with c·d(x,y) ≤ d(f x,f y) ≤ C·d(x,y) for all x,y. First, Z is complete and separable. Second, Z contains no linear copy of C₀: every continuous linear map T from C₀ to Z fails to satisfy ‖Tx‖ ≥ c‖x‖ for all x for any c>0. Third, there is a surjective bi-Lipschitz map F from the product metric space Z × C₀ onto Z. Fourth, there is a bi-Lipschitz map from C₀ into Z. Fifth, Z is metrically universal for separable metric spaces: every separable metric space M, in the base universe, admits a bi-Lipschitz map into Z. Sixth, Z × C₀ is not linearly homeomorphic to Z, that is, there is no continuous linear equivalence, with continuous inverse, between Z × C₀ and Z.
The target also includes a bi-Lipschitz embedding of c0, universality for base-universe separable metric spaces, and failure of linear homeomorphism between the product and Z. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The metric universality and absorption maps must not produce a bounded-below linear embedding of c0.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Parallel repetition is useful for amplifying errors in nonlocal games, but a joint entangled strategy can correlate outcomes across repetitions. Independence of the sampled questions does not imply independence of wins. The pinned manuscript supplies the research context.
A finite two-player game has a probability distribution on question pairs and a Boolean acceptance predicate. Its entangled value is a supremum over finite-dimensional states and local positive-operator measurements.
The selected goal is OAI.ThresholdParallelRepetition.threshold_parallel_repetition. Its central assertion is
The theorem states that there is a universal constant κ₀>0 such that the following holds for every two-player nonlocal game G with question sets of sizes x+1 and y+1 and answer sets of sizes a+1 and b+1, given by a probability distribution on question pairs and a Boolean acceptance predicate on questions and answers, whose entangled value is strictly less than 1. Here the entangled value is the supremum of the winning probability over finite-dimensional entangled strategies, which consist of a unit state on a bipartite space, positive semidefinite measurement operators for Alice and Bob summing to the identity for each question, with answer probabilities given by the Born rule. For every δ with 0<δ<1−entangledValue(G) and every number of repetitions k≥1, consider k-fold parallel repetition, where k independent question pairs are drawn from G's distribution and the players answer all coordinates at once. The threshold probability of a repeated entangled strategy S is the probability that the number of coordinates won is at least ⌈(entangledValue(G)+δ)k⌉. The theorem asserts that this probability is at most exp(−κ₀ δ¹³ k /(1+ln((a+1)(b+1)))) for every repeated strategy S, and that the threshold value, defined as the supremum of the threshold probability over all repeated strategies, satisfies the same bound. The statement is admitted without proof in the source.
The selected published Lean exponent is δ^13, not the manuscript abstract's δ^5 or its distribution-dependent cubic rate. Both every-strategy and supremum conclusions are included. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The estimate must hold uniformly over finite dimensions and collective strategies. Taking the supremum cannot assume that an optimal strategy exists.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.A divergent reciprocal sum is a sparse largeness condition on integers. The mission asks whether it still forces additive structure of every finite length. The source manuscript presents the surrounding research claim.
For A⊆ℕ, reciprocalTerm(A,n) is 1/n when n∈A and zero otherwise, using Lean’s total real inverse at n=0. A nonconstant arithmetic progression has terms a+i·d with positive integer d.
Prove
The starting term a is a natural number and is not separately required positive; the step d is strictly positive.
The selected formal target is OAI.Erdos3.manuscriptReciprocalProgressionTheorem.
The selected endpoint is the reciprocal-sum progression theorem. The manuscript’s quantitative bounds for progression-free subsets motivate it but are not supplied as separate published targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Positive density arguments alone do not cover all sets with divergent reciprocal sums. The hypothesis permits sets whose density tends to zero.
The formal hypothesis is ¬Summable of a real sequence and ranges over all natural-number sets. All natural lengths k are included, including the degenerate zero and one cases. The n=0 summand equals zero and does not affect divergence. No quantitative constants are asserted here.
adc7f1241b42. Goal source.How well can a graph be drawn inside a Banach space without stretching some distances much more than others? The distortion of the best such drawing measures the mismatch between the graph's metric and the geometry of the space. Diamond graphs are a standard test family: each edge is repeatedly replaced by parallel two-edge paths, so the graph contains many "midpoints" between the same two endpoints at every scale. For binary diamonds, bounded distortion in a space is tied to the failure of super-reflexivity (Johnson–Schechtman 2009). For countably branching diamonds, where each edge is replaced by infinitely many paths, the relevant property is asymptotic midpoint uniform convexity (AMUC): an equivalent AMUC norm prevents uniform embeddings (Baudier et al. 2017).
This mission asks for an explicit, quantitative lower bound on the distortion of countably branching diamonds in two specific James-type tree spaces, deduced from a midpoint "lens" estimate for those spaces.
The source of this mission is an OpenAI preprint dated September 27, 2026; its lens input comes from the companion OpenAI preprint Midpoint lenses in segment spaces of the same date.
Diamonds. The normalized diamond is one edge of length . replaces every edge of by countably many internally disjoint two-edge paths with the same endpoints, each new edge having half the length of its parent. Let be the shortest-path metric. A map has distortion at most if for some scale
Tree spaces. Let (one rooted tree of each finite height, prefix order inside each tree). A segment is the set of vertices between two comparable nodes. For a finitely supported array ,
is the completion and with the dual norm. On (root included) the same formula defines , and is the closed span of the coordinate functionals.
For every and every distortion- embedding of into ,
The Lean statement OAI.DiamondDistortion.headline_all_pairs is the conjunction of the two cases. It is open on the platform.
The bound shows that the countably branching diamonds do not embed with uniformly bounded distortion into either space, with an explicit square-root growth rate. Combined with the companion results that neither space admits an equivalent asymptotically uniformly convex norm, and that the forest dual is reflexive, it shows that the diamond obstruction can hold in reflexive spaces without AUC renormability, so the unconditional-structure hypotheses in the known converses are doing real work. The constant is obtained by retaining the full quadratic budget of the lens inequality. The paper also gives direct energy proofs (Theorem 5.1, Propositions 4.2–4.3) with weaker constants, and general transfer theorems (Section 7) from lens inequalities to distortion bounds.
The theorem is proved in the OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formalization would certify both the metric deduction and, through its input, the tree-space lens estimate.
The input lens inequality bounds only the tail of a displacement outside a finite head. Turning it into a loss of squared edge stretch at every replacement level requires selecting, among infinitely many middle vertices, two whose head projections nearly coincide, so that their half-difference is a tail vector that still lies in the lens. Doing this simultaneously along a descending chain of edges, with the head growing at each step, and summing the losses without wasting the quadratic budget is where the constant is decided. A binary diamond argument does not transfer, because finitely many midpoints give no near-coincident projections.
Diamond.Vertex k and Diamond.Edge k are defined by recursion on the stage, each parent edge receiving new vertices indexed by ; Diamond.graph k is the undirected replacement graph and Diamond.distance k u v is SimpleGraph.dist divided by . Since distortion is scale invariant, the normalization does not affect the statement.ForestDual is the full continuous dual of the completion of the finite-height forest James space; InfinitePredual is the norm-closed span of coordinate functionals in the dual of the infinite-tree space, with the subspace norm.A complete development needs the James segment norm and its dual, coordinate projections onto finite ancestral sets, the companion lens estimate, and graph distances on the countably branching diamonds. This infrastructure is shared with the other missions of this family. Formal proofs of Theorem 7.2 (lens-to-distortion transfer) and Theorem 7.12 (AMUC prevents uniform embeddings) are welcome as reusable components.
Bernoulli percolation is the simplest model of a random medium: each edge (or each vertex) of a lattice is independently kept open with probability , and one studies the connected components (clusters) of open edges or vertices. As increases, an infinite cluster appears at a critical parameter . Whether an infinite cluster already exists at decides whether the phase transition is continuous, and it is the basic question about critical behaviour. On the nearest-neighbour cubic lattice it has been a central open problem of probability and statistical physics since the 1980s; the dimensions where it was settled were and sufficiently high .
The source of this mission is an OpenAI preprint dated September 24, 2026, giving a self-contained argument for both bond and site percolation on .
Vertices are ; and are nearest neighbours if for a coordinate vector .
Let be the product law, , and
defined separately for bonds () and sites ().
The Lean statement OAI.CriticalZ3.critical_no_infinite is the conjunction of these two almost-sure statements. It is open on the platform.
Theorem 1.1 gives continuity of the percolation probability at the transition: as (the paper derives this on p. 1 from the theorem and finite-box approximation). It is the three-dimensional case of the Benjamini–Schramm criticality question and of the classical problem, which had resisted both planar methods (which rely on duality unavailable in three dimensions) and the lace expansion (which needs high dimension). The site statement is not a formal consequence of the bond statement: site bits become hyperedges with an endpoint convention that must be preserved.
The result is proved in an OpenAI preprint, which has not been peer reviewed. A public announcement reports a Lean formalization of the bond case on ; no machine-checked proof of this exact statement exists on the platform, and the site case is not covered by that announcement's formalization. A formal proof here would certify both models in one development.
The natural route is renormalization: show that if an infinite cluster exists at , then good finite-box events have high probability, persist at some , and can be glued into an infinite cluster at . The gluing step is where the obvious argument fails. Positive correlation (Harris–FKG) controls the probability that two increasing events both occur, but here one needs the probability of reaching a relay set and then a target, conditioned on an explored region; without a comparison inequality of the form the losses compound. Slab results do not suffice: extinction at each slab threshold plus convergence of thresholds does not give extinction on .
Vertex := Fin 3 → ℤ; bonds are pairs (x, i) representing the edge from x to step x i = x + e_i, so each edge appears once.bondLaw p and siteLaw p are Measure.infinitePi of bernoulliMeasure true false, giving mass to "open"; parameter clamps into .Relation.ReflTransGen of the open-adjacency relation; siteCluster ω x is empty unless ω x = true, matching the endpoint convention.bondCritical and siteCritical are sInf of . The statement does not assume ; it is a known fact for , and a solver may need to prove it to rule out the empty-set convention.A complete development needs product Bernoulli measures on countable index sets, monotone coupling, increasing events and Harris–FKG, the finite hyperedge comparison inequality, and a planar boundary-counting lemma. The percolation infrastructure is reusable for the quasi-transitive generalization in the same family. Contributions formalizing Proposition 2.1 (joint connection comparison), Corollary 2.3 (failure comparison), Lemma 4.1 (extension estimate) and Lemma 5.1 (neighbouring-box relay) are welcome.
The irreducible complex representations of the symmetric group are the Specht modules , indexed by partitions . How a tensor product (with diagonal action) decomposes is recorded by the Kronecker coefficients
for which no positive combinatorial rule is known; even deciding positivity is hard, and the question is studied in algebraic combinatorics and geometric complexity theory. In 2012 Jan Saxl proposed that the staircase , a partition of , has a tensor square containing every irreducible representation of .
A partition is a Mathlib YoungDiagram. The Lean development builds concretely: for a tableau (a bijection between and the cells), the polytabloid is the signed sum over the column group of of the permuted indicator of the row word of , inside the space of functions on words ; Specht t is the -span of the -orbit of . The coefficient kronecker a b t is the complex dimension of the space of -intertwining maps from spechtRep t into spechtRep a ⊗ spechtRep b. The staircase staircase m is the diagram of cells with , i.e. .
For every integer and every partition ,
equivalently contains every irreducible representation of . This is Theorem 1.1 of the source, formalized as SaxlConjecture (positivity of kronecker for every Young diagram with as many cells as staircase m). The goal is published on the platform with status Open.
The result itself. Saxl's conjecture is the best-known instance of the tensor-square covering problem for symmetric groups. The source proves a stronger cyclic form (its Theorem 3.1): every already occurs in the submodule generated by one explicit tensor of row and column polytabloids. A companion preprint uses this cyclic form to construct, for every , an irreducible representation of whose tensor square contains every irreducible (the tensor square conjecture of Pak–Panova–Vallejo).
Formalizing it. The Lean statement is the classical, non-cyclic conclusion, the form in which the conjecture is usually quoted. A formal proof would require Specht-module theory (irreducibility, Young's rule, branching, induced modules), none of which is presently in Mathlib in usable form; that layer would be reusable across representation theory of .
Positivity of a Kronecker coefficient cannot be read off from characters in general: character sums cancel, and the families handled earlier (hooks, two rows, double and triple hooks, dominance-comparable shapes, 2-height-zero shapes) each relied on a special structure. Asymptotic statements (almost all ) or higher powers (cube, fourth power) leave exceptional constituents. An induction on must retain an explicit vector at every step, because knowing that a constituent appears somewhere in a smaller square does not propagate through the projections needed to grow the staircase.
staircase m has cells , with cells; canonicalTableau fixes one enumeration of cells (any enumeration gives an isomorphic module). The target diagram ranges over all YoungDiagrams of the same cardinality.kronecker is Module.finrank ℂ of Representation.IntertwiningMap, the genuine multiplicity; positivity means a nonzero equivariant map exists.