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?
The path of a light beam changes when the transparent material through which it travels moves. This matters when interpreting light bending and phase shifts around a flowing liquid, and when asking whether a dielectric can imitate some effects of curved spacetime. Leonhardt and Piwnicki gave a geometrical-optics treatment of a moving, nondispersive dielectric and related its ray dynamics to a spacetime metric in their 1999 paper. This mission isolates their statement that light rays are null geodesics of that metric. Their treatment also connects this geometric picture to a Hamiltonian, a Lagrangian with an artificial mass, and a raised wave vector tangent to the ray. The physical model assumes that the refractive index and flow change gradually over an optical wavelength and cycle; the mission starts with the resulting local optical data rather than claiming an error estimate for that approximation.
A nondispersive dielectric has a refractive index that is independent of optical frequency. Let denote the vacuum speed of light, and let be the velocity of the material at an event, with . The paper uses . The four-flow is , where ; spacetime coordinates are with . The flat metric is .
Gordon's optical metric has contravariant and covariant matrices
The second matrix is the inverse of the first in the physical regime §III.B–C, equations (31), (42)–(43). A wave has laboratory frequency and spatial wave vector ; its covariant wave vector is . The eikonal null equation becomes the dispersion relation . The paper solves it for its positive comoving-frequency branch and defines the laboratory ray velocity . A ray parametrized by laboratory time has tangent , since §III.B, equations (28)–(36).
The goal is the existing Open platform theorem QAlgorithms.Papers.Independent.Renew46.P42.rays_nullGeodesic, posed from §III.D, equations (50)–(51). For a twice continuously differentiable optical patch with and subluminal flow, and a ray satisfying both Hamilton equations with , it asserts at every point of the ray
The scalar allows laboratory time to be a nonaffine parameter. The goal also includes the local-rest-frame identity
where takes a displacement from the medium's rest frame to the laboratory frame. The milestones follow the paper's path: the polarization-independent wave symbol, the dispersion polynomial, the Hamiltonian and its comoving light speed, the inverse metric, the massive action, the rest-frame line element, the zero proper time of the ray tangent, and the tangent relation for the raised wave vector. Three of these are new draft statements; the remaining five are published platform references. The rest-frame milestone is the pointwise form of the goal's second conjunct.
The result identifies the same rays through two descriptions: Hamiltonian trajectories in a moving dielectric and null curves of a Lorentzian optical metric. It fixes which metric acts on covectors and which acts on tangent vectors, and it makes the rest-frame speed visible in the line element. These identifications support the paper's later discussion of phase shifts and vortex flows §IV. Without the null-geodesic link, those later geometric analogies have no stated connection to the ray Hamiltonian.
The formalization work is still open even though the paper's result is known. The platform already has the shared definitions and six relevant theorem statements: three milestones are Proved, while the Hamiltonian characterization, the massive-action result, and the null-geodesic goal are Open. This proposal adds three local statements around equations (33) and (51) and the vanishing proper time. It does not duplicate the existing Open goal. A complete checked development would connect the local identities to the differential-geometric conclusion for rays in varying media.
The pointwise null identity is shorter than the geodesic conclusion. A ray velocity is a gradient of a Hamiltonian containing square roots, and its coordinates are defined only on the nonzero wave-vector branch used here. The full goal then has to relate Hamilton's time-parametrized equations to the Levi-Civita acceleration of a metric whose coefficients vary with position and time. A pointwise null calculation alone does not establish that the covariant acceleration is parallel to the tangent. The distinction between a covector and its raised vector , together with the spatial minus sign in , is essential: using the wrong variance changes the dispersion relation and the tangent statement.
The Lean model uses real coordinate vectors indexed by Fin 3 and Fin 4, real matrices, and the published module QAlgorithms_Papers_Independent_Renew46_P42. Its functions gUp, gDown, fourFlow, waveCovector, lorentzBoost, rayDispersion, rayHamiltonian, and rayVelocity are shared by the goal and every new draft. quadratic comes from the module's published dependency. The boost is the identity at zero flow. The ray tangent is in coordinates . Positive comoving frequency selects the Hamiltonian branch; laboratory frequency itself need not be positive.
The conditions , , and make the physical regime explicit. The zero-proper-time milestone also requires , where the Hamiltonian gradient represents a ray direction. The optical patch in the goal has an open domain and twice continuously differentiable index and flow. The ray has the stated regularity and satisfies both Hamilton equations on an open time set. The local null milestone has nonempty physical instances, rather than relying on a junk square-root value or zero wave vector. The curve-level goal is a universal implication and is vacuous when its open time set is empty. The paper's phrase about minimizing proper time is treated as a local null and pregeodesic claim, without a global minimizing assertion for Lorentzian length.
Reusable contributions include coordinate lemmas for the two Gordon metrics, Lorentz boosts, differentiation of the ray Hamiltonian, and the relation between Hamiltonian motion and covariant acceleration. The wave equation's slow-variation approximation, polarization transport, curvature formula, and vortex applications lie outside this mission's target.
Semidefinite programs that arise in coding theory, extremal geometry, crossing-number bounds and polynomial optimization are often too large to solve directly, but they are invariant under a large symmetry group. Restricting the matrix variable to the invariant matrices loses nothing, and the invariant matrices form a matrix ∗-algebra. The survey of Bachoc, Gijswijt, Schrijver and Vallentin (arXiv:1007.2905, published in the Handbook on Semidefinite, Conic and Polynomial Optimization, Springer, 2012) organizes this symmetry reduction into steps. Its Step 2 (§1.2, pp. 5–7) replaces an SDP over such an algebra by an SDP over a few small blocks, and the justification of that step is a single structure theorem: every matrix ∗-algebra is ∗-isomorphic to a direct sum of full matrix algebras (Theorem 1.2, restated as Theorem 2.7 on p. 13).
The theorem is classical. It is the finite-dimensional case of the structure theory of C∗-algebras (Davidson, C∗-Algebras by Example, Chapter I.10), and in the unital, non-star form it is the Wedderburn–Artin theorem for semisimple algebras over ℂ. Its use in SDP symmetry reduction goes back to Gatermann and Parrilo (2004) and de Klerk, Pasechnik and Schrijver (2007). Section 2.5 of the survey gives a short, elementary, self-contained proof using only linear algebra; this mission follows that proof.
A matrix ∗-algebra (Definition 2.1, p. 10) is a complex linear subspace that is closed under matrix multiplication and under the conjugate transpose . It need not contain the identity matrix, and it may be .
A map between matrix ∗-algebras is a ∗-homomorphism (Definition 2.6, p. 13) if it is linear, satisfies and ; a bijective ∗-homomorphism is a ∗-isomorphism. The direct sum is the algebra of block-diagonal matrices with diagonal blocks of sizes (p. 10).
The proof uses the following vocabulary (p. 13). The center of is . The unit of is the unique with for all . is simple if it is non-zero and . For a partition , is the zero-one diagonal matrix with ones in the positions of .
For every matrix ∗-algebra there are and and a ∗-isomorphism
The goal fixes no sizes: it asserts only the existence of the block structure, which is the form Step 2 uses.
Milestones 7 and 8 together give the goal.
The result. A ∗-isomorphism preserves positive semidefiniteness, so Theorem 2.7 turns the constraint ", " into independent constraints on blocks of sizes , with . This is what makes the Lovász ϑ-number of symmetric graphs, the Delsarte and Schrijver bounds for codes, and the crossing-number bound of de Klerk et al. computable at scale (§§4–6 of the survey). Without it, an invariant SDP still has a variable of the original size .
Formalizing it. The theorem is proved and textbook material; it is not open. As far as a search of the platform shows, it is not formalized in this form: Mathlib has Wedderburn–Artin for semisimple unital algebras over an algebraically closed field, which yields an algebra isomorphism but neither the star structure nor the non-unital case, and the platform holds a proved matrix-units statement for unital ∗-subalgebras (HarlowTASI.fdStarAlgebra_exists_matrixUnits, attached to this mission as a reference). The mission adds the non-unital ∗-isomorphism, the simultaneous unitary diagonalization of a commutative matrix ∗-algebra, and the intermediate facts of the elementary proof, each stated in a reusable form.
Two points make the obvious routes insufficient. First, a matrix ∗-algebra need not contain the identity: its unit is a projection onto a subspace, and the coordinates in carry no part of the algebra. Statements and arguments that start from a unital subalgebra do not apply without first cutting the algebra down to the range of its unit. Second, an algebra isomorphism onto a product of matrix algebras is not enough: the isomorphism must commute with the conjugate transpose, since positive semidefiniteness is defined through it. Abstract Wedderburn–Artin provides the first kind of isomorphism, and turning it into a ∗-isomorphism requires choosing the matrix units compatibly with the adjoint, which is where the content of the theorem lies. The elementary proof avoids ring theory entirely but has to control every off-diagonal block , which is the role of observations (i)–(iii).
NonUnitalStarSubalgebra ℂ (Matrix (Fin n) (Fin n) ℂ); Mathlib's star on matrices is the conjugate transpose. The index set is Fin n (0-based).StarAlgEquiv ℂ (≃⋆ₐ[ℂ]) on the subtype of : additive, multiplicative, ℂ-linear, star-preserving and bijective, exactly Definition 2.6.(k : Fin d) → Matrix (Fin (m k)) (Fin (m k)) ℂ with pointwise operations and star; it is ∗-isomorphic to the block-diagonal algebra (Matrix.blockDiagonal'). is allowed and is needed for .S : Fin n → Option (Fin k), with none for and some i for ; the paper's block is represented by the full-size product .The goal is not to be read with a unital StarSubalgebra (that adds the hypothesis and is the case already covered by the reference item), with an AlgEquiv that ignores the star, or with a mere linear equivalence (which exists for dimensional reasons and has no content). Each of these would trivialize or weaken the statement.
Useful infrastructure, reusable beyond this mission: simultaneous unitary diagonalization of commuting normal matrices, the unit and the central decomposition of a non-unital finite-dimensional ∗-algebra, and an explicit ∗-isomorphism from a corner algebra onto . Proofs of any milestone, and alternative routes to the goal (for example through Mathlib's Wedderburn–Artin plus a star-compatibility argument), are welcome.
A reverse convex set is the part of a polyhedron that lies outside an open convex set: , where and is open and convex. Such sets arise whenever a model forbids a convex region: integrality (a lattice-free convex set contains no feasible point in its interior), bilevel programs, where the points with for a convex value function are infeasible, and nonconvex quadratic or polynomial constraints. Optimizing over calls for valid inequalities for its closed convex hull.
The classical tool is the intersection cut of Balas (Balas 1971): starting from a basic solution of the linear relaxation that lies inside , one follows the extreme rays of the basis cone until they leave , and the exit points define a valid inequality. Towle and Luedtke study the opposite case, where the basic solution lies outside the closure of . Then the rays of the basis cone may enter , cross it, or never leave it, and no single inequality captures the structure. They replace the cut by a disjunction: a finite union of simpler sets that contains , to which the disjunctive programming machinery of Balas can be applied. The present mission targets their multi-term disjunction (Theorem 5 of the paper), which uses the full recession cone of .
Let have full row rank and . A basis splits the variables into basic variables and nonbasic variables , with a tableau and a basic solution ( for ) such that holds exactly when for all . Dropping the sign constraints on the basic variables gives the basis cone
a translated simplicial cone with apex and extreme rays (): , for , and for the other nonbasic .
The recession cone of is . Along each ray, the halfline , , meets in an interval with endpoints
in the extended reals, with , when the halfline misses . This sorts the nonbasic indices into (the ray misses ), ( finite and positive, : the ray enters and stays) and (: the ray crosses ); write . For extended reals and a vector , the segment is , and , are defined likewise. The paper builds the inner approximation of
and the sets
Throughout, , and (Assumption 2 of the paper) .
With ,
The relaxation of is thus a disjunction of terms.
Theorem 5 turns the nonconvex set into a finite union of sets with explicit generators. By the paper's Theorem 2, has the same closed convex hull as , so valid inequalities for the disjunction are valid for the reverse convex set and lose nothing in the limit. The paper then relaxes each term to a polyhedron (§4.4), and a cut-generating linear program over the union separates candidate points; when is bounded the disjunction collapses to the two-term disjunction of the paper's Theorem 1. The disjunction is therefore the bridge between the geometry of (its recession cone and the exit parameters along the basis rays) and polyhedral cut generation.
The result is proved in the paper (arXiv:1901.02112v5, pp. 17–18; Mathematics of Operations Research, 2022). It has no machine-checked proof. Formalizing it checks the extended-real conventions for , the treatment of empty and unbounded segments, and the role of the recession cone, all of which the paper handles in prose. The definitions of the basis cone, the exit parameters and the recession cone are reusable for other intersection-cut results on the platform.
The inclusion is immediate from the definitions. The reverse inclusion is the substance: a point lying in every term comes with unrelated representations, one per term, each using different segment parameters, a different multiple of and a different recession direction. A point of needs a single representation with all segment parameters inside and no negative multiples of the rays. A naive average of the representations keeps the negative components along the rays , so it does not land in . The rewriting of in Proposition 5 also needs care: it replaces by inside a convex hull, and absorbs the rays of into the recession cone, which holds only because is open.
Vectors are functions on a finite index type (the paper's ). The basis is the published Disjunctive.GeneralDisjunctions.IsTableau (a genuine tableau of , with a partition and ) together with , and the extreme rays are the published Disjunctive.GeneralDisjunctions.extremeRay. is defined, as on the page, by the tableau equations and . The exit parameters are EReal-valued infima and suprema over real parameters, so the empty set gives and and an unbounded set gives ; segments quantify over real compared with extended-real endpoints. are filters of , and . The index of is encoded by stating the term separately from the terms , . The recession cone is the universal-quantifier cone, which is the whole space for ; in that case every set in the goal is empty or and the identity is .
All hypotheses are the paper's: open and convex, of full row rank (§2), (§3), and Assumption 2 (§4). One generalization: the basic solution need not be feasible ( is not imposed); the paper's own Example 2 uses an infeasible basic solution and the proof of Theorem 5 does not use feasibility.
Real-valued (where an empty or unbounded parameter set returns ), segments with endpoints converted to reals, or an encoding in which is always empty would trivialize the statement; the extended-real definitions rule these out, and a sorry-free check confirms that the hypotheses are satisfiable with (one variable, ).
The development needs Minkowski sums and convex hulls of unions in , recession cones of open convex sets, and a Farkas-type alternative (for Lemma 2); the platform's LinearOptimization.farkas_lemma is available. Proofs of the milestones in any order are welcome; Lemma 2 is self-contained.
A creator-side experiment on a short-video platform may assign treatment to individual videos while measuring outcomes over a viewer's whole session. A treated video can alter what the viewer watches next, so its effect may persist beyond the immediate reward. The paper studies this form of interference using a Markov decision process and asks how well data from a per-video experiment estimate the effect of treating every video instead of none. Its motivating application is an experiment at Douyin, where viewer state includes attention and other factors that need not be observed by the estimator. Farias et al., 2023 give an estimator based on reward-to-go and a quantitative bias bound for an absorbing-session model.
The distinction matters for experimental design: the usual inverse-propensity estimate weights only the reward received immediately after an assigned action. In this setting it can omit the effect of that action on later rewards. The paper's Differences-in-Qs (DQ) statistic instead weights the remaining reward in the session after each assignment. The mission focuses on the theorem that quantifies the resulting bias in the finite absorbing model of Sections 3–5.
Let be a finite state set and let the actions be control and treatment . An action has a stochastic transition matrix and conditional mean reward . The initial state has probability law . A stationary policy assigns action probabilities at each state; its induced transition matrix is . Global control always selects , global treatment always selects , and the experiment independently selects each action with probability one half at each step. Thus .
A path consists of successive state-action pairs . Its law begins with , draws each action from , and then draws from . The total expected reward is . The target average treatment effect is .
The session has a common absorbing class : under each policy of interest, transitions from this class stay in it, and its mean rewards vanish. Assumption 1 bounds the expected number of steps spent outside that class, from every initial state, strictly by . These conditions make the infinite total-reward quantities meaningful. The paper writes a stronger absorbing-row equation that does not define a stochastic row when the class contains more than one state; the formalization uses the closed-class interpretation and records the discrepancy for review.
For a path from the half-treatment policy, the DQ estimator assigns weight or to the reward remaining after each treatment or control action, respectively. With the path stopped at , write that statistic as . The infinite-horizon expectation is defined through the limit of its finite-path expectations, not through a value-function identity.
The goal is Theorem 1 of Farias et al., in the absorbing regime. If every row of has total-variation norm at most and , then the estimator expectations converge to and
The milestone targets include the matrix resolvent identities of Lemmas 1–2, Theorem 2's finite-order expansion of the total-reward value functional, and Corollary 1's absorbing-case remainder bound. They also identify trajectory reward with the value functional and connect the trajectory DQ statistic to the first-order expansion. The listed order follows these mathematical dependencies. The mission does not assert Theorem 2's discounted, average-reward, or finite-horizon cases, which the goal does not need.
The bound distinguishes the DQ estimator from an immediate-reward estimate: its bias is at most quadratic in the row distance , with explicit dependence on expected session length and reward magnitude. It gives a criterion for when a per-video experiment can approximate the all-treatment versus all-control effect despite changes to later states. This is a statement about expected estimator bias; it does not by itself give a variance or finite-sample confidence bound.
The formal development separates three objects that are easy to conflate: the statistic computed from a trajectory, its expectation under the experimental policy, and a value-functional expansion used to analyze that expectation. The matrix identity corresponding to Lemma 1 is already machine checked on Prove2Me as MarkovEntanglement.resolvent_identity. The goal and other mission statements are compilation-checked drafts with proof obligations still open. A completed formalization would establish their convergence and equality claims as well as the printed bias constant, and would leave reusable finite-state path and absorbing-value definitions.
The immediate-reward estimate evaluates outcomes under the experimental state distribution, while ATE compares outcomes under two different state distributions. Weighting each current reward cannot generally account for that mismatch. The DQ statistic incorporates reward-to-go, but its infinite double sum must be related to a convergent trajectory expectation before any bias inequality applies. The central quantitative issue is to control how changing a policy perturbs the total-reward functional across repeated transitions, with the exact scale. A direct comparison of one-step rewards alone does not yield that order.
States and actions are finite. Transitions are nonnegative and row-stochastic, the initial law is a probability vector, and policies are stationary probability kernels. The goal's actions are Fin 2, with treatment and control. Path expectations are finite sums; infinite expected rewards and Q-functions use real series. The absorption-time condition asserts convergence with HasSum and a strict bound from every state. Its closed-class, zero-reward conditions apply under , , and . The reward field records conditional means, sufficient for the expectation claims.
Here is the row norm . The paper does not define its normalization; with the alternative half- convention the printed Theorem 1 constant fails. This choice is part of the statement, not a hidden rescaling. The truncated estimator is formed from path rewards exactly as equation (4) prescribes; defining its expectation as the first-order expansion would erase the mission's main identification step. The paper's Section 5.3 display also places the outer value functionals at and , while its claimed identity and Theorem 2 require ; the milestone states that corrected reading and retains the printed display in its provenance.
Useful contributions include convergence of finite-path expectations, the absorbing total-reward resolvent theory, and the exact finite-order remainder estimate. These definitions and lemmas can also support other finite absorbing policy-evaluation problems.
Quadratic hedging chooses a self-financing trading strategy that minimizes the expected squared difference between its terminal value and a payoff ; with constant it becomes mean–variance portfolio selection. The classical theory works in discounted prices: one asset is a risk-free numeraire, and optimal strategies are written in terms of the remaining assets (Černý and Kallsen 2007; the paper refers to Schweizer's 2010 encyclopedia entry Mean–variance hedging for an overview). Černý, Czichowsky and Kallsen drop that assumption. In their market no asset need be risk-free, and they want formulas for the optimal strategy that do not depend on which asset is used as the unit of account (arXiv:2110.09416v4, §1).
In their feedback formula (Theorem 4.1, p. 15) the optimal strategy is built from two processes. One is the adjustment process , which corrects the hedging error accumulated so far. The other is the pure hedge , which offsets the fluctuations of the claim's value process. At each time both are minimizers of a finite-dimensional quadratic problem with one linear budget constraint. The covariance-type matrix in that problem may be singular, for instance whenever a risk-free asset is present. So the minimizers are not unique and ordinary matrix inversion does not describe them. Theorem 4.3 of the paper (p. 16) gives explicit formulas for the whole solution sets, and Appendix A (pp. 24–28) proves the linear algebra behind them. That linear algebra is a general result on affinely constrained quadratic minimization with singular data, built on the oblique-projector analysis of Černý 2009.
Fix a time and a state. The data of the pointwise problem are:
Portfolios are row vectors and price-type quantities are column vectors, as in the paper (§2, p. 6). is the column space and the null space of a matrix. Every matrix exponent in the paper denotes the Moore–Penrose pseudoinverse: the unique with , , , (p. 24, (A.2)). The two problems are
where an is the set of all global minimizers over the whole hyperplane (possibly empty). With and the paper defines
The general problem of Appendix A is to minimize over with , where and .
and , .
In attack order: existence and uniqueness of the pseudoinverse (published, proved); Proposition A.1 (pseudoinverse rules); Proposition A.3 (affinely constrained least squares); (A.8) and ; (A.14)–(A.15); the completed square (A.16); Theorem A.4(1) (bounded below iff ); A.4(2) (all minimizers are with of minimum norm); A.4(3) (value identities); Lemma A.5; A.4(4) (formulas (A.6)–(A.7) through the oblique projector onto along ); and the range fact used in the proof of Theorem 4.3.
Theorem 4.3 gives closed forms for both ingredients of the optimal hedge. It covers markets with and without a risk-free asset in one formula, because and are the only two cases. In the second case is a fully invested portfolio with zero instantaneous variance. The paper uses them in its efficient-frontier analysis (§5) and its examples (§6). Theorem A.4 does not depend on finance. It gives a complete solution of a positive semidefinite quadratic program with linear equality constraints: when it is solvable, the full set of minimizers, and the minimum-norm minimizer. Its proof needs nothing beyond finite-dimensional linear algebra.
The paper proves all of these results. Proposition A.3 is taken from Černý (2009), and v4 (7 July 2025) strengthened Proposition A.3 and Theorem A.4 after the journal version (doi:10.1287/moor.2023.1374). The mission cites only v4. None of the statements has a machine-checked proof. The Penrose predicate and Penrose's existence and uniqueness theorem are already on Prove2Me as proved results. Mathlib at the pinned revision has no Moore–Penrose pseudoinverse, so the pseudoinverse calculus built here can be reused.
With a singular , completing the square with an inverse is not available. On the affine set, the quadratic part can vanish in some directions while the linear part keeps decreasing. The boundedness criterion has to detect exactly these directions. Under that criterion, a formula has to describe every minimizer, not just one stationary point. The constraint brings in the projector , and need not commute with it. As a result, the relevant projector is oblique, not orthogonal, and the obvious guess plus a correction fails. Exhibiting one feasible point with zero gradient does not prove the set equality, the minimum-norm property, or the case formulas (A.7). The case needs its own treatment through .
Fin d → ℝ with ⬝ᵥ, and matrices are Matrix (Fin m) (Fin n) ℝ. A row vector times a matrix is written x ᵥ* M and a matrix times a column vector M *ᵥ x, matching the paper's printed order. Column and null spaces are LinearMap.range/LinearMap.ker of Matrix.toLin'.LocalDistanceNetwork.IsMoorePenroseInverse (the four equations (A.2)). Because the pseudoinverse exists and is unique, this is the same as "the" pseudoinverse. Lean's ⁻¹ is used only on real scalars, never on a singular matrix.Matrix.PosSemidef, which includes symmetry. Argmin sets range over the whole affine set or hyperplane. Minimum norm compares squared Euclidean norms over the whole set.An investor can improve a portfolio by adding a zero-cost combination of long and short positions. Ordinary arbitrage asks whether such a combination pays nonnegatively in every outcome and positively in some outcomes. That test is restrictive when payoffs have both gains and losses. Arvanitis and Post instead ask whether one overlay portfolio raises expected utility for every admissible risk preference and every benchmark portfolio in a specified class. This gives an asset-pricing question that acknowledges uncertainty about investors' preferences and starting positions. The authors use the concept to study factor portfolios and transaction costs in their 2022 working paper Ordering Arbitrage Portfolios and Finding Arbitrage Opportunities (AUEB Department of Economics Working Paper 04-2022), published as Generalized Stochastic Arbitrage Opportunities in Management Science in 2024.
The target is the paper's Theorem 2.3.1, an existence condition for a pricing system. The working-paper statement needs a finite-generation condition on the utility class for its converse. The resulting mission records the corrected theorem and the general direction that does hold for arbitrary admissible utility classes.
There are finitely many base assets, indexed by . Their one-period payoff vector is with probability law , supported on for finite . A benchmark position costs . The benchmark set is closed and bounded; it can contain many portfolios and need not be convex. An overlay is feasible when , where has rows. Thus is the bounded overlay polytope, and is the passive choice.
The utility class contains continuously differentiable, strictly increasing, strictly concave functions . It is convex and uniformly bounded on bounded payoff intervals. For an overlay , the expected utility increment relative to benchmark is
A strict stochastic arbitrage opportunity is a single feasible overlay that improves every benchmark for every admissible utility. The set is
The paper's candidate stochastic discount factors are . A factor assigns the present-value vector to the base assets. The relevant polar cone is written in the paper's constraint coordinates as . This representation encodes the overlay inequalities and their shadow prices.
For the paper's general convex class , the existence of a mixture of marginal-utility discount factors whose present value lies in rules out every strict stochastic arbitrage opportunity:
If is the convex hull of a finite set of admissible utility functions, the converse is also claimed:
This is the mission's goal. The benchmark set remains any closed bounded set satisfying the budget restriction. ### Supporting milestones
The milestones follow the proof of Theorem 2.3.1 (pp. 34–35): the first-order (Karush–Kuhn–Tucker) condition for optimality on the segment , ,
the concavity bound ; the convexification step (9)–(10) in its pointwise form; the minimax reversal (10)–(11) and the linear-programming duality (11)–(13), both available as proved platform theorems; and the general pricing implication above.
The condition translates absence of a portfolio improvement shared by all the specified investors into the existence of a discount factor with constrained asset values. In markets with transaction costs, the cone can permit price intervals rather than one exact price vector. This connects an investor-facing arbitrage test to restrictions that can be checked through the market's linear constraints. The working paper (§2.3, p. 11) discusses that interpretation and its factor-investing application.
The result is a published mathematical claim but, in this representation, still a Lean proof obligation. A formal development would produce reusable definitions of strict utility-based arbitrage and marginal-utility pricing, plus machine-checked proofs of the valid pricing implication and the corrected converse. The two general minimax and linear-duality results referenced here already have proved Prove2Me statements; the paper-specific statements in this mission are draft goals and have no machine-checked proofs yet.
The converse has a quantifier problem: no single overlay can improve every utility and benchmark, even though different utilities may reject different overlays. Treating one failed endpoint comparison as a first-order optimality condition does not resolve that problem. In fact, a concave expected-utility function may end below its starting value at while initially increasing as leaves zero. The paper's proof makes that invalid identification. Its unrestricted utility class also permits limiting behavior that defeats the asserted converse. The finite-generation condition in the goal prevents that particular failure while retaining a nontrivial family of preferences and a general compact benchmark set.
Lean uses Fin N → ℝ for payoffs and portfolio positions, a probability measure for , and Bochner integrals for expectations. The almost-sure box-support condition makes the utility and marginal-utility expressions integrable under the stated continuity assumptions. The matrix inequality defines directly; is the paper's representation, rather than an abstract inequality definition. The set of discount factors allows every positive scale and takes the ordinary finite convex hull. The utility derivative is deriv u, justified by the continuously differentiable assumption. Lean's lo and hi name the support endpoints and aVec names the constraint right-hand side; the paper uses for both roles.
The corrected goal's finite generation of is an explicit addition to the printed Theorem 2.3.1. To see the need, take one riskless payoff , a second payoff with equal probabilities, one benchmark , and overlays for . A convex class generated by increasingly steep, smooth, strictly concave utilities has no strict SAO, yet every candidate marginal-utility discount factor at that benchmark is a positive constant and assigns positive value to the second asset, outside .
The SAO predicate remains the actual difference of two expected utilities. Defining it through the derivative inequality would erase the principal economic question. Supporting work may establish bounded-support integration, finite-dimensional compactness, convex-hull behavior, and the relation between the matrix cone and the overlay inequalities; these are reusable for other one-period pricing models. A result that only assumes the pricing restriction, or changes the benchmark set to a singleton, does not settle this goal.
Many problems in combinatorial optimization, control and signal processing reduce to minimizing a nonconvex quadratic form over a box. Max-cut and other boolean quadratic programs are special cases. Computing the global minimum of such a program is NP-hard in general, so the practical question is how well a tractable convex problem can bound it. The semidefinite relaxation replaces the rank-one matrix by an arbitrary positive semidefinite matrix . It can be solved to any accuracy in polynomial time by interior-point methods, the subject of the preceding chapters of Ye's Interior Point Algorithms (Wiley 1997).
The quality of this relaxation has a short history. Goemans and Williamson (J. ACM 1995) showed that rounding a relaxation solution with a random hyperplane recovers at least of the maximum cut. Nesterov (Optim. Methods Softw. 1998) showed that for a positive semidefinite objective over the relaxation is within a factor , with no definiteness assumption needed for a bound on the range of the objective. Section 9.5 of Ye's book extends this range bound to quadratic programs with quadratic equality constraints and box bounds, and with an arbitrary symmetric objective. This mission formalizes that section.
Fix , a symmetric real matrix , a real matrix with rows , and . Vector inequalities are componentwise and is the all-ones vector.
The quadratic program is
It is assumed feasible. Its maximum is .
Write , , for the diagonal of , and for the diagonal matrix with diagonal . The relaxation (9.48) is
with . Its dual (9.49) maximizes subject to and .
For with columns , the sign rounding (9.50) is . Here , applies for and otherwise to each component, and is uniformly distributed on the unit sphere of . For a function of one variable, is the matrix with entries .
The statement is deterministic. Its only hypotheses are that is symmetric and that the quadratic program is feasible.
Theorem 9.33 says that the range of a convex problem solvable by interior-point methods approximates the range of a nonconvex NP-hard program within the fixed factor . This holds for any symmetric objective, in the presence of quadratic equality constraints. Theorem 9.35 converts the bound into a randomized algorithm. One rounding of the relaxation solution gives a feasible point whose expected objective lies within a fraction of the range above the minimum. Repeated draws give such a point almost surely. The constant recurs throughout semidefinite approximation theory, from the Goemans–Williamson analysis to Grothendieck-type inequalities.
The platform already holds the Gaussian form of the arcsine identity (ConvexOptAlg.GoemansWilliamson.lemma_6_12), Grothendieck's identity, the Schur product theorem and Nesterov's positive semidefinite case (HighDimProb.RandomVectors.sdp_relaxation_approximates_max_cut). None of these covers quadratic constraints, the box, an indefinite objective, or the uniform-sphere rounding used here. A complete development would be the first machine-checked proof of a constant-factor semidefinite range bound for constrained nonconvex quadratic programming.
Lemma 9.31 is a matrix inequality between a nonlinear entrywise function of and itself. Entrywise functions do not preserve positive semidefiniteness in general, so the obvious attempt (a scalar inequality between and ) proves nothing about the matrices.
Lemma 9.30 and Theorem 9.32 need integration over the sphere. They need the probability that two hyperplane-sign coordinates disagree, which is a statement about the uniform measure on the sphere, not the Gaussian measure the existing platform results use.
The goal compares four optimal values, two of a nonconvex program and two of a semidefinite program, so it needs duality for the relaxation. The book's proof of Theorem 9.33 uses an optimal dual pair and positive definite feasible points of the relaxation. Neither is guaranteed under the stated hypotheses, and the theorem is claimed without them (see Beyond the paper).
Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ, indexed from . and are Mathlib's PosSemidef and PosDef, which include symmetry. and are real infima of the sets of feasible objective values. These sets are compact and, under the feasibility hypothesis every theorem carries, nonempty, so the infima are attained minima. The infimum in Theorem 9.32 is stated as IsGLB, so an empty set makes the statement false rather than trivially true. "Minimize" and "maximal value" in Lemma 9.30 and Proposition 9.29 are stated as a bound that is attained. The uniform measure on the sphere is Mathlib's surface measure volume.toSphere on the unit sphere of EuclideanSpace ℝ (Fin n), normalized to total mass one. Expectations are Bochner integrals of bounded measurable integrands, so the integral is the true expectation. is Mathlib's matrix inverse, used only at positive definite , where it is the true inverse.
Standing hypotheses of §9.5 that the book states once (p. 325) are explicit hypotheses of every theorem: symmetric and the quadratic program feasible. No positive definite feasible point and no dual attainment are assumed in the goal. In Proposition 9.29(ii) the two clauses that name are stated for every optimal dual pair, since the book names such a pair without establishing that it exists; the maximality of is stated outright. In Theorem 9.35, division is real division, so the case , where the book's quotient is undefined, reads . No appears in this section, and every constant is the book's own: , , and .
The theorem cannot be trivialized by an empty feasible region or a junk infimum. Feasibility is a hypothesis, the optimal values are attained minima of nonempty compact sets, and replacing the box or the quadratic constraints by an easy special case is ruled out by the definitions.
A complete development needs: the Schur product theorem and power series of entrywise functions of positive semidefinite matrices; the uniform measure on the sphere and its rotation invariance; and conic duality for the relaxation. The sphere and arcsine results are reusable well beyond this mission. Contributions on any milestone are welcome.
Beyond the paper. One variant is posed, qp_min_arcsin_infimum_corrected (kind: corrected). It is Theorem 9.32 with the added hypothesis that the relaxation has a positive definite feasible point. As printed, Theorem 9.32 fails for , , , : there every feasible has , while . Two further findings are recorded without variants. The dual (9.49) need not attain its optimum, and the proof of Theorem 9.33 relies on both assumptions while the statement holds without them.
Interior-point methods for linear programming generate a sequence of strictly positive primal-dual points that converges to the optimal set but never reaches it. The simplex method, by contrast, stops at an exact optimal vertex. Practical solvers and sensitivity analysis both need an exact answer: which variables are positive at optimality, and what the exact optimal solution is. The question of finite termination, of when an interior iterate carries enough information to recover an exact solution, was settled in the early 1990s (Ye 1992, doi:10.1007/BF01581087; Güler and Ye 1993, doi:10.1007/BF01580610; Mehrotra and Ye 1993, doi:10.1007/BF01585180).
Chapter 5 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley, 1997, doi:10.1002/9781118032701) presents the answer for real data. It works under the real-number model of computation, where the data are real rather than integers of bit length . Once the duality gap of a well-centered iterate is below a threshold set by a condition number of the data, the comparison identifies the strict complementarity partition exactly. That happens after a number of iterations polynomial in , and . The chapter also bounds the arithmetic cost of an iteration through rank-one updating (§5.1).
Let be a real matrix with , , . The standard-form pair is
Vector inequalities are componentwise. A triple is an interior point if , , , .
The strict complementarity partition is defined as follows: is the set of indices with for some optimal , and is the set of indices with for some optimal . When optimal solutions exist, these two sets partition (Goldman–Tucker; the book's Theorem 1.14). The optimal faces are
The condition number (5.3) is
It is how far the optimal faces reach into the open orthant. For an iterate let .
An interior-point sequence has property (5.7) with constant if for every , i.e. it stays away from the boundary relative to its gap. It satisfies the polynomial bound with constant if , where (the chapter's standing assumption, p. 147).
For §5.1, given positive iterates , the rank-one updating scaling is defined by , and if , else . The update set collects the indices that were reset at iteration .
For every interior sequence with property (5.7) and the polynomial bound,
The mission also references Proposition 5.5 (skew-symmetric self-dual programs are self-dual with optimal value zero), already proved on the platform as SelfDualLP.Complexity.proposition_1.
Theorem 5.3 shows that an interior-point method has a finite, data-dependent termination time. After iterations the partition is known. Projecting the iterate onto and the dual face then costs one least-squares solve and yields an exact optimal pair (§5.2.2). The iteration count depends on the data only through , not on a bit length. This is what makes the result meaningful under the real-number model. Lemma 5.1 is the counting step behind the saving in arithmetic operations: the number of rank-one corrections to the normal matrix is controlled by the scaled movement of the iterates.
None of these results is on the platform. The homogeneous self-dual results of §5.3 are already posed there from the Ye–Todd–Mizuno paper and are not re-posed. A formal proof would give the first machine-checked statement linking the duality gap, centrality and the optimal partition. That link is reused in the analysis of predictor directions (Chapter 7) and in basis identification.
The arithmetic of the proof is short; the difficulty is in the linear-programming facts it rests on. First, the existence of a strictly complementary pair, so that and cover all indices and are disjoint. Without it, cannot even be concluded on the indices outside both sets. Second, the optimal faces must be shown nonempty and bounded whenever an interior point exists, so that the maxima in are attained and positive. Third, the orthogonality must be derived for feasible pairs. A newcomer's first idea is to argue from convergence of the iterates to a limit point. That gives no iteration count, and the theorem needs the quantitative threshold instead.
For Lemma 5.1 the obstacle is the telescoping of across updates. The book's final step writes , but the bound needs .
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ, with indices starting at . The Euclidean norm is written out as norm2 because Mathlib's norm on Fin n → ℝ is the sup norm. Optimality is defined by comparison with every feasible point. and are defined as unions of supports of optimal solutions; no Goldman–Tucker property is assumed. Each maximum in is Lean's sSup over the face; xi_pos asserts that it is attained. is one minimum over all indices, taking the primal maximum on and the dual maximum elsewhere. Property (5.7) is written coordinatewise.
Explicit constants replacing the book's : Theorem 5.3 writes and appeals to the polynomial bound of the algorithms. The Lean statement makes that bound a hypothesis, with the algorithm's constant ; the per-step reduction implies it. The threshold from the proof then gives . The standing assumption (p. 147) and interior feasibility are explicit hypotheses. Because , property (5.7) can only hold when . It never holds at , so the theorems are vacuous there, as in the book.
A trivializing formalization is ruled out: is an explicit function of , not an existential "for some ", and is computed from , not a free parameter.
The update set of §5.1 is printed with in the numerator, which makes it empty for every . The mission defines it with , as the proof of Lemma 5.1 uses it (finding F2).
Needed infrastructure: LP weak duality and Goldman–Tucker strict complementarity (both proved elsewhere on the platform for other encodings), boundedness of optimal faces under interior feasibility, and attainment of linear maxima on compact polyhedra. The definitions module YeIPA.WorstCase.Termination (partition, faces, ) is reusable for Chapter 7's asymptotic analysis.
Not in scope: Theorem 5.14 and Lemma 5.15 (the infeasible-starting algorithm; Lemma 5.15's proof is an exercise and overloads ), Theorem 5.9(i) (its uniqueness claim needs of full row rank, finding F1), and the remaining §5.3 homogeneous self-dual results, which are posed on the platform for the paper's special starting point.
Primal–dual interior-point methods are the standard polynomial-time algorithms for linear programming. They do not walk along the vertices of the feasible polyhedron as the simplex method does. They follow a smooth curve through its interior, the central path, toward the optimal set. Every complexity bound for these methods is a statement about iterates kept close to that curve. Their practical value, recovering an optimal basis or the optimal partition of the variables, depends on where the curve ends.
Chapter 2 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, DOI 10.1002/9781118032701) develops the geometry behind these methods. It covers analytic centers of polytopes, potential functions, and, in §2.5, the central path of a linear program and its limit. The limit result is due to Güler and Ye and to McLinden (Güler and Ye, Mathematical Programming 60, 1993; McLinden, Pacific Journal of Mathematics 88, 1980). The central path converges to the analytic center of the optimal face, a strictly complementary optimal solution singled out among all optimal solutions. This mission formalizes that theorem (Theorem 2.17), with the boundedness and neighbourhood results (Theorems 2.17 (i), 2.18) that accompany it.
Let be a real matrix of rank with , and . Ye's standard-form primal and dual linear programs are
Vector inequalities are componentwise. A point is interior feasible if, in addition, (resp. ). It is assumed throughout that both programs have interior feasible points. A feasible is optimal if for every feasible ; a feasible is optimal if for every feasible .
For , a central path point is a triple of interior feasible points with
Theorem 2.16 says that it exists and is unique.
A pair of feasible and is strictly complementary if and for every . Such pairs exist (Goldman–Tucker, Theorem 1.14 in the book), and the supports and do not depend on the pair. is the strict complementarity partition. The primal optimal face is , and the dual optimal face is . The analytic center of the primal optimal face is the point of the face with that maximizes . On the dual side, the slack of the dual optimal face maximizes over the face.
With , the neighbourhood of the central path is
where , is the all-ones vector, and is any norm, or the one-sided "norm" , that dominates (every norm does).
For any choice of central path points , , there are and an optimal with
optimal for (LP), the analytic center of the primal optimal face, and the analytic center of the dual optimal face.
The goal identifies the end point of the central path: not an arbitrary optimal solution, but the unique strictly complementary one at the center of the optimal faces. This yields the optimal partition in the limit. It underlies finite termination and basis-identification procedures and the asymptotic analysis of later chapters, where predictor directions are measured on and . Theorem 2.18 extends the picture from the path to the neighbourhood that path-following algorithms actually maintain, with an explicit rate, , at which coordinates in the optimal partition stay away from zero.
The results are classical and proved in the literature. None is formalized on Prove2Me. Theorem 2.16 is already there, as a proved statement for Matoušek and Gärtner's equivalent max-form LP. The formalization adds machine-checked statements of the limit theorem, which so far exists only in prose, together with a precise record of which hypotheses each part needs. Reading the chapter turned up three: Theorem 2.17 (ii) is false as printed when an objective is constant on its feasible region; boundedness of the -component in Theorem 2.18 (i) needs of full row rank; and the "any norm" in the definition of is too permissive for Theorem 2.18 (ii).
The limit is taken along a curve defined only implicitly, as the solution of a nonlinear system for each . The obvious argument, compactness of the bounded path, only produces limit points. It says nothing about uniqueness of the limit or about which optimal solution is reached. The difficulty is that the claim pins down a single point among the typically infinitely many optimal solutions, and it must do so for any selection of path points, with no continuity of assumed. The book leaves the proof of Theorem 2.17 (ii) as an exercise and gives no proof of Theorem 2.18.
Vectors are Fin n → ℝ and Fin m → ℝ; is Matrix (Fin m) (Fin n) ℝ; indices run over . Every theorem carries the chapter's standing assumptions explicitly: and (p. 48), and interior feasible points for both programs (pp. 63, 70). The central path enters the goal as an arbitrary selection of central path points for ; no continuity is assumed, and limits are taken along . and are constructed from the data, as the indices positive in some strictly complementary pair. The optimal faces are written for full vectors in , and analytic centers are attained maximizers of , never a supremum. takes the size function as a parameter, and Theorem 2.18 is stated for every with ; the book allows "any norm, or even a one-sided norm", and with an arbitrary norm (say ) the lower bounds of 2.18 (ii) fail. There are no constants in these statements; the bound of Theorem 2.18 (ii) is the book's exact constant.
A trivializing formalization would take , or the limit points as free parameters constrained by hypotheses, or define the analytic center through a real supremum that defaults to . Both are ruled out: the partition and the faces are computed from , and the analytic center is an attained maximizer over points with positive coordinates.
Beyond the paper. Two variant items are posed beside the faithful ones. [Corrected] Theorem 2.17 (ii) replaces both strict inequalities by weak ones, because the strict ones fail when or is constant on its feasible region, e.g. , , (findings F1, F6, F8). [Sharpness probe] Theorem 2.18 (i) drops : with a zero row in a coordinate of is free and the set is unbounded (finding F7); a disproof is the sought outcome.
A complete development needs strong LP duality and the Goldman–Tucker strict complementarity theorem for standard-form LPs, strict concavity of on a polyhedron, and compactness arguments in . The duality and complementarity layers are reusable across the whole series; contributions of these as standalone lemmas are welcome.
Empirical risk minimization (ERM) is the inductive principle behind most of statistical learning: a learning machine picks, from a set of functions, the one with the smallest average loss on the training data, in place of the one with the smallest expected loss under the unknown distribution. Whether this substitution is justified is the first question of learning theory, and Chapter 2 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) answers it.
The history is short. Vapnik and Chervonenkis gave the entropy criterion for uniform convergence of frequencies to probabilities in 1968 and published the proof in 1971 (Theory Probab. Appl. 16, 264–280); in 1981 they extended it to uniformly bounded real functions (Theory Probab. Appl. 26, 532–553); in 1989 they proved the key theorem, which reduces consistency of ERM to uniform one-sided convergence. The book states all of these results without proofs (Preface, p. xi); the proofs are in Vapnik, Statistical Learning Theory (Wiley 1998) and the cited papers.
Let be a probability measure on a measurable space , and let , , be a set of real functions on indexed by an arbitrary parameter set . The risk of is . For an i.i.d. sample drawn from , the empirical risk is . Probabilities are taken under the product measure .
For let . The ERM method is nontrivially consistent (from p. 38 on simply "consistent") if for every with nonempty,
Removing the functions of smallest risk rules out consistency that is caused only by a single function lying below all the others. Uniform one-sided convergence means for all (2.4). Uniform two-sided convergence is the same with (2.6).
For a set of bounded functions , the random VC entropy is the logarithm of the size of a minimal -net, in the metric (maximum over the sample points), of the vectors . The net is internal: its points are themselves vectors of the set. The VC entropy is . For indicator functions, is the number of distinct binary vectors on the sample. From it the book defines the entropy , the annealed VC entropy , and the growth function .
If for all , then
Only the risks are bounded, not the functions. The constants and are arbitrary, and they appear only in the hypothesis.
VapnikChervonenkis.Entropy.theorem4_entropy_criterion and is referenced here.The key theorem says that consistency of ERM is decided by the worst function of the set, in the one-sided sense of (2.4). Every analysis of ERM must therefore control a supremum over the whole set, a worst-case analysis (p. 39). This turns the question of consistency into the question of uniform laws of large numbers. Theorem 2.3 and its corollary answer that question through the VC entropy. The three capacity concepts underlie the "three milestones" of §2.7: consistency, a fast rate of convergence, and distribution-free guarantees. These are also the objects of the later missions of this series.
The platform already has the 1971 indicator-class criterion (Proved) and the related entropy-rate lemmas for event classes. It has no real-valued loss class with a parameter set, no notion of nontrivial consistency, no key theorem, and no VC entropy built from -nets of real functions. This mission supplies those definitions with the book's conventions, and states the key theorem and its neighbours as open targets.
The theorem is an equivalence between a statement about infima over the shrinking families and a statement about one supremum over all of . Neither the functions nor the empirical risks are bounded; only the risks are. The empirical infimum over may therefore be , and no compactness of is available. Single-function laws of large numbers control each separately, but they do not control the supremum: for an infinite they are not enough, and that is the content of the chapter. For Theorem 2.3, the necessity direction is a genuine probabilistic argument about the growth of covering numbers, and the measurability of suprema over an uncountable must be handled explicitly.
All declarations are in the namespace NatureSLT.Consistency. The parameter set is an arbitrary Lean type and . A sample of size is Fin ℓ → Z under Measure.pi (fun _ => F), and a probability is a value of that measure in . The risk is a Bochner integral, and every theorem that uses it assumes each integrable. Logarithms are natural. The minimal -net is internal and uses the metric , as in the book's footnote 3; it is not Mathlib's external covering number. "Monotonically decreases" (p. 50) is read as non-increasing.
Suprema of deviations and the infimum of empirical risks over are taken in the extended reals, so they are genuine values and never a junk default. The infimum of the risks is a real infimum over a nonempty , which is bounded below by . No extended-real subtraction occurs: the event is written as or .
The book's "some (technical) conditions of measurability" are explicit hypotheses. In Theorem 2.1, and are measurable functions of the sample. In Theorem 2.3, , , the half-sample deviation and the random VC entropy are measurable. For indicator classes, is measurable.
A trivializing formalization is ruled out. Consistency is the nontrivial notion (2.3), quantified over every nonempty , not the classical one that a minorizing function satisfies trivially. The probability of a non-measurable event is never read as : Lean evaluates it as an outer measure.
Beyond the paper. One strengthened variant is posed, key_theorem_strong (finding F1). It is Theorem 2.1 with the two measurability hypotheses removed and probabilities read as outer probabilities. The known argument needs only monotonicity and finite subadditivity of the probability of events, together with the weak law of large numbers for a single integrable function, so measurability is never used.
Contributions are welcome on any item. Reusable beyond this mission are the risk and empirical-risk definitions, uniform one- and two-sided convergence, and the VC entropy of a real class. Theorems 2.2 (maximum likelihood), 2.4 (one-sided convergence through minorant classes), 2.5 and 2.6 (nonfalsifiability) are not part of this mission.
A bandit sampling process models a population from which values are drawn one at a time: the values are independent with a distribution whose parameter is unknown, the decision maker holds a prior on and updates it by Bayes' theorem, and each draw earns a reward. When several such populations compete for the same sampling effort, the Gittins index theorem reduces the allocation problem to computing one index per population (Gittins, J. R. Stat. Soc. B 1979). The obstacle is computation: the state is a posterior distribution, so the index is a function of every parameter of the posterior.
Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), shows that location and scale structure removes most of that dependence. For a normal population with unknown mean and variance, Theorem 7.15 says that the index in the state is , so a single function of suffices; the tables of Chapter 8 rest on this. The same reduction holds for target processes, where the aim is to observe a value above a target as soon as possible (Theorems 7.19–7.23).
This mission continues the public series Multi-armed Bandit Allocation Indices I–VI in the namespace AllocationIndices. Mission VI formalized the location and scale halves of the theory (Theorems 7.9 and 7.11) and the location invariance of target processes (Theorem 7.17), all now proved; this mission states the joint location–scale results on the same published definitions.
A sampling model SamplingModel Θ Q (published, AllocationIndices_Sampling) consists of a likelihood , a family of priors on indexed by the parameters of a conjugate family, and the update of those parameters when is the next value sampled; the family is conjugate on a set of parameters if the update computes the Bayesian posterior there. The reward process has state , draws from the predictive distribution , moves to , and earns the predictive mean . Rewards are discounted by , ; for a stopping time , is the expected discounted reward before , and is the Gittins index (2.6). The target process with target stops as soon as a sampled value is .
Two calibration quantities compare a process with a known one. The calibration payoff against a standard bandit process paying per period is
the supremum over all stopping times, being the time at which the standard process is first selected (calibrationPayoff). The target cost against a standard target process with known success probability is
where is the expected number of samples drawn before or before the target is reached, and the probability that comes first (targetCost, undiscounted, valued in ).
Parameters and are joint location and scale parameters if is the image of under for , . With unknown the conjugate prior on has parameters , which change by the rules of the sample mean, the sample standard deviation and the number of observations, and are joint location and scale parameters of the prior family: the prior with parameters is the image of that with parameters under . With known the parameters are and only change.
For the reward process with unknown, in a state with , , for all , and ,
Both conclusions are part of the goal (AllocationIndices.Targets.location_scale_invariance).
The result reduces the index of a two-parameter family of posteriors to a function of one variable and makes the normal reward process with unknown variance computable at all; the Chapter 8 tables of and the corresponding target-process tables are only meaningful because of it. The identities for and are what the calibration method of computing those tables uses, so they are stated too.
The theorems are proved in the book only in outline: the proofs of Theorems 7.13 and 7.15 are "left as exercises", and those of 7.19–7.23 are said to be similar to their reward-process counterparts. A formal proof supplies the arguments the book omits. Mission VI proved the one-parameter cases on the platform; the joint cases, the calibration payoff and the target cost have no machine-checked version.
The book reasons with densities and improper priors. In the formal model the state is a parameter vector, the posterior is Mathlib's Bayesian inverse, defined only almost everywhere with respect to the predictive distribution, and stopping times are measurable functions of an entire trajectory of states. Relating the processes started at and at requires relating two Markov chains on an uncountable state space, together with their stopping times, rather than two densities. The two index identities are also not formal consequences of the identities for and in the published model, whose index is defined as a supremum of reward rates rather than by calibration.
Discrete time throughout; uses the factor exactly as printed in (7.15), so no unit conversion is involved; the index is gittinsIndex (2.6) of the reward or target chain with , and is undiscounted as in (7.16). The book's improper priors ( uniform, ) are used only through the proper posteriors they generate; as in Corollaries 7.14, 7.16 and mission VI, the state is the parameter vector of a proper conjugate family, required to be conjugate on (σ known) or on , (σ unknown), the domain on which the sample-standard-deviation update is defined and keeps . "σ known" means the prior is concentrated on the scale coordinate of the state. The prior family's location–scale property is an image of measures; the printed density form (7.25) has a Jacobian where is needed and lacks the shift in the conditioning argument, so as printed no probability density satisfies it. The reward theorems assume integrable observations and finite expected discounted absolute rewards from every state, which makes a finite supremum over a nonempty set; this rules out the trivializing reading in which a real supremum of an unbounded set defaults to , and the goal states both the identity for and the index identity, not the reward shift alone. In Theorem 7.19 the index identity carries , which the book leaves implicit; in Theorem 7.23 the stray argument of is dropped.
Beyond the paper. The first identity of Theorem 7.21 scales and by but shifts without scaling it; with normal observations, , , , , , the two sides are at most and at least . The faithful item states it as printed; a corrected variant with is posed beside it.
Definitions are in AllocationIndices.Targets.Model; the model, conjugacy, reward and target chains, HasScaleParameter, PriorHasScaleParameter and meanUpdate are the published AllocationIndices_Sampling. Lemmas on transporting a Markov chain's path measure and its stopping times along a measurable bijection of the state space are reusable beyond this mission; proofs of single milestones are welcome.
Gittins index policies are optimal for a single server choosing among alternative bandit processes, and the achievable region method of Bertsimas and Niño-Mora (Math. Oper. Res. 1996) explains why: when the performance vectors of a scheduling system satisfy generalized conservation laws, the region they fill is a polytope whose optimal vertex is an index priority. Most real systems have several servers working in parallel, and for them the conservation laws fail. Glazebrook and Wilkinson (Ann. Appl. Probab. 2000) observed that parallel machines are close to a single machine working at times the speed, where the laws do hold, and turned that closeness into explicit bounds on how much an index policy can lose. Section 5.7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), presents that analysis for the simple family of alternative bandit processes (SFABP). Its first quantitative output is an upper bound on the optimal return, Corollary 5.20. This bound is the reference point against which the index heuristics of the rest of the section are measured.
This mission continues the public series Multi-armed Bandit Allocation Indices I–VI. Mission IV of that series formalized the single-machine achievable region theory of Chapter 5: Lemma 5.1, Theorems 5.5 and 5.10, and the identity of the adaptive greedy indices with Gittins indices.
There are arms. Arm has a finite state space ; the are disjoint, and their union is the set of job types. One transition kernel on moves an arm when it is processed. Each is closed under , and is irreducible on each . Time is discrete, rewards are discounted by with , and processing a job of type earns . There are identical machines, . At each time a policy chooses, on the basis of the history, a set of exactly arms. Each chosen arm makes one transition and the others are frozen. From the initial state-vector , the performance is the expected total discounted number of times a job of type is processed. The return is , and .
The matrix is the single-arm matrix of §5.3, published in the series as conservationCoeff: for , , where is the number of transitions the chain started at needs to return to , and otherwise. Job types are numbered in ascending order of the indices produced by the adaptive greedy algorithm (IsAdaptiveGreedy, greedyIndex), and . Write
Let be the number of arms with no job type in , let , and number the arms so that . For each other arm, is the processing needed to bring it from into for the first time, and is the sum of these over the other arms, which evolve independently.
The goal keeps the book's constants. Eq. (5.27) is a companion bound from the same identity.
The bound is explicit and computable from single-arm quantities: the AG indices and the laws of first-entry times. Subtracting from it the exact return of a concrete policy gives a certified suboptimality gap without solving the parallel-machine dynamic program, which has no index solution. The book uses it in exactly this way. With the exact return (5.30)–(5.31) of the heuristic , it shows that loses , and in the limit that is average-overtaking optimal (Theorem 5.25).
All of these results are proved in the book and in Glazebrook and Wilkinson (2000). None is machine-checked. The series so far covers only the single-machine theory, and there is no parallel-machine bandit model on Prove2Me. This mission supplies that model and states the first link of the chain: from conservation-law algebra to a bound for a system that does not satisfy the conservation laws.
The identity (5.25) is algebra once the policy processes exactly arms in every period. The difficulty is the lower bound on . The obvious idea, which works for one machine, is to minimize by giving priority to job types outside . On machines such a policy cannot keep every machine busy outside , and the minimizing policy is not known, so has no closed form and must be bounded below over all history-dependent policies at once. The bound has to hold uniformly: it must account for each arm's processing both before and after its first visit to , with arms frozen for random lengths of time in between. The printed proof also contains a step whose last inequality goes the wrong way (finding F2). The lemma is true, but the printed chain of inequalities cannot be followed literally.
Job types are Fin (N + 1), so the book's is Lean's N + 1 and the book's type is the Lean index i - 1. Sums over run over i : Fin N, with = ν i.succ, = ν i.castSucc and = Finset.Iic i.castSucc. The arms are Fin n, and arm : Fin (N + 1) → Fin n assigns job types to arms. One kernel on the disjoint union replaces the book's per-arm matrices , and IsArmFamily states closedness and irreducibility. A policy (ParallelPolicy n N M) is a sequence of Markov kernels from histories to Boolean selection vectors with exactly true entries. The law of the history is built by composition, and the performance is a discounted sum of expected per-period occupation counts. and are a real supremum and infimum over all policies. The class is nonempty because , and both families are bounded, so neither takes a junk value. is an integral against the product of the single-arm chain laws, with a real exponent and . The numbering by AG indices is two hypotheses: the identity permutation is an output of , and is monotone. The arm numbering is a function lowest with lowest b and lowest monotone.
Unit conversions: none. Section 5.7 is written in discrete time with discount factor , the convention of the series' published definitions, so every constant is the book's.
Correction of the setup: the book assumes "the number of parallel servers exceeds the number of arms " (p. 139). The rest of the section needs the opposite (finding F1): for instance, the arm index in Corollary 5.20 is not positive when . Every item assumes .
Trivializing formalizations ruled out: is not a hypothesis or an abstract GCL quantity. It is the infimum over an explicitly constructed, nonempty class of parallel-machine policies, so the goal cannot be discharged by assuming the conservation laws for the -machine system (which fail). The theorems do not allow , where the policy class is empty and the supremum would take the junk value .
Out of scope: the branching-bandit bounds of §5.5 (Theorems 5.12 and 5.13). They need a continuous-time branching-bandit model whose GCL property the book only cites. Also out of scope are Theorem 5.11 (priority classes) and the results 5.21–5.23 and Theorem 5.25.
Reusable infrastructure: the parallel-machine SFABP model (Def_AllocationIndices_Branching_Parallel) serves the remaining results of §5.7. Lemmas on the law of a frozen arm's trajectory under an arbitrary policy are welcome contributions.
A multi-armed bandit in the sense of Gittins is a sequential allocation problem: several independent Markov reward processes compete for a single resource, at each decision time exactly one of them is operated, and the goal is to maximize the expected total discounted reward. The Gittins index theorem says that it is optimal to operate, at every decision time, a process of largest index, where the index of a process depends only on that process. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), extends it to superprocesses, precedence constraints and arrivals.
In practice an index is rarely computed exactly. It is approximated numerically, or a heuristic policy is shown to be close to an index policy, so one needs to know how much reward is lost when a policy is only approximately an index policy. Section 4.10 of the book answers this for two notions of approximation. For ε-index* policies, which choose whole stages whose reward rate is within ε of the largest index, Corollary 4.16 bounds the loss by ε times the total discounted time. This mission formalizes Corollary 4.16 and the freezing-rule and promotion-rule lemmas of §4.5 on which its proof rests. The bound goes back to Katehakis and Veinott (Math. Oper. Res. 1987).
This mission continues the public series Multi-armed Bandit Allocation Indices I–VI in the same namespace, AllocationIndices, reusing its model and definitions.
A bandit process is a Markov chain on a countable state space with transition kernel . Each time the continuation control is applied it yields the bounded reward and moves one step; under the freeze control it stays put and pays nothing. Decision times are and rewards are discounted by with . For a positive stopping time of , and are the expected discounted reward and time before , , and the Gittins index is (the discrete-time index (2.6), gittinsIndex P r a x).
A freezing rule for is a nondecreasing sequence in , where depends only on . The reward of process time is postponed to time , and means it never accrues. Then
A stopping rule is the special freezing rule for and otherwise.
A simple family of alternative bandit processes is operated by a policy : at each decision time chooses, possibly at random and on the basis of the whole history, one process to continue, and the others are frozen. Its payoff is the expected total discounted reward, and . For a positive stopping time of the family's history, and are the reward and discounted time accrued before , and the index of the family is
An ε-index* policy proceeds in stages. At the start of a stage it chooses a process and a positive stopping time of 's own evolution with , all indices evaluated at the current states. It continues up to and then repeats.
For every ε-index* policy , every and every initial state-vector ,
The book states in continuous-time units; is the same bound in the discrete-time units of the index (2.6) (see Formalization scope).
where and are the reward and discounted time with no freezing.
5. Theorem 2.1 (p. 91, restated in §4.5), referenced: an index policy attains (BanditAlgorithm.gittins_index_theorem, proved on the platform).
Corollary 4.16 makes the index theorem robust. Any procedure that certifies, stage by stage, a reward rate within ε of the largest index is guaranteed a payoff within of optimal. Examples are a numerical index computation with error ε, or a heuristic whose stages are near-optimal stopping problems. At it is the statement that modified forwards induction policies are optimal. Lemmas 4.5–4.7 carry the freezing-and-promotion proof of the index theorem, which the book notes "comes into its own" for families that are not simple (§4.6–4.7, jobs with precedence constraints).
Status: the index theorem itself is formalized and proved on the platform (BanditAlgorithm.gittins_index_theorem). The companion bound for ε-index policies, Theorem 4.18 ( in the same units), is posed and open as AllocationIndices.eps_index_policy_near_optimal. Freezing rules, the family index (4.5) and ε-index* policies have no formal counterpart yet.
The obvious attempt is to repeat the interchange argument of Lemma 2.4 stage by stage. It does not work directly: an arbitrary policy interleaves the first stage of with portions of the other processes in a history-dependent way. Moving that stage to the front postpones the other processes' rewards by a random amount and advances 's rewards by another. Comparing the two needs inequalities that hold for every past-measurable postponement or promotion, not just for stopping rules. These are Lemmas 4.5 and 4.7. Lemma 4.6(i) is also needed, to bound the reward rate of the rest of the family by the largest index. The stage-by-stage losses then have to be summed over infinitely many stages, each started at a random time.
markovChainMeasure P x, trajectory stopping times (ℕ → S) → ℕ∞, gittinsIndex, stoppedReward, stoppedTime, stoppedRatio, IsPositiveStoppingTime, BoundedReward. Families use the published MarkovBanditPolicy k T and markovBanditDiscountedValue P r a π x: all bandits share one kernel P and reward r on a common state space, which by §2.9 is no loss of generality (disjoint unions). State spaces are countable with measurable singletons, and rewards are bounded (§2.4).markovBanditDiscountedValue over all MarkovBanditPolicys, a bounded set because rewards are bounded.Prove a block-sensitivity versus sensitivity separation exponent of 2.15.
Prove a separation exponent of 2.127294, building on Robin Kothari’s 2.075 construction and yousofy’s 2.105 proof with twelve nested predicates and sharper joint boundary bounds.
Recommendation platforms and online retailers choose which products to show a customer, and customers often buy more than one of them in a single visit. Classical choice models such as the multinomial logit (MNL) assume a customer buys at most one product, and under MNL the revenue-maximizing set of products to display is easy to find: it is one of the revenue-ordered sets, so it can be found in linear time. Tulabandhula, Sinha, Karra and Patidar (arXiv:2006.08055, Manufacturing & Service Operations Management, 2023) introduce the BundleMVL-K model, a multivariate logit model in which a customer buys a bundle of up to products, with pairwise interaction terms that capture complementarity and substitution. They estimate it on retail data and design algorithms for choosing the recommendation set.
The first question for any such model is whether the revenue problem stays tractable once purchases of two products are allowed. Theorem 1 of the paper answers it negatively: already for the unconstrained revenue problem is NP-complete. This mission formalizes that theorem and its proof, a reduction from Max-Cut.
The products are . Product has a revenue . A BundleMVL-2 instance assigns a nonnegative weight to every product and to every unordered pair of products, together with a no-purchase weight . (In the paper , and , so , is allowed.) A customer shown the recommendation set buys the nonempty bundle , , with probability , and buys nothing with probability . The expected revenue of is eq. (4),
With the indicator of , the weights , () and the revenues , (), both numerator and denominator are quadratic forms in .
The revenue problem (5) is ; its decision version asks, for a threshold , whether some has . SIMPLE MAX CUT asks, for a simple graph and an integer , whether the nodes of split into two parts with at least edges between them.
NP-completeness is in the sense of Cook's Definition 4: membership in NP and a polynomial-time many-one reduction from every NP language.
The result. Theorem 1 separates the multi-purchase model from its single-purchase counterpart: the revenue-ordered structure that makes MNL assortment optimization linear-time fails once pairs can be bought, and no polynomial-time exact algorithm exists unless P = NP. This is what justifies the paper's design of exact algorithms without running-time guarantees (a noisy binary search over the Compare-Step) and of polynomial-time heuristics, and it places BundleMVL-2 next to other hard assortment problems such as the mixture of two multinomial logits (Rusmevichientong et al. 2010, as cited by the paper) and the MMC model of Benson, Kumar and Tomkins (2018), whose hardness is the paper's Theorem 2.
Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. The paper's argument constructs the instance and asserts the equivalence; it does not argue NP membership or the polynomial running time of the reduction, and it leaves the revenues and threshold free subject to inequalities. A formal proof must fix concrete rational parameters, show that the instance code has polynomial size, and handle malformed inputs. The Compare-Step identity (milestone 2) is also the correctness lemma for the paper's binary-search algorithm.
The mathematics of the reduction is short; the obstacles are the two halves that the paper treats as evident. First, the reduction must be a polynomial-time computable map on strings, in Cook's one-tape Turing-machine model, that sends codes of Max-Cut instances to codes of BundleMVL-2 instances and every other string to a non-member; the rational entries must be computed and written in reduced form. Second, NP membership needs a polynomial-time verifier that evaluates exactly in rational arithmetic, with a bound on the bit size of the sums. An approach that states the reduction as "for every graph there is an instance with the same answer" proves nothing: a fixed yes- or no-instance does that.
The development is in MultiPurchase.Hardness. Conventions committed to:
Fin n, 0-based; in the reduction the hub is 0 : Fin (m+1) and graph node i : Fin m is product i.succ.ℚ). Weights may be zero (), as the paper's own reduction requires (); revenues are positive and . These well-formedness conditions are part of the yes-predicate.BSym, rationals as reduced numerator and denominator.The complexity layer is the published CookPvsNP_defs (Cook's , , , NP-completeness) and ProjSchedTW_Complexity_Encoding (binary codes, cutSize, maxCutLang), with the proved CookPvsNP.polyReducible_trans. Contributions welcome: Turing-machine programs for rational arithmetic and list manipulation (reusable for every NP-membership proof over rational data), the polynomial-time reduction, and a proof of Karp's theorem for SIMPLE MAX CUT, which would discharge the hypothesis.
Multiplying two -bit integers on a multitape Turing machine takes steps by the algorithm of Harvey and van der Hoeven (2021), and was long conjectured to be optimal. The OpenAI manuscript Integer multiplication below (September 2026) gives a machine running in time with , which beats by a factor that grows without bound. That theorem is now fully formalized on this platform: IntMul.Kappa.campaign_bound_inv_two_pow_182 is Proved, through the published development NLogN.KFTop.kappa_bound.
The manuscript calls its constants "deliberately conservative; no optimization is claimed." The community repository CrocSwap/integer-mult-bounds records which constants the same construction tolerates. Its patch frozen-154 keeps the original swap networks and recurrence exponents and changes only four constants of the final assembly, which raises the saving to . This mission formalizes that retuning.
Timeline of the saving for this construction:
frozen-154 patch: , with , , , and the same networks. Not yet formalized.A multitape Turing machine has a finite alphabet, finitely many states, a read-only input tape, an output tape and finitely many work tapes. On input with it must halt with the -bit binary expansion of on the output tape. Write . The proposition (from IntMul_MultitapeModel) says that one such machine is correct for every and runs in at most steps for all large .
The OpenAI machine processes inputs of length using the parameters , , (the number of axes of the transform), (the chunk width of the transform layout), and , where is least with and is the bit volume. Its running time divided by is bounded by the normalized cost table (Table 1 of the manuscript)
Each row is at most to a power below one. The seven margins below one are
and the saving is . At the manuscript's constants the minimum is . At the frozen-154 constants ( and unchanged) the minimum is , so .
The definition file IntMul_OpenAI_R154 fixes these constants, the table (named Ncost) and the parameter map dP, KP, ℓP, αP. It reuses , , , and from the published IntMul.OpenAI.Glue, since they do not depend on the constants.
This is the campaign template with value , stated over the campaign's foundation definitions.
frozen-154 parameters.The goal follows from milestones 3, 4 and 5 by a short argument.
The result itself. The bound improves the formally verified saving for exact integer multiplication on multitape machines from to , a factor of , without new mathematics in the networks. It also checks that the manuscript's construction is robust to its constants, which the manuscript asserts but does not exercise.
Formalizing it. The development hard-codes and in its parameter map (IntMul.OpenAI.Glue.dP, KP) and in the statements built on them. A development written against general constants, or a second instantiation, makes every later retuning cheap and separates what depends on the constants from what does not. Milestones 1 to 4 are short and mirror proved lemmas of the development. Milestone 5 is the substance.
The cost analysis is not where the difficulty lies; it is finite arithmetic with real powers. The difficulty is milestone 5: re-establishing the machine's time bound at the new and . A larger makes grow much faster with , and a larger makes the chunk width grow faster with . Every lemma whose proof used the old exponents numerically must be rechecked. These include the depth guard for the recursive layers, the bound on the simultaneous-layer exponent , and the requirement that the auxiliary gate counts fit in bits. Reusing the proofs verbatim fails wherever they rely on or specifically.
All statements use the Mathlib environment of the campaign (0df444a, Lean v4.33.1) and the machine model IntMul_MultitapeModel: a fixed finite alphabet and state set, one-way infinite tapes, a read-only input tape, and exact output . Real powers are Real.rpow. is IntMul.lg.
The machine milestone quantifies over one machine for all lengths. A machine that hard-codes answers for finitely many lengths still has to be correct everywhere and to meet the time bound for all large , so no finite table trivializes it. The polylogarithmic factor in milestones 4 and 5 matches the manuscript's statement that the slack "covers any remaining fixed power of ". It does not weaken the goal.
Contributions are welcome at every level: proofs of milestones 1 to 4, a parametric version of the Glue, KFM and KFV parameter lemmas, and sketches that split milestone 5 into the phases of the machine.
frozen-154. https://github.com/CrocSwap/integer-mult-bounds/blob/main/patches/frozen-154.patchNLogN.KFTop.kappa_bound and IntMul.OpenAI.Glue.kappaBound_of_machine (the formalized development).A supplier whose regular production can be disrupted must decide who bears the risk of a shortfall. Under a price-only contract the supplier promises the full order and covers any shortfall from a costlier, reliable expedited source; the buyer bears no supply risk but pays for the supplier's insurance through the wholesale price. Farahani, Dawande, Gurnani and Janakiraman (SSRN 3143238) study the supply-flexibility contract, under which the supplier may deliver less than the order, down to a guaranteed fraction of it that she chooses together with the price. The paper documents contracts of this kind in practice: coal supply in India with a commitment to deliver at least 80% of the agreed quantity, corn supply agreements with no penalty as long as 75% of the order is delivered, and minimum-volume provisions in printed circuit boards and fresh foods (§1, pp. 2–3).
The question is who gains. The supplier leads the game and can always offer zero flexibility, so she cannot lose. The buyer, by contrast, hands the supplier the power to pass disruption risk to him, and it is not evident that he is not hurt. The paper's main result says that, for log-concave demand, he is not: both parties are weakly better off. The price-only benchmark with supply risk extends the analysis of Lariviere and Porteus (2001); the disruption model with an expedited backup follows Tomlin (2006).
A buyer faces random demand with density , positive on an interval ( allowed) and zero elsewhere, with survival function and finite mean. He sells at a fixed retail price ; unmet demand is lost. A supplier's regular production costs per unit of input, and an input yields , where with . An expedited source delivers any quantity at cost per unit. Assumption 1 is . Assumption 2 is that the generalized failure rate is non-decreasing on .
Write for the guaranteed fraction. A contract obliges the supplier to deliver at least of an order . The game runs:
The supplier earns ; the buyer earns . Assumption 3: an indifferent supplier delivers the least quantity. With , the equilibrium is expressed through the solutions , , , of
equations (1)–(4) of the paper.
For every model satisfying Assumptions 1–3 with a log-concave density, both games have a subgame-perfect equilibrium, and for every equilibrium of the flexibility game and every equilibrium of the price-only game,
where , are the buyer's and supplier's expected equilibrium profits. The goal fixes no distribution and no parameter values; it asserts only the direction of the comparison.
The result separates two effects of flexibility. Lowering the guarantee lets the supplier cut the wholesale price, which raises the order and the total profit of the chain; the theorem says the buyer's share of that gain at least offsets the risk he takes on. Corollary 1 of the paper, that supply-chain efficiency is higher under the flexibility contract, follows directly. The paper's remark after Theorem 6 notes that the conclusion holds for uniform, normal, exponential, and Gamma and Weibull demand with shape at least one, which covers the distributions used in most newsvendor studies.
The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. A formalization adds three things. It fixes the equilibrium concept: the paper solves a "Stackelberg equilibrium" by backward induction and states it as unique, which fails in three edge cases (a zero price-only order, an irrelevant guaranteed fraction when the price exceeds or when , and a tie between two supplier strategies); the milestones state the corrected versions. It supplies the existence argument for (A2.8), whose proof the paper omits. And it checks a proof that differentiates the roots of (1)–(3) in the parameter , while the statement needs no differentiability of .
The supplier's half is a deviation argument. The buyer's half is not: the buyer's equilibrium profit depends on which of three regimes the supplier chooses (, or ), and in two of them he receives a smaller quantity with probability . Comparing truncated means at the roots of three different equations has no pointwise argument: the roots move with at different rates, and the comparison needs a shape condition on beyond Assumption 2. The paper uses log-concavity, and remarks that monotonicity of suffices. A second difficulty is the equilibrium itself: the supplier's problem in is not concave, and its recast form (A2.8) has a non-convex feasible set. Reading off the equilibrium requires solving every subgame, including off-path ones at prices below , where the supplier's production choice changes.
The model is a structure of reals , a density , and ; demand is Lebesgue measure with density , and is the published SupplyChainTheory.expSales. , and is the integral over . The disruption is a Boolean, with expectation . Log-concavity is the published ConvexOptimization.LogConcaveOn on all of , which allows to vanish off its support. The roots of (1)–(4) are not defined by choice; every theorem takes them as arguments with hypotheses stating that they solve the equations.
The equilibrium is subgame perfect: delivery is the least maximiser of the supplier's ex-post profit (Assumption 3), and production, order and offer are optimal at every admissible history, not only on the equilibrium path. The price-only game fixes . Two hypotheses are added to the paper's and disclosed: continuous on , so that (1)–(4) have solutions, and offers restricted to , without which the buyer's problem has no maximiser and no equilibrium exists (Lemma A2.1 shows the restriction changes no equilibrium).
A formalization in which the comparison holds trivially is ruled out: optimality is required off the equilibrium path, so threats cannot sustain arbitrary outcomes; the price-only game cannot choose a guaranteed fraction; delivery follows the least-quantity rule; and the goal asserts that equilibria exist, so the comparison is not vacuous. "Better off" is the weak inequality, since in some cases the two contracts give the same outcome.
A complete development needs truncated-mean and survival-function calculus for densities, uniqueness and continuity of the roots of const under IGFR, and comparative statics of those roots in . The IGFR root lemmas and the expected-sales identity are reusable across newsvendor-contract missions. Contributions to any milestone, and to these supporting lemmas, are welcome.
The price of anarchy (PoA) measures how much selfish routing costs compared with a coordinated optimum: it is the ratio of the cost of a Wardrop equilibrium to the minimum social cost. Worst-case bounds on this ratio are classical (Roughgarden and Tardos, JACM 2002; Correa, Schulz and Stier-Moses, Math. Oper. Res. 2004), and for polynomial costs of degree they grow with . Empirical studies of road traffic, however, observed that the PoA of real networks is close to 1 both in light and in heavy traffic (Youn, Gastner and Jeong, Phys. Rev. Lett. 2008; O'Hare, Connors and Watling, Transp. Res. B 2016). This mission concerns the theorem that explains the heavy-traffic half of that observation for a large class of cost functions.
Timeline:
A non-atomic congestion game has a finite non-empty set of groups, a finite set of resources, and for each group a finite non-empty set of strategies, each a non-empty subset of ; every resource belongs to some strategy (2.1). Each resource carries a cost function , non-negative, non-decreasing and continuous on .
Given a demand vector , a profile splits each over with . The load of a resource is , a strategy costs , and the social cost is . An NE profile uses only cheapest strategies of each group; an SO profile minimizes . The price of anarchy is
The total demand is ; a demand sequence is unbounded if . A game is asymptotically well designed (Definition 2.1) if for every unbounded demand sequence. A function is regularly varying (§1.2) if for every the limit exists and lies in .
If every is regularly varying, then for every demand sequence with and ,
Each resource may have its own regular variation index, and nothing is assumed about how the groups' demands grow relative to each other.
The paper's own route, in order:
The result shows that for every cost class in common use (polynomials with non-negative coefficients, the BPR functions of traffic engineering, logarithmic factors and their products and sums) selfish routing becomes asymptotically efficient as traffic grows, whatever the demand pattern. It replaces the growth conditions of earlier work by a condition on the cost functions alone, and its limit-game and decomposition framework is reusable for other asymptotic questions about equilibria. For BPR costs the paper further shows that every SO profile is an -approximate NE profile (Theorem 4.1); that refinement is not part of this mission.
The theorem is proved in the paper; none of it is machine-checked. The platform has the Wardrop layer (KellyStochasticNetworks_Wardrop) and fixed-demand PoA results, and KellyStochasticNetworks.wardrop_equilibrium_exists proves existence of Wardrop equilibria for globally continuous monotone delays, but nothing about limits of the PoA in the demand. A formalization would produce the first verified heavy-traffic efficiency theorem for congestion games, and check a proof whose central step (Theorem 3.2, Appendix A.3) is a six-page induction.
The natural first idea is to scale all costs by one common factor and pass to a limit game, as for gaugeable sequences. That fails when groups' demands grow at different rates: a single scaling makes the slower groups' contribution vanish or blow up, and the limit game then says nothing about their equilibrium behaviour. The paper therefore scales each class of comparable groups separately, and must show that interactions between classes through shared resources become negligible in the right order. Two further obstacles are specific: the limit cost functions take the value on resources that grow faster than the scaling, so the limit game lives in with the convention ; and the choice of scaling for a class in Appendix A.5 relies on the uniform behaviour of regularly varying functions (, Karamata's characterization, which Mathlib does not have).
The game is a structure with J resources, R strategies and Sd groups, a 0/1 incidence inc and a group map grp; profiles, loads and the Wardrop condition are those of the published definition KellyStochasticNetworks_Wardrop. Conventions fixed in Lean:
Game.Standing.ℝ≥0∞. Condition (L4) is encoded as: an NE profile of the limit game exists, and every NE profile has cost in and is an SO profile of the limit game.EReal.The goal does not mention limit games or decompositions: these appear only in milestones, so the goal cannot be satisfied by an encoding that builds the conclusion into a definition. Regular variation is not encoded as a power law or with a fixed index.
A complete development needs: existence and equal cost of Wardrop equilibria for costs continuous and non-decreasing on ; compactness of profile sets; uniform convergence of monotone functions to a continuous limit; Karamata's characterization theorem for monotone regularly varying functions. The last two are reusable well beyond this mission and are welcome as separate contributions.
A decision maker who asks several experts for the probability of a one-off event (an election result, a geopolitical outcome, a product launch) has to turn reported probabilities into one. Simple averages are known to be under-confident when the experts hold different information, and over-confident when they share noise. Model-based aggregators correct for this. The event is a one-off, however, so there is no history from which to estimate the model's parameters, and the aggregate has to come from a single cross-section of predictions. Satopää (SSRN 3769945, 2021; Operations Research 70(6), 2022, doi:10.1287/opre.2021.2224) answers this with a Bayesian aggregator whose prior carries no tuning parameters. That only makes sense if the resulting posterior is a genuine probability distribution. This mission formalizes the theorem that guarantees it.
A binary event is , where is a latent Gaussian variable. The common prior is , where is the standard normal distribution function and . There are forecasters. Forecaster holds evidence , and in addition irrational noise . They report ; the real number is the probit prediction, and .
Under exchangeability and Gaussianity, the model has three parameters : is the information each forecaster holds, the information two forecasters share, and the noise. The evidence has covariance matrix
where is the identity and the all-ones matrix. The parameter space is
The probit predictions are Gaussian, with . The likelihood is this density. The two eigenvalues of are
and the sufficient statistics are and .
The prior family is
It contains the Jeffreys prior , which is proportional to the square root of the determinant of the Fisher information , and the independence Jeffreys prior .
For every , , and with for some and ,
The statement holds for the whole family, not only for the two Jeffreys priors.
The result. An objective prior "may not have a finite integral and hence may not represent an actual probability distribution. Inference, however, is valid as long as the resulting posterior distribution is proper" (p. 16). Theorem 3.3 (iii) gives conditions on the data under which the likelihood tames the prior's mass near the boundary of : the forecasters do not all agree, and their mean probit differs from . The revealed aggregator of the paper is defined through this posterior, so its MCMC implementation and every application in §4 rest on this theorem.
Formalizing it. The result has a published, informal proof. No part of it has been machine-checked. The mission adds a machine-checked statement of the model (parameter space, likelihood as a Gaussian density, the prior family, the Fisher information) and of the steps the proof relies on. A complete solution also corrects a slip in the printed proof: the posterior display on p. 40 centres the predictions at , while the likelihood (6) centres them at . The formal statement uses the likelihood as defined.
The integral is over a three-dimensional region whose boundary is curved, , and the integrand degenerates in several directions at once: , , , and . A bound that treats the parameters one at a time fails, because the prior's singularity in is integrable only after the exponential factor in is used. That factor depends on through the mean, and the printed argument handles the dependence with a mis-centred posterior. Showing that the likelihood written with and coincides with its closed form needs the spectral structure of compound-symmetric matrices, which Mathlib does not package.
DKFAsymptotics.gaussianPDF.A formalization in which the likelihood is defined by the closed form (6), or in which the integral ranges over a bounded box, would make the goal a different and easier statement. The likelihood here is the Gaussian density, and the domain is all of .
A complete development needs:
The compound-symmetric matrix lemmas and the inverse gamma integral are reusable well beyond this paper. Contributions to either are welcome, as are alternative proofs of the goal.
Not formalized: Theorem 3.3 (ii), the independence Jeffreys prior, whose derivation drops cross-block factors inside its proportionalities. Its prior is still covered by the goal at . Also not formalized: Propositions 2.2 and 3.1, and the empirical §4.
Redundancy (sending several copies of a job to different servers and keeping the first one to finish) is a standard way to cut response times in parallel computing systems whose servers have variable speeds: replicated requests in data centres, speculative execution in MapReduce-type frameworks, duplicated queries in distributed storage (Vulimiri et al., CoNEXT 2013; Gardner et al., 2017). The price is extra work: while a job is present, all its copies occupy servers. The first question about such a system is therefore whether redundancy shrinks the set of arrival rates the system can handle.
For i.i.d. exponential copies and First-Come-First-Served service, Gardner et al. (Queueing Systems 2016) and Bonald and Comte (Performance Evaluation 116, 2017) proved that the stability region is , the same as without redundancy. Anton, Ayesta, Jonckheere and Verloop (arXiv:1903.04414, Operations Research 2021) studied other service disciplines and other correlation structures. Their first result, Proposition 3, extends to Processor Sharing and Random Order of Service. Their Example 1 shows that the extension fails for an arbitrary work-conserving discipline.
There are servers , each of capacity , and a redundancy degree . Jobs arrive in a Poisson process of rate . Each job chooses servers uniformly at random and sends one copy to each. The copies of a job have i.i.d. exponential service requirements of mean . When one copy completes, the other copies of that job are removed (cancel-on-complete).
A job's type is its set of servers . The set of types is , with , and . is the number of type- jobs and the number of copies at server . Two service disciplines are considered:
The system is stable when this Markov process is positive recurrent. The load is .
The statement contains no constant beyond the paper's threshold . That threshold cannot be improved: the total service rate is at most , so is necessary for every (p. 5).
The result. Proposition 3 shows that, with i.i.d. copies, replication costs no capacity under PS or ROS. Redundancy can then be used for its latency benefits at any load the non-redundant system can carry. The comparison with the rest of the paper shows what is at stake. With identical copies under PS the region shrinks to (Proposition 11). A priority discipline with i.i.d. copies can be unstable at (Example 1). The PS/ROS result is therefore not a consequence of work conservation.
Formalizing it. The result is proved on paper, and nothing of it is machine-checked. A complete formalization would check every step: a fluid-limit argument for a queue with simultaneous service at several servers, and the transfer from an empty fluid model to positive recurrence of a countable continuous-time chain (Robert 2003, Corollary 9.8, which the paper cites). The paper's argument also has two weak points that a formal proof must settle. Lemma 1 prints , which is false for (see below). The proof of Lemma 2 uses the PS departure rate (1) for ROS as well, where (1) holds only on average (p. 6).
The obvious argument is a Foster–Lyapunov drift for . It fails at finite states. The departure rate from a most-loaded server is at least only through the ratios , which are not monotone along the chain, and under ROS the instantaneous departure rate depends on which jobs happen to be in service, not on alone. The paper therefore passes to fluid limits. The drift (14) has to be identified for the limit of with (a differential inclusion, via Gast and Gaujal), and the negative drift at the maximum has to be turned into stability through a general fluid-stability theorem. For ROS, the averaging "a fraction of server serves type " must be justified at the fluid scale; the paper does not do this in the proof of Lemma 2.
Fin K; types are {c : Finset (Fin K) // c.card = d}; is lam.ProcessingNetworks.Stability definitions. Stability is their PositiveRecurrent: every state recurrent with finite mean return time of the continuous-time chain, holding times included. For PS this ranges over all of , which is one communicating class.A trivializing formalization is ruled out: the state spaces are infinite (a finite-buffer chain is positive recurrent for every ), the rates are the paper's (with an "all copies must finish" rule the threshold would be ), and the only load hypothesis is .
The development needs Poisson processes built from exponential sequences, a strong law of large numbers for them, Arzelà–Ascoli on , a Lipschitz/a.e.-derivative argument for the maximum of finitely many functions, and a fluid-stability criterion for countable continuous-time chains. The last three are reusable well beyond this mission. Contributions of any of these, and of the milestone lemmas, are welcome.
Firms increasingly outsource innovation to crowdsourcing contests: a firm posts a design or software problem, many independent solvers submit solutions, and the best one wins a prize. Platforms such as Topcoder, 99designs and Kaggle run thousands of such contests, and a recurring design question is whether a project with several attributes (say, a logo's shape and its colour scheme, or an algorithm's speed and its accuracy) should be run as one joint contest judged on the aggregate quality, or split into separate sub-contests, one per attribute, each with its own prize.
M. Hu and L. Wang, Joint vs. Separate Crowdsourcing Contests (Management Science 67(5), 2021, doi:10.1287/mnsc.2020.3683; accepted manuscript SSRN 2892683), answer this in a rank-order tournament model in the tradition of Lazear and Rosen (1981). Their Proposition 1 isolates two opposing forces. Separating the contests lets the firm combine the best realization of luck in each attribute, possibly from different solvers (the combination effect). Joining them concentrates the whole prize in one competition, which raises the effort solvers exert (the pooling effect). The rest of the paper (the luck-versus-effort thresholds of Propositions 2–3, the optimal prize, heterogeneous solvers) builds on this decomposition.
There are ex ante identical contestants. Contestant chooses an effort in each attribute , and her performance in attribute is , where the random factors are independent across attributes and contestants with a common density and cdf . The density is symmetric () and log-concave ( for , ). Effort in attribute costs , with and for .
Write for the density of , for its cdf, and for a quantile function. A contestant whose effort exceeds the common effort of the other by wins with probability
and the paper's key quantity is , with the same expression for .
With the maximum of independent copies, the difference of expected best performances splits as , where
and is the aggregate equilibrium effort of the joint contest. Assumption (R) asks for a with on and on .
(i) Under Assumption (R),
(ii) For interior symmetric equilibria of the sub-contests and , , of the joint contest,
and the condition may be replaced by when (a) , or (b) with convex derivative.
Proposition 1 is the structural result of the paper: every later comparison of the two mechanisms weighs against . Propositions 2 and 3 find thresholds on the noise scale and on the number of contestants at which the sign of flips, and Corollary 1 shows that for normal noise , so the joint contest elicits more effort whenever . The combination effect is also a statement about order statistics of independent sums that holds outside contests: the sum of the maxima of two samples exceeds, in expectation, the maximum of the sums.
The result is proved on paper; nothing in it has been machine-checked. The formalization adds a precise account of the equilibrium concept (global best responses against the expected payoff rather than first-order conditions), of the joint contest's two-dimensional strategies, and of the regularity condition the strict inequality needs. Reusable by-products are the quantile representation of the expected maximum and the differentiability of the rank-order winning probability, which recur throughout the tournament literature.
The weak combination inequality is pathwise and easy; the content of part (i) is strictness, which fails for degenerate noise and needs the quantile representation together with Assumption (R). Part (ii) rests on first-order conditions for equilibria that are only assumed to be global best responses: one must differentiate the winning probability, an integral of a power of the cdf, without assuming the density continuous (a uniform density jumps at the end of its support). In the joint contest the deviations are two-dimensional, and one has to show that an equilibrium pair is an optimal allocation of its own sum before the one-dimensional argument applies; the paper's Lagrangian derivation of differentiates an allocation map whose differentiability it never establishes.
Everything lives in the namespace CrowdContest.Pooling, in two definition files: Density (densities, symmetric log-concave densities, cdf, convolution, quantile, expected maximum) and Setting (winning probability, , costs, payoffs, equilibria, , , Assumption (R)). Log-concavity is the published platform definition ConvexOptimization.LogConcaveOn.
Committed conventions:
The goal is not trivialized by its encoding. The equilibrium efforts are characterized as global best responses against the expected winner-take-all payoff, not by first-order conditions. The first-order conditions (Lemmas 1 and 3) are milestones to be proved, not definitions. Part (i) is the strict inequality under (R), not the pathwise weak inequality of p. 16. The hypotheses of part (ii) can all hold: for , uniform on , , and , the efforts and are interior symmetric equilibria (both payoffs are strictly concave), with , and .
Needed infrastructure: differentiation under the integral sign for a convolution of an integrable function with a bounded one, the quantile transform for an atomless distribution, the boundedness and moments of log-concave densities, and infimal convolution of strictly convex functions on a half-line. All of it is reusable beyond this mission, and contributions of any of these pieces are welcome, as are proofs that a given distribution satisfies Assumption (R).
Sensitivity and block sensitivity measure two ways that a Boolean function can react to changes in its input. Both are basic measures in query complexity, where the input is accessed one coordinate at a time. Their relationship asks how much a function's response to changes involving several coordinates can exceed its response to individual coordinate changes.
Hao Huang's proof of the Sensitivity Conjecture established a polynomial relationship between sensitivity and polynomial degree in 2019, resolving the qualitative polynomial-relation question. The quantitative problem of obtaining the largest possible separation exponent remains the focus of this campaign. This mission asks for the specific exponent .
The relevant progression is:
A total Boolean function assigns an output bit to every input consisting of bits:
For an input and a coordinate set , write for the input obtained by flipping exactly the coordinates in . The sensitivity at an input counts the individual coordinates whose flip changes the output:
The block sensitivity at an input is the largest number of pairwise disjoint nonempty coordinate sets whose separate flips each change the output:
The two global measures maximize over all inputs:
There is no restriction to monotone functions, symmetric functions, or any particular construction. The number of variables may vary with the desired sensitivity threshold and approximation to the exponent.
Prove that for every real and every integer , there are a dimension and a total Boolean function such that
The shared campaign predicate SensitivityCampaign.AchievesExponent (2.10 : ℝ) expresses exactly this statement. The decimal denotes the exact rational number . The witnesses may depend on both and ; no fixed function is required to work for every threshold. The unbounded-threshold requirement is essential to the asymptotic separation being asked for.
A solution would strengthen the campaign's proved lower bound on the possible separation exponent from to . It would provide Boolean functions with arbitrarily large sensitivity and block sensitivity growing with the specified larger power, with an arbitrarily small loss in the exponent.
This is an open research target, rather than a request to transcribe an existing proof of . A complete contribution must establish the mathematical claim and provide a Lean proof using the shared definitions. Improvements to constructions, sharper bounds for existing constructions, and reusable supporting results are all relevant contributions. Acceptance of a proposal merely opens the target; a proof is needed to establish the new bound.
A successful construction must support many disjoint sensitive blocks while controlling sensitivity at every input. A large collection of block witnesses at one input supplies only part of the required information: the upper bound on sensitivity is global. Bounds that lose too much in this global analysis can erase the desired exponent improvement.
The available campaign infrastructure already includes proved theorems converting suitable finite certificates into the asymptotic conclusion. The unresolved work is to obtain stronger certified bounds on a construction, or to establish the asymptotic target directly. A numerical estimate of a separation exponent does not replace a proof of the inequalities on which that estimate depends.
Functions are represented as (Fin n → Bool) → Bool. Both complexity measures are natural-number maxima over finite sets; the comparison involving an exponent casts them to real numbers and uses real exponentiation. Since every requested witness satisfies , its power has a positive base. Zero-dimensional and constant functions cannot satisfy the sensitivity requirement.
The proposal retains the foundation definitions SensitivitySeparation and SensitivityCampaign. It also references two already-proved supporting theorems, rather than introducing alternative definitions or assuming any particular family of functions:
SensitivityCampaign.finite_certificate: bounds on sensitivity and block sensitivity at a chosen input, together with an exact power inequality, imply the campaign conclusion at the stated nonnegative exponent.SensitivityCampaign.finite_certificate_log: the same finite bounds certify the exponent given by the ratio of their logarithms.These statements are included as reusable foundation milestones. Their hypotheses require integer bounds greater than one, so the logarithmic denominator is positive. Solvers may use either criterion or prove the quantified target directly. The environment is Lean 4.33.1 with the campaign's pinned Mathlib revision.
Establish a separation exponent of at least between block sensitivity and sensitivity of total Boolean functions.
The target is an infinite family such that
Here tends to zero with . Sensitivity is the maximum number of individual coordinate flips that change the output at a common input; block sensitivity allows pairwise disjoint nonempty sets of coordinates instead. Both maxima range over all inputs.
The Lean goal uses the campaign’s shared definition: for every and every integer , there must be a total Boolean function with and . The decimal means exactly .
One sufficient route is a finite function , an input , and integers satisfying
The proved theorem SensitivityCampaign.finite_certificate then gives the asymptotic conclusion. Direct family constructions are equally welcome.
The starting milestone is the campaign’s proved exponent . The target is a challenge to prove, not an established campaign record. Further background and construction parameters appear in the campaign proposal.
Quantum algorithms can reduce the work needed for some computations, but a provider also has to build hardware capable of serving a market. Bova, Goldfarb, and Melko model these two costs separately in Quantum Economic Advantage. Their question is whether a quantum provider can choose more market-creating investment than a classical rival even when building that additional quantum capacity is more expensive. The answer matters to their economic comparison: a lower variable cost does not, by itself, order the firms' investment decisions.
The working paper was circulated as NBER Working Paper No. 29724 in February 2022 and appeared in Management Science in 2023. This mission cites the NBER version throughout. It addresses the paper's Proposition 2, its explicit numerical witness, and the model results used around that proposition. The paper proves these results analytically; the remaining task here is a machine-checked formalization of their statements and proofs.
There are two firms. Firm 1 supplies quantum computing and has constant unit cost ; firm 2 supplies classical computing and has unit cost . A common demand intercept measures the initial market size. The paper assumes . The firms sell differentiated computing services, with substitution parameter : at their products do not compete through demand, while at they are identical in the model. This is an economic representation of quantum advantage, rather than a formal model of a quantum algorithm. See §2 of the working paper.
In stage 1, firms simultaneously choose investments . Firm pays , where , and its investment raises its own demand intercept to . In stage 2, after observing both investments, firms simultaneously choose quantities . Their inverse-demand prices and profits are
A subgame-perfect equilibrium consists of an investment pair and a quantity strategy assigning a Cournot Nash equilibrium to every feasible investment pair, including pairs reached after a unilateral deviation. At the chosen investments, neither firm can improve its profit by changing its own investment, anticipating the stage-2 strategy. The stage-2 payoff excludes investment cost because that cost is already sunk when quantities are chosen.
The goal is the paper's existence claim, over the game itself:
The classical firm's cost coefficient is smaller, yet the quantum firm invests more. The proof gives , , , , ; its investments are and . The goal concerns the actual two-stage equilibrium, so the closed forms are supporting milestones rather than the definition of success. The paper's Proposition 2 and its proof appear on PDF pages 14 and 27–28.
Equations (3)–(4) give the interior Cournot quantities; (14)–(15) give the second derivatives of reduced profit; Lemma 1 gives sufficient parameter thresholds for positive investments and concavity; and (5)–(6) give equilibrium investments. Section 7 derives an exact threshold for the inequality and evaluates it at the numerical witness. Additional milestones record the displayed optimal profits, Proposition 1 on positive quantum profit, the no-investment comparative static of (11)–(12), and Corollary 1's monopoly case. These targets follow the working paper's equations and proofs.
The result separates a firm's marginal cost of supplying computations from its cost of expanding the market. In this model, the quantum firm can justify a larger investment even with a larger coefficient on investment cost. The exact threshold identifies which combination of demand, variable cost, competition, and investment costs creates that ordering. Proposition 1 and the comparative static make related claims about profitability and the value of additional market size.
A complete formalization would connect the printed algebraic formulas to best responses over nonnegative actions, including possible corner outcomes after off-path investments. The reusable component is the published linear differentiated Cournot game; this mission adds the investment stage and source-specific parameters. The working paper supplies proofs on paper, while the Lean theorem files here are open statements awaiting machine-checked proofs.
Equations (3)–(4) solve interior first-order conditions, but stage-2 deviations can drive one firm's quantity to zero. A proof about a genuine subgame-perfect equilibrium must handle those corners throughout the strategy, not only at the final investment pair. Likewise, the second derivatives of the algebraic interior profit do not automatically settle every stage-1 deviation in the constrained game. The mission's equilibrium milestone must bridge those two readings. Lemma 1's thresholds also contain quotients whose denominators require checking under the stated parameter conditions.
All parameters, investments, quantities, profits, and thresholds are real. The formalization requires in the equilibrium predicates. Standing records , , and positive . Lemma1Cond records the strict thresholds at the end of the proof of Lemma 1, with the paper's represented by real max. Firm 1 is quantum throughout; firm 2's unit cost is defined as , not an independent parameter. The closed-form quantities and investments are used in milestones; the main goal quantifies over the subgame-perfect equilibrium predicate.
Several printed or implicit conventions affect the statements. Lemma 1 is phrased loosely on PDF page 11; its proof's exact sufficient conditions on page 26 are the milestone. The proof's strict claims about differences of thresholds become equalities when , without changing the final sufficient condition. Corollary 1 uses a different regime, , and is stated without the main model's Standing condition; ensures the asserted quantum monopoly has positive output. The comparative static concerns the separate model with . A printed reference to optimal profits in “(11)” in the proof of Proposition 1 points to the unnumbered optimal-profit display on PDF page 12. The repeated in the proof of Proposition 2 is read as .
Useful contributions include proofs about nonnegative Cournot best responses and their uniqueness, the boundary behavior of stage-1 reduced profits, the exact sign conditions on the paper's denominators, and proofs of the source-indexed statements. The definition layer is meant to be shared by all results in this one paper.