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?
Differential privacy (Dwork, McSherry, Nissim and Smith, 2006) requires a randomized algorithm's output distribution to change little when one individual's record is changed. PAC learning asks an algorithm to output, from i.i.d. labeled examples, a hypothesis whose error is small with high probability. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith (arXiv:0803.0924v3; SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090) asked which concept classes can be learned under both requirements at once. All theorem, page and display numbers in this mission are those of the arXiv v3.
Their generic learner (§3, the subject of mission I of this series) learns every finite class privately with a polynomial number of examples, but its running time is exponential in the representation size for classes such as parity. Parity functions are the standard example of a class that is learnable efficiently by linear algebra and not learnable with statistical queries (Kearns, 1998; Blum et al., 1994), a model that was then the main known source of efficient private learners (Blum, Dwork, McSherry and Nissim, 2005). Section 4 of the paper gives an efficient private PAC learner for parity. The result separates efficient private learning from statistical-query learning, and the local (randomized-response) model from the centralized one (missions III–V).
For and , the parity function is the inner product of and modulo 2; PARITY is . A database is with . Two databases are neighbors if they differ in exactly one entry. A randomized algorithm , identified with the law of its output, is -differentially private if for all neighbors and all sets of outputs. is the Laplace distribution with density .
For , is the solution space of the linear system . The basic learner outputs with probability ; otherwise it puts each into independently with probability and outputs for uniform in , or if .
The amplified learner sets , , , , for constants . If it returns "insufficient samples". Otherwise it runs on disjoint blocks of examples, obtaining . It perturbs each training error on the next examples by independent noise and outputs the with the least perturbed error.
For a distribution on and a target , the error of is , and probabilities of the learner's success are over i.i.d., , and the learner's coins.
There are constants such that for all , , : is -differentially private on databases of every size, and
for every distribution and every target . When the bound is the paper's . The constants are fixed before all other parameters. The goal is literally the conjunction of Lemma 4.5 and Lemma 4.6.
The theorem shows that the restriction to private algorithms does not separate efficient learnability from statistical-query learnability: parity is efficiently and privately PAC learnable, yet not SQ learnable. Its sample complexity exceeds the non-private by a factor (remark, p. 18). The private amplification step (private model selection with Laplace-perturbed test errors) is a general technique that converts any private learner with constant success probability into a private PAC learner.
The result is proved in the paper; none of it is machine-checked as far as we know. The mission produces a formal library of the basic privacy calculus (Laplace mechanism, composition and post-processing), the solution-space estimate behind the privacy of , and the analysis of both learners. Formalizing it also repairs the paper's statement: the printed sample bound fails when is large compared with (see the scope section), and the base of the logarithm defining is misprinted.
The obvious private learner, "solve the linear system on all examples and output a random solution", is not private. One changed example can make the system inconsistent and turn every hypothesis output into failure, so the output law on neighboring databases differs by an unbounded factor. Two devices restore privacy: subsampling each example with probability , and failing with probability unconditionally. The privacy proof then needs a quantitative fact about : adding one consistent equation at most halves the solution space. The proof must also handle databases labeled by no parity at all, where solution spaces are empty.
Utility has its own difficulty. The amplified learner selects among candidates through noisy test errors, so three failure events (no good candidate, unrepresentative test set, large Laplace noise) must be bounded together. The sizes , , must also be shown to fit inside the claimed sample bound.
ZMod 2; is Fin d → ZMod 2; is dotProduct r x. Databases are Fin n → (Fin d → ZMod 2) × ZMod 2, with 0-based indices.Option (Fin d → ZMod 2) (none = ). 's output is "insufficient samples", , or a hypothesis . Every set of outputs is measurable, and differential privacy is required for all measurable sets.PMF on the finite set . The probability over the examples is a finite sum weighted by , and has error 1.ComputationalLearning.chernoff_bounds (Theorem A.1) and ComputationalLearning.occam_cardinality (Occam's razor), both proved on the platform.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.A self-similar measure on the line is the natural probability measure on the attractor of finitely many contracting similarities , chosen with probabilities . Self-similar measures are the basic test case for fractal dimension theory; Bernoulli convolutions, the laws of , are the classical example. When the pieces are well separated, the dimension is given by the entropy-to-Lyapunov formula . When they overlap, dimension can drop, and the question is exactly how much. If two compositions of the same length coincide as maps (an exact overlap), information is genuinely lost; the entropy-rate dimension conjecture, formulated in Varjú's survey, predicts that this is the only mechanism: the dimension equals , where is the entropy rate of the random walk on composed maps.
This mission asks for a formal proof of that formula, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let be a finite nonempty alphabet and with , ; different symbols may give the same map, and ratios may be negative and unequal. Let be a probability vector with all . The self-similar measure is the Borel probability measure with
For a word let , and let be the random affine map when the letters are independent with law . With logarithms in base ,
where is Shannon entropy of the distribution of the map (coinciding words are merged). The lower Hausdorff dimension of is . The system has no exact overlaps if distinct words of the same length give distinct maps.
If there are no exact overlaps, the attractor is compact and nonempty, the equation has a unique solution , and .
If for all and there are no exact overlaps, then .
For every such family and every strictly positive probability vector ,
No separation assumption is made; exact overlaps and repeated generators are allowed.
The result itself. It removes every arithmetic and separation hypothesis from the dimension theory of self-similar measures on the line: the only way dimension can drop below is through exact overlaps, and then the drop is exactly measured by the map entropy. Without exact overlaps it gives the classical formula (Corollary 6.2, p. 19), and hence the dimension of every self-similar set without exact overlaps (Corollary 6.3), which is the exact-overlaps conjecture for sets. It asserts nothing about absolute continuity.
Formalizing it. Hausdorff dimension and self-similar measures exist only partially in Mathlib, and the proof needs a quantitative entropy calculus for finite laws at multiple scales. A formal proof would certify the general theorem together with the consequences that previously required separate arithmetic hypotheses. The only external input is the Feng–Hu exact-dimensionality theorem.
Hochman's method yields the formula under exponential separation of cylinders, but Baker and Bárány–Käenmäki showed that without exact overlaps cylinders can still come superexponentially close, so no lower bound on the separation is available, and exact overlaps add further collisions. The proof must therefore detect entropy hidden at arbitrarily fine scales with no control on the smallest positive distance. The preprint does this with a finite-law pair estimate independent of minimal separation (Lemma 3.2, p. 9), conditioning on block types to recover the map-entropy rate when addresses collide (Lemma 4.1, p. 13), and disjoint windows of entropy gain whose depths are chosen adaptively (Section 5).
System ι over a nonempty Fintype ι carries ratio, offset, weight with , , . SelfSimilar S μ is the equation for a probability measure on .wordAffine composes maps as and records (slope, translation); mapMass merges words with equal complete maps; walkEntropy n is base-2 Shannon entropy of ; entropyRate is the sInf over of ; lyapunov is base-2.lowerHausdorffDimension μ is an iInf in ℝ≥0∞ of dimH E over measurable with ; the goal compares it to ENNReal.ofReal (min 1 (h/χ)).NoExactOverlaps is injectivity of wordAffine on all words; words of different lengths always differ in slope modulus, so this matches the same-length condition of the source. The homogeneous milestone allows a single map, a degenerate case where both sides are .codingPoint and word functions, equivalent to the definitions above.A linear projection can concentrate a measure even when the measure has no atoms; how much depends on how much mass sits near the affine subspaces that the projection collapses. Quantitative versions of this principle go back to the potential-theoretic projection method of Kaufman and Mattila, which relates ball-growth bounds to the behaviour of projections. This preprint proves explicit, dimension-dependent versions for random exact projections and applies them to a learning question: how many noiseless Gaussian measurements does a learner with bits of memory need to recover a unit vector to angular accuracy ?
The answer proved here is that bits force measurements, matching the real-valued randomized Kaczmarz scale, and more generally for every .
Let be uniform probability on . A finite measure on satisfies an all-ball mass bound with constants if for every ball. For an orthonormal -frame , is the image measure on and its density. The Riesz functional of is .
In the finite-state regression experiment, the signal ; at each step a row arrives with its exact label . A learner keeps one of states, may use arbitrary measurable randomized transitions of the current state and pair, stops by a deterministic horizon , and outputs a unit vector from its terminal state, stopping index and fresh randomness. Success means .
In Lean (OAI.ProjectionMoments, OAI.NoiselessRegression), learners are FiniteKernelLearner d M T (Markov-kernel transitions on completed observations, states Fin (2^M)), mixed over a seed space Ξ with probability ρ; seededSuccess is uniform-prior success; AllBallMass ν K β, coordinateDensity, frameLaw, capMeasure, rieszPotential encode the geometric objects.
OAI.ProjectionMoments.mainA conjunction of the paper's results, including:
also under an every-signal guarantee.
The result. The projection moment estimates are general statements about finite measures with ball-growth control and apply beyond learning. In the learning application they give three proofs, with different stopping and accuracy costs, that bits cannot beat the sample scale for exact Gaussian measurements, plus an explicit trade-off for all .
Formalizing it. The results are in an unrefereed preprint; there is no machine-checked proof. The conjunct FixedQuadraticMemory coincides with part of the goal of the companion mission on Memory and precision in noiseless Gaussian regression, so progress here is shared.
Integrated density norms do not determine density values on a matrix-dependent graph, so pointwise statements need an explicitly chosen density version. The high moments of projected densities require controlling collisions of independent points under projection, which leads to inverse affine heights whose integrability must be extracted from the ball-growth hypothesis at all scales. In the learning application, conditioning on an exact label produces a singular posterior, so arguments that track a posterior density fail.
EuclideanSpace ℝ (Fin d); frames are orthonormal families Fin k → E drawn by frameLaw; densities are ℝ≥0∞-valued with explicit measurable versions.d/4, d/8, d/16); block counts appear as (T+k-1)/k.FiniteKernelLearner with CompletedRules almost surely in the seed; success probabilities are ℝ≥0∞.The goal has no trivial reading: each conjunct quantifies over all measures or learners satisfying the stated hypotheses, and the hypotheses are satisfiable.
Needed infrastructure: Stiefel and Haar measures, Gaussian polar decomposition of matrices, Gram–Schmidt Jacobians, spherical caps, Riesz potentials. Contributions proving individual conjuncts (for example Theorem 3.3) are welcome.
Draw independent fair bits , compute a one-bit summary , and send the bits through independent binary symmetric channels with crossover probability , producing . Which summary tells the receiver the most about ? Kumar and Courtade conjectured that a single coordinate, , is optimal: bits for every Boolean , in every dimension and at every noise level (ISIT 2013; IEEE Trans. Inf. Theory 2014). The Courtade–Kumar (most informative Boolean function) conjecture is a basic question about how noise destroys information on the discrete cube, connecting information theory with Boolean Fourier analysis and hypercontractivity.
This mission asks for a formal proof of a sharp contraction theorem for arbitrary randomized binary summaries, whose Boolean case is the Courtade–Kumar conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.
Let with uniform measure; information is in nats unless stated. For put
with ; is the increasing branch . A soft channel is , the conditional mean of an auxiliary sign given ; its information is . For let with independent signs , and let , so . For an interior field with , the production is with ; the rate is defined by ; (zero for ); .
For , and every Boolean on ,
with equality for every coordinate and its complement.
The goal OAI.SoftChannel204.fullMain is the conjunction of:
with equality for every soft coordinate , ; and for the joint law of . 2. Corollary 1.2. For Boolean with and : , strictly below when and ; coordinates and their negations attain ; and the bits conversion . 3. Theorem 1.3. For every interior : .
The result itself. It settles the Courtade–Kumar conjecture and strengthens it in two directions: to randomized summaries at fixed initial information, and to a bias-dependent bound that is strictly better for nonconstant biased outputs. Theorem 1.3 is a mean-dependent entropy-production inequality, stronger than the scalar rate needed for Theorem 1.1. Several independent proofs of the Boolean conjecture were announced in the same period; the preprint compares its production profile with that of Chen et al. in Section 8.
Formalizing it. All objects are finite sums over , so the statements are elementary to state in Lean. The proof requires an explicit three-point optimizer for a joining problem, convexity facts about and (Lemmas 2.2–2.4, pp. 5–6), dimension induction and integration along the noise semigroup. A formal proof would give a checked solution of a conjecture with several competing announced proofs, some computer-assisted.
The local-to-global method of Chen, Gohari and Nair needs a local inequality to pass from the two halves of the cube to the whole. The natural information-only profile fails the corresponding local comparison for some coupled pair laws, so the induction must carry the mean as well. The preprint uses the maximum of two profiles, and ; it must solve the minimization of the joining cost exactly (Section 3), pay the interior pair with a variance-refined one-bit inequality (Lemma 4.1, p. 12), and control the common-output corners by a thinning argument (Theorem 6.1, p. 17). The linear bound from the log-Sobolev inequality does not suffice; the nonlinear surplus above is where the difficulty lies.
Cube n = Fin n → Bool, averages are finite sums divided by , logs are natural; sign maps Bool to .psiInv is Function.invFunOn psi (Icc 0 1); since is strictly increasing on and , this is the paper's branch.noise ρ u y = ∑ x, kernel ρ y x * u x with kernel the product of , which is . Mutual information is the finite sum over the joint table, with terms omitted where the joint probability is .F is stated as psiInv s * artanh (psiInv s) and is only used on ; for interior , and , so reserve and hybrid are evaluated in their source domain.i : Fin n. The milestone (separate definition file) uses the crossover form with bits.Given vectors in the Euclidean unit ball of that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on ? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is , the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs , chosen once and for all, such that every signed prefix is , independently of . Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.
Work in Euclidean space with norm , and let satisfy ; repetitions and zero vectors are allowed. A prefix sum is for (the empty sum is ). For a zero-sum family, the Steinitz quantity
is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant is its supremum over all such families.
There is an absolute constant such that for all and all with :
The constant is not fixed. The simplex example in the source shows , so the order is optimal. The goal statement is published on the platform with status Open.
The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: . Theorem 1.1 settles the prefix-discrepancy question of Bansal et al., removing the term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.
Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.
Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a factor, because the probability that a random walk stays in a ball of radius for steps decays with . The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.
EuclideanSpace ℝ (Fin d), indexed by Fin N, with and .SignedPrefixBound C asks for signs (as reals) with every signed prefix at most . OrderingPrefixBound C asks, for zero-sum families, for a permutation with every reordered prefix at most . The goal is ; the same constant serves both, as stated in the source.The triangular Hilbert transform is a bilinear singular integral on the plane that couples translations in two different coordinate directions:
Paired with a third function, it becomes a trilinear form whose three inputs depend on the three pairs of variables of . This "triangular" or entangled structure defeats the time–frequency methods that handle the one-dimensional bilinear Hilbert transform. Boundedness of this operator is a model problem for multilinear singular integrals with simplex structure, and is closely tied to norm convergence and variation of ergodic averages for two commuting transformations. Thiele listed the symmetric case () as Problem 13 in the 2017 collection Some problems in harmonic analysis.
For complex functions on and , the hard truncation is
and the maximal truncation is
For the finite truncations converge absolutely outside a common null set, and is measurable (Lemma 7.1 of the source).
There is an absolute constant such that, for all complex ,
The Lean goal also includes the measure-theoretic preliminaries of Lemma 7.1: almost every point is a point where all finite truncations converge absolutely, and is almost-everywhere measurable. The goal statement is published on the platform with status Open.
The result itself. A uniform bound for the maximal operator controls a truncation chosen independently at each point, which is stronger than a uniform bound on each . It yields existence of the joint principal value almost everywhere and in (Theorem 7.2). By duality and a determinant-one change of variables, it gives endpoint-uniform bounds for the symmetric trilinear triangular form , which resolves Thiele's Problem 13 positively. Earlier bounds all grew with the number of scales.
Formalizing it. The estimate is a clean statement in Mathlib's and lower-integral language. Its proof combines matrix trace inequalities, Gaussian heat-flow energies and discretization limits, all of which would have to be built. The finite-dimensional matrix inequalities (Sections 2–3 of the source) are self-contained and reusable for other entangled multilinear forms.
Time–frequency analysis, which handles the one-dimensional bilinear Hilbert transform, does not adapt to the triangular form because its three inputs are entangled: each depends on a different pair of variables, so no single frequency-localization serves all three. Energy and telescoping methods (Kovač; Durcik) work for bipartite forms, but the triangular cycle is the documented obstruction. Previous cancellation estimates lose a factor depending on the number of scales . The maximal version adds a further difficulty: the truncation endpoints vary from point to point, so the energy argument must tolerate entries that switch on and off at independently chosen scales, without losses depending on the number of scales or on matrix dimensions.
ℝ × ℝ → ℂ with Lebesgue measure; hypotheses are MemLp F 3 and MemLp G 3 (which include a.e. strong measurability).truncation F G E z is the Bochner integral of over , with endpoints packaged as Endpoints ().GoodPoint requires integrability on the annuli for all , hence on every finite annulus. maximal is the ℝ≥0∞-valued supremum over all endpoint pairs at good points, and elsewhere. The goal asserts that almost every point is good, so this junk value cannot help.ℝ≥0∞, compared with eLpNorm F 3 * eLpNorm G 3. The constant is an existential ℝ≥0, so it is finite and independent of .Finite games in strategic form are the basic model of strategic interaction in economics, engineering and computer science. Potential games (Monderer and Shapley, 1996, DOI 10.1006/game.1996.0044) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics converge to one.
Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) decompose every finite game canonically into a potential, a harmonic and a nonstrategic component, by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games are the complement of potential games, and their equilibria behave in the opposite way: they generically have no pure Nash equilibrium. This mission formalizes the paper's positive result on the harmonic side. In every harmonic game, whatever the number of players and strategies, the profile in which every player randomizes uniformly over its strategies is a mixed Nash equilibrium. Rock–paper–scissors and matching pennies are the familiar two-player instances.
A finite game has a finite set of players and, for each player , a nonempty finite strategy set with elements. A strategy profile is . We write for the strategies of the players other than , , and for with player 's strategy replaced by . A game is identified with its utilities , , which form an element of , where carries .
Two profiles are -comparable if they are distinct and differ only in player 's strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function on ordered pairs of profiles with on edges and off edges. The space of edge flows carries . The combinatorial gradient is , with the edge indicator, and is its adjoint. Restricting to -comparable pairs gives , and is the flow of payoff differences of . With (Moore–Penrose pseudoinverse) and , Definition 4.2 of the paper sets
A game is a harmonic game if , and a normalized harmonic game if .
A mixed strategy of player is a probability vector , and a mixed strategy profile is . The mixed extension is (34). The payoff of the pure strategy against is (35). A mixed Nash equilibrium (Definition 5.1.1) is a mixed profile with for every and . A probability distribution on profiles is a correlated equilibrium (Definition 5.1.2) if for all and . The uniformly mixed strategy profile (Definition 5.2) has for every and .
For every harmonic game , the uniformly mixed strategy profile is a mixed Nash equilibrium:
Theorem 5.4 is the counterpart, for harmonic games, of the existence of pure equilibria in potential games. It exhibits an explicit equilibrium that does not depend on the payoffs at all, only on the strategy counts . Corollary 5.2, a milestone here, adds that at any mixed equilibrium of a harmonic game every player is indifferent among all its pure strategies, including those outside the support. That is much stronger than the usual support condition. Proposition 5.2 shows that the correlated equilibria of a normalized harmonic game are the points of the probability simplex in a linear subspace determined by the utilities. The paper uses that description in its later analysis of two-player harmonic games.
The results are proved in the paper; none of them is machine-checked. The formalization connects the paper's operator layer (flows on the game graph, the gradient and its adjoint with the -weighted inner product, pseudoinverses) with standard equilibrium notions on finite games. It reuses published definitions of lotteries, the mixed extension and correlated equilibria.
The equilibrium statement follows quickly once Lemma 5.2 is available. The difficulty lies in translating the harmonic condition, a statement about the adjoint of an operator on edge flows, into an identity about payoffs. That needs the explicit form of , which depends on the in the inner product of . It also needs the fact that kills the nonstrategic component, and a computation of the flow of across the boundary of the set of profiles in which player plays . Corollary 5.2 needs the passage from mixed profiles to product distributions on profiles and a careful accounting of sums over against sums over full profiles.
The first idea, to use the normalization , is not available. The goal concerns all harmonic games, not only normalized ones, and normalization alone does not give indifference against uniform opponents: the harmonic condition is essential.
Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper (). The hypothesis [∀ m, Nonempty (E m)] is stated explicitly on the game theorems, because the uniform profile is a probability vector only if . A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted sum inner product of p. 14. is the subspace of edge flows with the inner product of (7). is Mathlib's adjoint, and the pseudoinverse is defined directly. and are defined by (28), and harmonic games are the submodule H ⊔ N. Lotteries, mixed profiles and the mixed extension (34) come from the published agt_games definitions; correlated equilibrium is the published HartSchmeidler.Finite.IsCorrelatedEq. The pure-deviation payoff (35), mixed Nash equilibrium with pure deviations (Definition 5.1.1, as printed), and the uniform profile are defined in the mission. Sums over are written as sums over the profiles with player 's strategy fixed, so each is counted once.
The goal concerns mixed Nash equilibria. Stating it for the uniform product distribution as a correlated equilibrium, or for normalized games only, would be a weaker statement and is not the target. No hypothesis is added beyond the nonemptiness of the strategy sets.
Contributions welcome: proofs of the milestones, and general lemmas on adjoints of graph gradients and on product distributions that are reusable beyond this mission.
Many data matrices are, to a good approximation, the sum of a sparse matrix (few nonzero entries) and a low-rank matrix. In system identification the low-rank part models a system of small order and the sparse part a system with sparse impulse response; in statistics the same structure appears in latent-variable graphical models, where a sparse inverse covariance is corrupted by a low-rank effect of hidden variables; in signal and image processing it separates a slowly varying background from sparse outliers. Recovering the two components from their sum is NP-hard in general, so a convex relaxation is the natural tractable approach.
Chandrasekaran, Sanghavi, Parrilo and Willsky (arXiv:0906.2220, SIAM J. Optim. 21(2), 2011, doi:10.1137/090761793) introduced the convex program that minimizes a weighted sum of the entrywise norm and the nuclear norm, and gave a deterministic condition under which it recovers both components exactly. The condition is an uncertainty principle between the support of the sparse matrix and the row and column spaces of the low-rank matrix. Their analysis was followed by probabilistic guarantees for the same program under random sparsity patterns (Candès, Li, Ma, Wright, Robust Principal Component Analysis?, J. ACM 2011, arXiv:0912.3599).
All matrices are real and square, . For a matrix :
The two rank-sparsity incoherence quantities are
Small says that the elements of are not concentrated on few entries; small says that the elements of have diffuse spectra.
Given and a trade-off parameter , the decomposition program is
If
then for every
the pair is the unique optimum of (1.3); moreover always lies in this interval (for ).
Theorem 2 is a deterministic exact-recovery guarantee: it involves no randomness, only the support of and the row and column spaces of , and so it applies to any fixed instance for which and can be bounded. Combined with the paper's bounds of by the maximum number of nonzeros per row or column and of by the coherence of the singular vectors, it yields explicit sparsity-versus-incoherence trade-offs under which (1.3) succeeds. It is the starting point of the analysis of sparse-plus-low-rank decompositions in robust PCA, latent-variable graphical model selection and system identification.
The theorem is proved in the paper. No machine-checked proof of it, of Propositions 1–2, or of the subdifferential characterizations (4.4)–(4.5) is known to exist. A formalization adds: a checked account of the edge cases the paper leaves implicit (a zero sparse or low-rank component, the open endpoints of the -interval), a reusable library of the two tangent spaces and their projections for the Prove2Me matrix-completion definitions, and the nuclear-norm subdifferential (Watson's theorem), which is used throughout low-rank recovery.
The obvious argument writes down a dual certificate and checks four conditions; the work is in showing that one exists. The natural candidate is defined implicitly, as the unique element of with prescribed projections onto and , and its existence is a linear-algebra fact about two transverse subspaces, not a formula. Bounding its components outside and requires coupled estimates in two different norms, the spectral norm and the entrywise maximum, related only through and . On the convex-analysis side, the "only if" direction of the nuclear-norm subdifferential characterization (4.5) is a genuine theorem about singular values, not a computation.
Statements follow the arXiv v1 preprint (arXiv:0906.2220v1), with its numbering and page numbers. Matrices are Matrix (Fin n) (Fin n) ℝ; the rectangular remark of §3 is not formalized. The nuclear norm, spectral norm, , trace inner product, , , the SVD datum and are the published Prove2Me definitions matrix_completion_basic, matrix_completion_svd and matrix_completion_tangent. The SVD of is an explicit argument: , and are taken with respect to it, and every statement holds for every compact SVD. and are real suprema of bounded sets containing , hence maxima. Subgradients use the inequality ; means for a subgradient .
"Unique optimum" is strict: every other feasible pair has strictly larger objective, so a statement only asserting that minimizes the objective, or a definition of or that collapses to , does not count. The upper end of the -interval is stated as , which is the paper's condition when and means "no upper bound" when ; the "specifically" clause assumes and because it divides by and needs .
A complete development needs: the subdifferentials of the and nuclear norms, the fixed-point and norm properties of (in particular ), and the direct-sum argument for . The nuclear-norm subdifferential and the bounds are reusable across all of low-rank matrix recovery. Proofs of any milestone, and lemmas that shorten the Appendix B estimates, are welcome.
In a flexible commitments contract a retailer announces, before a selling horizon starts, a vector of planned orders (commitments) to its supplier, who uses them to plan capacity. During the horizon the retailer may deviate from the commitments, but pays penalties for each deviation and for changes between successive commitments. Such contracts were studied with stochastic demand by Bassok and Anupindi, Tsay and Lovejoy, and others, typically by dynamic programming over a discretized state space.
Ben-Tal, Golany, Nemirovski and Vial (2005) treat the retailer's problem as a robust multiperiod linear program: demand is only known to lie in an uncertainty set, decisions may adapt to observed demand, and the retailer minimizes its worst-case total cost. Most of the paper approximates this problem by affinely adjustable decision rules. For one important case, however, the paper shows that the problem can be solved exactly: when the uncertainty set is a box, nature may be restricted to the finitely many corner trajectories of the box. That reduction, Proposition 1 of the Appendix, is the subject of this mission, together with the general principle behind it (Lemma 2), which applies to any multistage worst-case problem with polyhedral dynamics and convex polyhedral costs.
Data. There are periods. Period carries an ordering cost , a holding cost , a shortage cost , penalties for ordering above or below the commitment, and penalties for raising or lowering the commitment relative to the previous one. A salvage value applies to the final inventory; put for and . The initial inventory and a nominal previous commitment are given, as are order bounds and cumulative bounds , possibly infinite.
Decisions. Before any demand is observed the retailer fixes commitments and amounts . Demand lies in a product set . The order and the cost bounds of period are decision rules, functions of the past demands ; the inventory is a function of . This nonanticipativity is required on trajectories of .
The min-max RSFC problem (5)–(6). A policy is feasible if for every and every : ; the order and cumulative-order bounds hold; and ; and ; and , . The optimal value is
Box uncertainty (9)–(10). with ; its extreme points are .
Convex polyhedral functions. A function is a c.p.f. if its domain is the solution set of finitely many linear inequalities and is convex and lower semicontinuous on it. Lemma 2 concerns the generic problem : minimize, over decision rules , the worst case over of , subject to , and .
The data are arbitrary reals (bounds in ) and the values are compared in the extended reals, so the statement covers infeasible and unbounded instances.
Proposition 1 turns a semi-infinite multistage problem into a finite one: with box uncertainty, the min-max RSFC problem is equivalent to a linear program over the scenario tree of the corner trajectories, problem of §2.3. The paper uses this exact value as a benchmark for its affinely adjustable approximation in the simulation study. Lemma 2 is the transferable statement: in any multistage worst-case problem whose stage costs are convex polyhedral and whose dynamics are linear with a uniform box on the decisions, the adversary may be restricted to the vertices of each period's uncertainty polytope.
The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a reusable notion of convex polyhedral function in the extended reals, closure properties of that class (partial minimization over a polyhedral box, affine substitution, finite maxima, sums), and a formal worst-case Bellman equation for nonanticipative policies. The corrected form of the -box step also records precisely when the paper's informal "for large enough" argument is valid.
The natural argument, "a convex function attains its maximum over a polytope at a vertex", applies to one stage only. In a multistage problem the cost of the last stage depends on the earlier decisions, which depend on earlier demands, so the worst case is not a convex function of the whole trajectory. The proof must therefore pass through a dynamic programming recursion, and the class of stage costs must be closed under the recursion: the optimal last-stage value as a function of the previous decision must again be convex polyhedral. That closure (the value of a parametric problem with a convex polyhedral objective and a box constraint) is where the work is: the domain is a projection of a polyhedron, and attainment and lower semicontinuity have to be shown with infinite values allowed.
A second difficulty is bookkeeping. The RSFC problem must be rewritten as an instance of Lemma 2 with the right stage vectors so that nonanticipativity of in is preserved, and the bounded problem must be related back to the unbounded one, which can have value .
Periods of the RSFC model are Fin T, 0-based. Policies are functions of the whole demand trajectory with nonanticipativity imposed on trajectories of the uncertainty set; a policy that sees future demand is not admissible, which rules out the clairvoyant reading under which the statement changes. Optimal values are EReal infima of suprema: for infeasible problems and possibly , never a real sInf that would turn both into . The c.p.f. definition requires the domain to be exactly a finite system of linear inequalities, so it cannot be satisfied vacuously.
The standing assumptions of §2.2, and (1) , are not imposed, and no sign is assumed on any cost or penalty: Proposition 1 holds without them, so the formal statement is a generalization. The norm is Mathlib's default norm on Fin m → ℝ. Lemma 2's families are indexed by with the paper's indices; B t, C t stand for , . Two printed slips are corrected in the statements: (38) keeps the that the page drops, and the -box step is stated in the corrected sandwich form because the literal claim fails when the value is .
Useful infrastructure: convex polyhedral functions in EReal, Fourier–Motzkin projection of polyhedra, maximum principle for convex functions on polytopes, extreme points of convex hulls of finite sets. Contributions to any milestone, and to general lemmas on these topics, are welcome.
Airlines, hotels and car-rental firms sell reservations ahead of service, and a fraction of those reservations cancel or do not show up. Overbooking — accepting more reservations than there is capacity — recovers revenue that cancellations would otherwise destroy, at the risk of denying service to some customers. In practice inventory is often substitutable: a passenger booked in economy can be upgraded to business, a guest booked in a standard room can be given a suite. With substitution, the right overbooking level for one reservation class depends on the levels of all the others.
Karaesmen and van Ryzin (Operations Research 52(1):83–104, 2004) model this as a two-period problem: overbooking decisions in a reservation period, followed by an optimal assignment of the customers who actually show up to inventory classes in a service period. Their structural result, Theorem 2, establishes the shape of the expected net revenue as a function of the overbooking levels. That shape is what justifies critical-level booking policies and the stochastic-gradient method of their §4, and it is the textbook account of joint overbooking with substitution (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 4.4).
There are reservation classes and inventory classes . Class is virtual: assigning a customer to it means the customer is denied service.
Reservation period. The firm holds reservations of class and chooses overbooking levels . Accepting a class- reservation earns ; a cancellation of class is refunded , with . The number of class- customers who survive to the service period is a random variable with values in . The family has the semigroup property: if and are independent with the laws of and , then has the law of . The binomial model ( for integer ) and the Poisson model () both have it. The survivals of different classes are independent.
Service period. Given the survivals , net benefits (of either sign) and capacities , the firm solves the transportation problem
Expected net revenue. The objective of the reservation period is
to be maximized over .
A function on is submodular on if for , with the componentwise maximum and minimum.
For every with levels in the parameter set , every class and all ,
and is submodular on :
The first statement is the paper's componentwise concavity (6); the second is its submodularity, proved in the paper through the pairwise inequality (7) and Theorem 1.
Componentwise concavity of implies that for each reservation class there is a critical booking level beyond which expected revenue does not increase, other levels held fixed. Submodularity implies that these critical levels are nonincreasing in the bookings accepted for any other class: heavier overbooking in one class leaves less spare substitute capacity for the others. These two properties underpin the heuristics and the stochastic-gradient optimization of §4–§5 of the paper.
The result is proved in the paper (for , with the general case described as straightforward). A machine-checked version would cover the general semigroup case, which includes the binomial model the paper calls realistic, real-valued levels and arbitrary step sizes. The platform already holds a proved special case, RevenueManagement.joint_overbooking_concave_submodular (Talluri–van Ryzin, Proposition 4.4): Poisson survivals, integer levels and unit steps only. This mission generalizes it in all three respects and also formalizes the transportation-problem facts (LP duality, submodularity and concavity of ) as reusable statements.
The obvious route — differentiate and use concavity of — fails twice. First, is piecewise linear and the survivals are discrete, so there is nothing to differentiate; under the binomial model is only defined at integer levels. Second, concavity of alone does not survive the expectation: is a mixture over laws that change with , and a concave function of a random vector whose law moves with the parameter need not be concave in the parameter. The semigroup property is what replaces a change of law by the addition of an independent block of survivors, and that coupling must be built for every coordinate and every pair of coordinates at once. On the LP side, submodularity of a transportation-problem value in its demands is a lattice-programming fact (Topkis, Theorem 3.4.1; Shapley 1962), not a consequence of concavity.
All declarations are in the namespace SubstOverbooking.Structure. Reservation classes are Fin n (0-based), inventory classes Fin (m + 1) with 0 the virtual denied-service class. Conventions committed to:
SupermodularOn applied to .A formalization that fixes Poisson laws, integer levels or unit steps, or that defines or through the inequalities to be proved, is the already-proved special case or an empty statement, and is not the goal.
A complete development needs finite LP duality for the transportation problem, the lattice-programming argument for Lemma 1, product measures and image measures on , and the coupling of the semigroup property. The LP and lattice parts are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1 (for instance via monotonicity of optimal duals, after Erlenkotter 1970).
Conic quadratic (second-order cone) programs are solved in practice by primal-dual interior-point methods. Each iteration solves a Newton system for the central-path equations, and for non-polyhedral cones that system is only guaranteed to be well posed after the problem is scaled: the primal point and the dual slack are transformed by a matrix chosen from the current iterate. Among the scalings analysed by Monteiro and Tsuchiya (2000), the best complexity bounds are obtained with the Nesterov–Todd (NT) scaling of Nesterov and Todd (1997), which maps and to the same point.
Andersen, Roos and Terlaky (2003) describe the conic quadratic interior-point solver of MOSEK. Their Lemma 4.2 gives the NT scaling in closed form for each of the three cone types they use. It is what makes the NT direction cheap: each cone block of is determined by one vector , and , and their inverses can be applied in time linear in the dimension. For the quadratic cone the formula goes back to Tsuchiya (1999); the paper re-derives it and extends it to the rotated quadratic cone.
Fix one cone block of dimension . Coordinates are , denotes the subvector of coordinates , and is the Euclidean norm. The block is one of
A scaling matrix (Definition 3.3) is a symmetric positive definite with . For the scaled points are and . The pair is an NT scaling of when , equation (28); equivalently , equation (29).
For in the interior of the cone:
the following matrices make an NT scaling: for ;
for ; and
for . In the last two cases , equations (33) and (35).
Lemma 3.3 i)–iii) (scaling preserves and rescales , by ); (30) on its own; the normalization and the square (62) of the arrow form (31); positivity of the radicand of (32); the identity and the formula (32); for the rotated cone, the transport (63) by , the identities and , and . Two companions: Lemma 4.3, , and Lemma 3.3 iv), that a scaling maps the cone and its interior onto themselves.
The result. Lemma 4.2 turns the NT scaling, defined implicitly by (28), into explicit data: one scalar and one vector per cone. Combined with Lemma 4.3 it shows that every product with , or their inverses in the scaled Newton system (27) is a rank-one correction of a signature matrix, which is what the paper's implementation relies on. The rotated-cone formula (34) is the paper's own addition and is what lets rotated cones be handled natively instead of through a change of variables.
Formalizing it. The result is proved on paper; no machine-checked version is known to exist, and the platform has no formalization of second-order-cone scalings. The work is the matrix algebra of the Lorentz group — the signature matrix , the matrices with , and their action on and — which is reusable for every second-order-cone algorithm.
Most of the items are finite-dimensional identities, but they are identities between block matrices of arbitrary size with entries that are nested square roots, and they hold only on the interior of the cone, where the radicands are positive. The derivation in the paper runs backwards: it assumes has the shape (31) and solves for , taking a square root without fixing its sign. The goal asks for the forward direction — that the displayed , , do satisfy (28) and — which needs the normalization , positive definiteness of , and, for the rotated cone, the reduction to the quadratic cone through with and .
kind : ConeKind, and vectors are Fin d → ℝ.0. is written as a sum of squares (tailSq x 1); Mathlib's norm on Fin d → ℝ, which is the sup norm, is never used.A complete development needs:
Matrix.PosDef and Matrix.inv;Lemmas about (closure under products and inverses, invariance of ) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for positive definiteness of (31).
In a road or communication network, each user picks a route to minimize its own delay, without regard to the delay it imposes on others. The outcome is an equilibrium that is in general not socially optimal: Braess's paradox shows that adding a road can make every user worse off, and Pigou's two-link example shows that selfish users can incur a third more total delay than a central planner would. Transportation science has studied such equilibria since Wardrop (1952) and Beckmann, McGuire and Winsten (1956). The computer-science question of how much is lost, uniformly over all networks, was answered for linear delays by Roughgarden and Tardos in How Bad is Selfish Routing? (FOCS 2000; J. ACM 2002, doi:10.1145/506147.506153). Their bound became the first instance of the price of anarchy for nonatomic routing and the template for a large literature on the inefficiency of equilibria.
Timeline. Wardrop (1952) states the equilibrium principle. Beckmann et al. (1956) and Dafermos–Sparrow (1969) characterize equilibria and optima by convex programs. Koutsoupias and Papadimitriou (1999) introduce the worst-case ratio of equilibrium to optimum. Roughgarden and Tardos (2000/2002) prove the bound for linear latencies, tight by Pigou's example. Roughgarden (2003) and Correa, Schulz and Stier-Moses (2004) extend the analysis to general latency classes.
A network has finitely many edges and finitely many routes ; a route is the set of edges it uses, recorded by a incidence. There are commodities; each route serves one commodity , and is the set of routes serving . Commodity has a positive rate . A flow assigns a nonnegative amount to each route; it is feasible for if for every . The edge flow is .
Each edge has a linear latency with . The latency of a route is , and the cost of a flow is
A feasible flow is at Nash equilibrium if no small amount of flow on a route can reduce its latency by moving to another route of the same commodity (Definition 2.1); equivalently (Lemma 2.2), every used route of commodity has minimum latency among the routes in . A flow is optimal if it is feasible and has minimum cost among feasible flows. The marginal cost of edge is , and .
The Lean development uses the names pathLatency, cost, IsNashFlow, IsOptimalFlow, linLatency, marginalLatency and minMarginalPathCost for these objects.
For every instance with linear latencies , every Nash flow and every feasible flow ,
This is the paper's , stated without the ratio.
The bound says that, with linear delays, selfish routing never costs more than times the optimum, independently of the network's size and topology and of the number of commodities. It explains why Braess-type phenomena are bounded in magnitude, and it yields consequences for mechanical networks of strings and springs (Corollary 4.6 of the paper). The inequality for every feasible is the basic input to later work on bicriteria bounds, Stackelberg routing, tolls and the general price-of-anarchy framework.
The result is proved in the paper and in textbooks (Nisan et al., Algorithmic Game Theory, ch. 18). No machine-checked proof is known to exist on Prove2Me or in Mathlib. A formalization produces a checked model of nonatomic routing (route flows, Nash and optimal flows) together with the first-order characterization of optimal flows for convex quadratic costs, both of which are reusable for the other results of the paper and for later routing papers.
The equilibrium bound is not a pointwise inequality between the two flows: the Nash flow and an arbitrary feasible flow can use entirely different routes. The step that requires real work is the comparison between an optimal flow for the rates and an arbitrary flow for the rates (Lemma 4.4), which rests on the characterization of optimal flows of a convex program (Lemma 4.1(b)). That characterization is a Karush–Kuhn–Tucker statement over a polytope of route flows; the paper cites it rather than proving it, and Mathlib has no ready-made version. The naive approach, bounding each edge's cost separately, fails because the two flows load different edges.
Fin J, Fin R, Fin Sd. A route is a column A j r of the incidence; the commodity of route r is s r. The paper's simple paths in a directed graph are one instance, so all statements are a disclosed generalization; copies of one path serving two commodities are two routes.KellyStochasticNetworks.linkFlow and KellyStochasticNetworks.wardropFeasible; the Wardrop condition is KellyStochasticNetworks.IsWardropEquilibrium.0 < rate i), as on p. 6. Linear latencies have , and only their values at nonnegative arguments matter.Needed infrastructure: the edge/route exchange of summation, the first-order optimality conditions for a convex differentiable function on a product of simplices, and the convexity inequality . Contributions of a general KKT lemma for separable convex costs on flow polytopes are reusable beyond this mission.
Many problems in system identification, collaborative filtering, low-dimensional embedding and model reduction ask for the simplest matrix consistent with a set of linear observations, where "simplest" means "of least rank". Given a linear map and a vector , the affine rank minimization problem is
This problem is NP-hard in general: it contains the problem of finding the sparsest solution of a linear system as the special case of diagonal matrices. A standard heuristic, popularized in control by Fazel, Hindi and Boyd, replaces the rank by the nuclear norm , the sum of the singular values, which is the convex envelope of the rank on the unit ball of the operator norm. The resulting problem is a semidefinite program and can be solved efficiently.
Recht, Fazel and Parrilo (arXiv:0706.4138, SIAM Review 2010) gave the first general conditions under which this heuristic provably returns the minimum-rank solution. Their argument transfers the compressed sensing theory of Candès and Tao (Decoding by linear programming, 2005) and Candès, Romberg and Tao from sparse vectors and the norm to low-rank matrices and the nuclear norm. This mission formalizes the paper's deterministic recovery theorem (Section 3).
Matrices are real matrices. For matrices of the same size, is the trace inner product. With the singular values of , the three norms used are the operator norm , the Frobenius norm , and the nuclear norm .
A linear map is given by measurement matrices through ; is the Euclidean norm of the vector .
For an integer , the -restricted isometry constant (Definition 3.1) is the smallest with
Fix a matrix of rank at most , put , and consider the nuclear norm minimization problem
If and , then ; precisely,
The statement holds for every linear map, every and every of rank at most . The constant is the paper's; the paper notes (p. 14) that its derivation is chosen for simplicity and is not optimal.
Theorem 3.3 is a deterministic certificate: it separates the question "does nuclear norm minimization recover low-rank matrices?" into a property of the measurement map alone, with an absolute constant independent of , , and . Section 4 of the same paper then shows that random maps with i.i.d. Gaussian or Bernoulli entries satisfy with high probability once is of order , so a matrix with entries is determined by far fewer measurements than entries and is found by a semidefinite program.
The theorem is proved in the paper, and the sparse-vector analogue has been formalized on this platform (HighDimProb.SparseRecovery.rip_implies_exact_recovery, from Vershynin's textbook; CandesTao.Decoding.decoding_by_lp). The matrix version is not formalized. A machine-checked proof needs the basic theory of singular values for rectangular real matrices (the norm comparisons (2.1), additivity of the nuclear norm, the triangle inequality for the nuclear norm, and block decompositions via the singular value decomposition), most of which Mathlib lacks in this form. That infrastructure is reusable for every nuclear-norm result on the platform.
For sparse vectors the analogous proof splits the error vector by its support, and every step is coordinatewise. For matrices there is no common basis: the error and the target have different singular vectors, and the restricted isometry inequality controls only matrices of low rank. The first obstacle is therefore to split into a piece of rank at most and a piece whose row and column spaces are orthogonal to those of , so that the nuclear norm is additive. The second is that the triangle inequality, additivity and the norm chain (2.1) for the nuclear norm are themselves nontrivial statements about singular values. Applying the restricted isometry inequality directly to fails, because need not have low rank.
Matrix (Fin m) (Fin n) ℝ; rank is Matrix.rank; transpose is Xᵀ. The norms and the inner product are opNorm, frobeniusNorm, nuclearNorm and traceInner of the published module HighDimStat_MatrixRank_Core, which defines the nuclear norm as the sum of the square roots of the eigenvalues of .Xs : Fin p → Matrix (Fin m) (Fin n) ℝ and evaluated by observationOp; measNorm Xs X is .ripConst Xs r is the infimum of the admissible ; the set is nonempty and closed, so the infimum is attained. It is defined for every , not only , since the goal uses . The paper's normalization is not assumed.Welcome contributions: a rectangular SVD with ordered singular values, the triangle inequality and duality for nuclearNorm, and the attainment and monotonicity lemmas for ripConst.
The support vector machine (SVM) is a linear classifier trained by minimising a regularised hinge loss. For training sets with millions of examples, solving the SVM problem to high accuracy by interior-point or dual decomposition methods is too slow, and what is needed is an algorithm whose cost per iteration does not grow with the number of examples. Pegasos (Primal Estimated sub-GrAdient SOlver for SVM), introduced by Shalev-Shwartz, Singer and Srebro in 2007 and analysed in its final form by Shalev-Shwartz, Singer, Srebro and Cotter in Mathematical Programming (2011, doi:10.1007/s10107-010-0420-4), is a stochastic sub-gradient method on the primal SVM objective with step size . Its analysis showed that the number of iterations needed for accuracy is , independent of the training-set size, and the method became a standard baseline for large-scale linear SVM training.
The analysis rests on a logarithmic-regret bound for online gradient descent on strongly convex functions, due to Hazan, Agarwal and Kale (Machine Learning 69, 2007), which the paper re-proves for non-smooth functions as its Lemma 1 and then applies to the Pegasos iterates in its Theorem 1.
A training set consists of examples , , with and labels . The hinge loss of a weight vector on is . For a regularisation parameter , the SVM objective (Eq. (1)) is
and denotes a minimiser of (Eq. (9)). For a mini-batch of example indices, the instantaneous objective (Eq. (7)) is
Mini-batch Pegasos (Fig. 2 of the paper) starts at . At each round it receives a mini-batch , forms the sub-gradient
of at , and sets with . Optionally it then applies the projection step (6), , which maps to the closest point of the Euclidean ball of radius . A function is -strongly convex if is convex, and is a sub-gradient of a convex at if for every .
In the Lean development these objects are svmObj, instObj, subgrad, projBall and run in the namespace Pegasos.Analysis; the hinge loss is UnderstandingML.hingeLoss, sub-gradients are UnderstandingML.IsSubgradient, and " is the projection of onto " is LogRegretOCO.OGD.IsProj B v z.
Assume for every , and set when the projection step is performed and when it is not. Then for every sequence of mini-batches and every ,
The constants are the paper's and are stated exactly; a version with a single constant for both variants, or with an unspecified constant, is a weaker theorem.
Theorem 1 is the deterministic core of every guarantee in the paper. Taking expectations over uniformly random mini-batches turns its left side into the expected objective of the iterates and its right side into plus the rate, which yields the iteration bound and, via Markov-type arguments, the high-probability bounds of the later sections. Because the bound holds for every sequence of mini-batches, it is also an online-learning regret bound for the sequence of instantaneous objectives.
The result is proved in the paper and is classical. To our knowledge it has no machine-checked proof. Formalizing it produces a verified logarithmic-regret lemma for non-smooth strongly convex sub-gradient descent with an arbitrary closed convex feasible set (the platform currently has the twice-differentiable version with a bounded feasible set), a verified sub-gradient calculus for the regularised hinge loss, and an exact treatment of the Pegasos iteration including both the projected and unprojected variants.
The obvious argument applies Lemma 1 with the ball of radius in both variants and the sup of over that ball. This fails twice. Without the projection step the iterates are not confined to that ball, so a separate argument (the closed form (13)) is needed to bound them, and it gives the different constant . With projection, Lemma 1 requires the comparator to lie in the ball, and is not implied by the elementary comparison , which only gives ; the paper obtains the sharp radius through duality. In Lemma 1 itself, the telescoping only closes because the step size is matched exactly to the strong-convexity modulus; any off-by-one in the step indexing breaks the cancellation.
Vectors are EuclideanSpace ℝ (Fin n), examples are indexed by Fin m, labels are real numbers with the hypothesis , and , are hypotheses. A mini-batch is a -tuple Fin k → Fin m: an injective tuple is a subset of size as in Fig. 2, a non-injective one is the multi-set with repetitions the paper also allows. The theorem is stated for every sequence of mini-batches A : ℕ → Fin k → Fin m; no probability space appears, because the proof never uses that the batches are random. Iterations are 1-based: run … 1 = 0, the step producing uses and the batch only, and index 0 is unused. The variant is selected by a Boolean flag, and depends on it. is any with for all , minimising the full objective (1), not the instantaneous ones. Strong convexity is the paper's own definition, convexity of . At the projection formula is evaluated with Lean's , which gives the intended value . The paper's display (12) has two printed slips (the sign of the term and for ); the Lean states the correct update, and Eq. (13) is correct as printed.
A trivializing formalization is ruled out: the goal is stated for the concrete iteration run, not for an abstract sequence assumed to be sub-gradient steps or projections, and those facts are separate milestones.
A complete development needs the sub-differential sum rule for a convex function plus a quadratic, convexity of the hinge loss, the variational characterisation of the projection onto a ball, the harmonic-sum bound , and a proof of (through duality or a direct optimality argument). Lemma 1 and the sub-gradient lemmas are reusable for any strongly convex stochastic sub-gradient method. Proofs of any milestone, and alternative proofs of the bound on that avoid the dual problem, are welcome.
Scheduling jobs on identical parallel machines to minimize the total weighted completion time , the problem , is one of the basic NP-hard problems of machine scheduling. On a single machine it is solved by Smith's ratio rule (Smith 1956); with several machines the only hard decision is which jobs share a machine. Section 6 of M. Skutella's paper Convex quadratic and semidefinite programming relaxations in scheduling (J. ACM 48 (2001)) observes that this decision is a graph partitioning problem: the cost of a schedule is, up to a constant, the weight of the edges that a partition of a weighted complete graph does not cut. Minimizing on machines is therefore equivalent to Max--Cut on that graph, and the paper shows that the equivalence preserves approximation in a quantified way.
The reduction explains, from the graph side, why semidefinite rounding works for two machines: with the 0.878-approximation for MaxCut of Goemans and Williamson (1995) it gives a 1.122-approximation for (Corollary 6.2 of the paper). For general , the uniform random partition is both a -approximation for Max--Cut and randomized rounding of the optimum of the convex quadratic relaxation (CQP).
There are jobs and identical machines. Job has a processing time and a weight . Smith's order puts when , ties broken by index. An assignment is a partition of the jobs; each machine processes its jobs in the order without idle time, so the completion time of is
The value of is , and is the minimum value over all assignments.
The graph is the complete graph on in which the edge with has weight ; is its total weight. A partition induces the -cut , the edges whose endpoints lie in different parts, of weight ; is the maximum weight of an -cut.
The convex quadratic relaxation (CQP) of §2.2, specialised to identical machines, has variables with and objective where
Its optimum value is .
For , any assignment whose -cut weighs at least satisfies
That is, a -approximation algorithm for Max--Cut translates into a -approximation algorithm for . The constant is a parameter, so the goal does not depend on the best known cut algorithm.
The result. Theorem 6.1 makes Max--Cut algorithms usable for scheduling with an explicit loss: a cut algorithm with ratio close to yields a schedule within of optimal. For and the Goemans–Williamson ratio the guarantee is , better than the of Theorem 2.6 b) and the of the paper's semidefinite rounding in §5. In the other direction, (38) bounds the maximum cut of by the scheduling lower bound , which is how a relaxation for scheduling becomes a bound for a cut problem. The problem itself is better understood today: has a polynomial-time approximation scheme (Skutella and Woeginger 2000), and a fully polynomial one for fixed (Sahni 1976). The reduction remains of interest as a structural identity between the two problems and as the source of the closed-form relaxation bound (37).
Formalizing it. All statements are proved in the paper; none is known to have a machine-checked proof. The mission produces a formal model of identical-machine scheduling under Smith's rule, of the weighted graph and its -cuts, and of (CQP) for identical machines, together with the closed-form optimum of (CQP) (Lemma 2.5), which is the basis of the guarantee of Theorem 2.6 b).
The bookkeeping identity (36) and the final chain of inequalities are finite-sum manipulations. The substance is Lemma 2.5: that the uniform vector minimizes the quadratic objective (11) over the product of simplices. The objective is not separable, since the term couples jobs through Smith's order, and its convexity on the feasible region (the positive semidefiniteness established in Lemma 2.4 of the paper) is the fact on which optimality and, with distinct positive ratios, uniqueness rest. The relaxation half of (37), that is at most the value of every schedule, needs the observation that evaluated at the 0/1 vector of an assignment equals the value of that assignment.
Jobs are Fin n and machines Fin m, 0-based; Smith's order is cross-multiplied (, or equality and ), equal to the ratio definition because . Assignments are functions Fin n → Fin m, and every machine is sequenced by ; by Smith's rule (p. 7 of the paper, a classical result it cites) this loses no optimality, so is the minimum over assignments and is never a primitive: "within factor of " is stated against the value of every assignment. Likewise "weight at least " is stated as for every assignment , so no supremum of an empty or unbounded set can enter. The edge weight is attached to the ordered pair with and is zero on the other orientation, so each edge of is counted once. Standing hypotheses on every theorem: , (p. 2 of the paper) and (needed for ). Theorem 6.1 keeps the page's .
Not formalized: polynomial running time, the phrase "approximation algorithm" beyond the value bound it asserts, and the semidefinite results of §5 and Corollary 6.2. A trivializing reading, such as stating the cut condition against a junk-valued supremum or replacing by a free variable, is excluded by the encodings above.
The development needs only finite sums over Fin types and real arithmetic; the model of identical-machine scheduling under Smith's rule and the closed form of (CQP) are reusable for other results on . Proofs of the milestones, alternative proofs of Lemma 2.5 (the KKT argument the paper mentions, or Goemans' symmetrization argument it gives), and a proof of Theorem 2.6 b) are all welcome.
Retailers in many categories accept returns of products that are not defective: a consumer buys, learns whether the product suits them, and may send it back for a refund. Returns of this kind are a large cost item in retailing, and the refund a retailer offers is an operational decision on a par with its price and its stocking quantity. Xuanming Su, Consumer Returns Policies and Supply Chain Performance (SSRN 1020451, version of August 2008; published in Manufacturing & Service Operations Management 11(4), 2009, doi:10.1287/msom.1080.0240), studies this decision first for a single seller and then in a supply chain.
This mission formalizes the supply chain part, Section 5 of the paper. A classical result of supply chain contracting is that a manufacturer can align a retailer's ordering decision with the interest of the whole chain by a buy-back contract, which pays the retailer a credit for unsold units (Cachon, Supply Chain Coordination with Contracts, 2003). Su shows that once the retailer also sets a consumer returns policy, the standard buy-back no longer coordinates, and identifies three contracts that do. The companion mission (mission 1 of this series) formalizes the single-seller results of Sections 3–4, in particular Proposition 2, which gives the supply chain optimum used here.
A consumer who buys at price learns a valuation , drawn independently from a law with finite mean , and then either keeps the product or returns it for the refund . Keeping is optimal when . Write
for the probabilities of keeping and returning. A consumer's expected utility from buying is , which is therefore the reservation price: all consumers buy if and none buys otherwise (the demand rule (6)). Market demand has distribution function and ; a stock sells in expectation when consumers buy, and nothing when they do not. Write for these expected sales. The production cost is , leftover and returned units are salvaged at , and .
The total supply chain profit is
A manufacturer sells to a retailer, who sets , and (except in Proposition 4) . The contracts are:
The supply chain optimum, from Proposition 2 of the paper, is
For and , the differentiated buy-back
makes the supply chain optimum a retailer optimum and gives the retailer the share :
and the contract is implementable: , , .
The results separate what a contract must observe in order to coordinate a chain with consumer returns: either the manufacturer distinguishes returned from unsold units (Propositions 3 and 4), or it observes sales (Proposition 5). The negative results (milestones 1 and 8) show why the standard buy-back and a kept-only rebate fail: each distorts the retailer's refund away from the salvage value. These statements are proved in the paper by short arguments; none of them has, to the knowledge of this mission, a machine-checked proof. Formalizing them yields a reusable model of a newsvendor with an endogenous price and refund under valuation uncertainty, and a checked account of the coordination conditions, including the boundary cases (, atoms in the valuation law) that the paper does not discuss.
Each result combines two optimizations, and neither is routine at the generality of the formal statements. The first is over price and refund jointly: the demand rule makes every profit discontinuous in and , and the refund problem must be solved for an arbitrary valuation law, where atoms make the tie rule at matter. The second is a newsvendor problem in for an arbitrary demand law: the paper writes the optimal stock as of a fractile, which presumes a continuous, strictly increasing , whereas here may jump or be flat and the optimal stock is any solution of the fractile equation. The obvious reduction, "the retailer's profit is , so its maximizer is the chain's", is not available: that identity holds only at the chain's price and refund, and away from them the retailer's profit is not proportional to . In Proposition 4 the manufacturer's deviation to a refund below acts on the consumers' purchase decision, and the paper's remark that no one then buys is false when almost surely, so that case needs its own argument.
Prices, refunds, costs, quantities and profits are real numbers. The valuation law is a probability measure on with integrable identity (a strict generalization of the paper's density ); and , matching the rule "keep iff ". The demand law is a probability measure on with , and is SupplyChainTheory.expSales from the published module SupplyChainTheory_contracts. Every profit includes the demand rule (6): without it, (15) and (31) are unbounded in . Optimization is over all real and and all , nonnegative stocks and demand being the paper's setting; with negative stocks the profits are unbounded. Optimality of the paper's closed-form triple is claimed, never uniqueness, and "induces the retailer to maximize supply chain profit" is stated as "the chain-optimal triple is a retailer optimum"; that the triple maximizes is Proposition 2, formalized in mission 1, and not restated. The optimal stock is any solution of the fractile equation, and no continuity of is assumed. The Nash equilibrium of Proposition 4 is written as the two best-response inequalities. Proposition 5 adds the hypothesis , implied by the paper's range (p. 19) and necessary: for the retailer's profit is unbounded. The kept-only rebate of Sec. 5.4 has no printed formula; its profit is (24) with the rebate removed from the returned-units term. Printed page numbers equal PDF page numbers throughout the source. A formalization in which the retailer's profit is defined as , or in which the optimization is restricted to , would make the goal trivial and is excluded: (31) is stated with free , , , and the contract enters only through hypotheses.
The model module (SuReturns.Coordination.Model) restates the single-seller objects of mission 1 in this sub-namespace. Contributions welcome: proofs of the two optimization steps as reusable lemmas (the refund step for a general valuation law and the newsvendor step for an arbitrary demand law), which serve every milestone here.
Financial institutions, insurers and engineers who manage the risk of a decision describe it by a statistic of the loss distribution that the decision induces. The value-at-risk (VaR) at confidence level , the -quantile of the loss, became an industry and regulatory standard in the 1990s, but it is not subadditive and behaves erratically as a function of the decision when the loss distribution has atoms, as it always does in scenario-based models. The conditional value-at-risk (CVaR), roughly the average of the losses beyond VaR, was proposed as a replacement that is coherent in the sense of Artzner, Delbaen, Eber and Heath and that can be optimized.
In an earlier paper (Rockafellar and Uryasev, 2000) the same authors showed, for loss distributions with continuous distribution functions, that CVaR is the minimum value of an explicit convex function of one real variable, and that VaR is a minimizer. That formula turned CVaR minimization over a portfolio into a linear program and is the reason CVaR is used in practice. The paper formalized here (Rockafellar and Uryasev, Research Report #2001-5, 2001, published in J. Banking & Finance 2002) defines CVaR for general loss distributions, discrete ones included, and proves that the minimization formula survives.
Timeline.
A decision lies in a set ; an uncertain outcome has a Borel probability law that does not depend on . The loss is , where is continuous in on , measurable in , and for each . A confidence level is fixed.
When jumps across at , the tail distribution keeps only the part of that atom needed to give the tail total mass one: the atom is split.
For each : is finite and convex (hence continuous), and
the minimum being attained and the argmin a nonempty closed bounded interval; in particular .
A companion item states Corollary 7: , strictly when .
Theorem 10 is what makes CVaR computable and optimizable. Since , minimizing CVaR over is the joint minimization of over ; with a finite scenario set and a loss linear in , that is a linear program, and VaR comes out as a by-product. The convexity and sublinearity of CVaR in (Corollary 11), its coherence (Corollary 12) and the equivalence of CVaR-constrained and CVaR-penalized problems (Theorem 14) are all derived from it. The formula is the basis of CVaR portfolio optimization software and of a large literature on risk-averse stochastic programming.
The result has been proved since 2001 and is not open. To our knowledge it has no machine-checked proof with CVaR defined independently: the CVaR items already on Prove2Me take as the definition of CVaR, which makes (28) true by definition. This mission produces a formal proof that the tail-mean definition, with its atom splitting, agrees with the minimization formula for every integrable loss, together with reusable facts about one-sided derivatives of and the argmin of the Rockafellar–Uryasev function.
The minimization side is elementary convex analysis in one variable once the one-sided derivatives are known; computing them requires passing a limit under the expectation, with the jumps of handled separately for right and left limits. The step that does not follow from that analysis is the identification of the minimum value with . When the loss has an atom at that straddles level , neither nor equals the minimum value; only the mean of the distribution with the split atom does. The obvious approach, proving the formula for continuous laws and passing to a limit, does not deliver the identity at the level of the defined objects; the identity has to be proved directly from the definition of the tail distribution, through Proposition 6.
Fin m → ℝ) with its Borel σ-algebra and a probability measure P. The paper's support set is not modelled: a law on is a law on concentrated on , and no statement uses .P.real). is , as the paper defines it in (2).MultistageStochastic.valueAtRisk P (f x) β (a real infimum, referenced, not redefined); is a real infimum. Both are meaningful because is a probability measure and , and those hypotheses are carried wherever they appear.Defining CVaR as , or as the quantile average, or by formula (21), would make the goal or a milestone true by definition; CVaR is defined here as the mean of the -tail distribution, and any such redefinition is ruled out.
A complete development needs: right-continuity and limits of distribution functions, dominated convergence for the difference quotients of , the uniqueness of a probability measure on with given distribution function, and one-variable convex analysis linking one-sided derivatives to minimizers. The derivative and argmin lemmas are reusable for any Rockafellar–Uryasev-type objective. Proofs of any milestone, and Lean lemmas that bridge valueAtRisk (stated with ENNReal) and P.real, are welcome.
A correlated equilibrium (Aumann, 1974) is a probability distribution over the strategy profiles of a game such that no player gains by deviating from the strategy it recommends. It is the natural solution concept for repeated play by adaptive agents, because the set of correlated equilibria is a polytope described by linear inequalities and, as Hart and Mas-Colell showed, it can be reached by simple learning rules that use only a player's own past payoffs and regrets.
Hart and Mas-Colell's paper (Econometrica 68 (2000) 1127–1150) has two procedures. Its Main Theorem concerns regret matching (2.2), in which a player switches away from its last strategy with probabilities proportional to its regrets; it is the subject of a companion mission. Section 3 studies a variant in which, at every period, the player plays an invariant vector of the regret matrix, and proves with Blackwell's approachability theorem (Blackwell, 1956) that the player's regrets vanish almost surely, whatever the other players do. This result, Theorem A, is the target of this mission. It is the conditional ("internal") counterpart of Hannan's no-regret property (Hannan, 1957) and the template for later internal-regret algorithms in online learning (Cesa-Bianchi and Lugosi, 2006).
Timeline. Hannan (1957) gave a procedure with vanishing unconditional regret; Blackwell (1956) proved the approachability theorem and derived a universally consistent procedure from it; Foster and Vohra (1997) obtained convergence to correlated equilibria through calibrated forecasts; Fudenberg and Levine (1995, 1999) introduced universal consistency and calibrated smooth fictitious play; Hart and Mas-Colell (2000) gave Theorem A and regret matching.
A finite game has a finite set of players, a finite nonempty strategy set for each player, and payoffs on . For and , is 's payoff when 's coordinate of is replaced by .
The game is played at . After the history each player chooses a mixed action, and given the players randomize independently. For in the regret of player for not having played whenever it played is
With , a probability vector satisfies (3.1) if
i.e. is an invariant distribution of the transition matrix of regret matching. The empirical distribution of play is .
If at every period player plays a probability vector satisfying (3.1), then, whatever the other players do,
The Corollary (p. 1134): if every player follows (3.1), converges almost surely to the set of correlated equilibria. The equivalence of (3.1) with invariance for the (2.2) matrix (p. 1133). Theorem B (p. 1139): the procedure proportional to unconditional regrets satisfies Hannan's universal consistency (4.1).
Theorem A shows that conditional regrets can be driven to zero by a stationary rule of fixed size , with no assumption on the other players beyond conditional independence. Combined with the Proposition of §3 it gives the Corollary: if all players follow such a rule, play converges to the set of correlated equilibria. The same argument with a different vector payoff yields Theorem B, a short proof of Hannan consistency. The approachability reduction used here is the standard route from vector-valued games to no-regret learning.
Theorem A and Blackwell's theorem are proved results. What this mission adds is a machine-checked development: a formal statement of Theorem A for arbitrary opponents, a formal statement of Blackwell's procedure in Hart and Mas-Colell's form (condition (3.2) via the support function, opponents that see the whole history), and the algebra connecting the two. Prove2Me already has Blackwell's original THEOREM 1 (strategies depending only on past payoff vectors, geometric separation condition); it is a different statement, and deriving this one from it, or proving it directly, is part of the work.
The algebra (milestones 1–5) is finite-dimensional and elementary, apart from the existence of an invariant vector, which needs a fixed-point or Perron–Frobenius type argument for a matrix that is not stochastic. The probabilistic core is milestone 6. The geometric picture of the paper (Figure 1) shows that the expected next average payoff moves closer to , but that controls only , not the realized averages (footnote 15 of the paper); the opponent adapts to the whole history, so the increments are neither independent nor identically distributed, and the almost-sure statement has to be obtained on a measure known only through its conditional laws given each history.
stdSimplex. is EuclideanSpace ℝ L with its inner product and Euclidean distance.play τ is ); every regret quantity is a function of a finite history Fin t → S, and every statement uses histories of length .IsLUB/¬ BddAbove.Useful infrastructure, reusable beyond this mission: the existence of invariant vectors of nonnegative matrices, projections onto orthants, and a general Blackwell approachability theorem for history-dependent opponents. Proofs of any milestone, of the companions, and alternative proofs of Theorem A are welcome.