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?
Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.
The Monge optimal transport problem on the real line with the classical distance cost famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs with and letting : the limit selects a distinguished optimal plan, the excursion coupling, built from the level sets of the difference of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.
This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.
How much flow can be sent from a source to a sink through a network with arc capacities — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination of simple circulations with only forward arcs, with integer when is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ( s.t. , , for , ), defines augmenting paths (Definition 7.2: on forward arcs, on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:
(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;
(b) the value of the maximum flow equals the minimum cut capacity
— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).
Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time and a recommendation must be sound (wrong with probability at most ) while minimizing . The information-theoretic complexity is : every sound strategy needs , and the Track-and-Stop algorithm — the goal theorem — achieves exactly. The mission also covers the fixed-budget counterpart, sequential halving.
When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of , and the correct exponential rate is governed by the binary relative entropy rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of . The goal theorem shows KL-UCB attains
— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.
Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy , and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event , — no test can distinguish from with total error probability below . This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality ), Pinsker's inequality , and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.
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.
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.
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.
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.
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.
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.
Since 2017, billions of dollars have been raised through the issuance of crypto-assets, many of them tokens: digital claims on a future product or service, issued before the product exists. Malinova and Park, Tokenomics: When Tokens Beat Equity (SSRN 3286825; Management Science, 2023, doi:10.1287/mnsc.2023.4882), ask when such a pre-sale is a better way to finance a venture than the two classical instruments, equity and debt. To answer, they first work out how equity and debt perform in a simple monopoly model in which demand is uncertain when the money is raised. This mission formalizes the debt half of that benchmark (Proposition 2), together with the equity half (Proposition 1). The other three missions of the series treat the optimal token contract (Proposition 3), its comparative statics (Proposition 4) and financing under moral hazard (Proposition 8); all of them compare against the benchmark proved here.
An entrepreneur must pay a set-up cost before she learns demand. Afterwards she is a monopolist with constant marginal cost , facing the linear inverse demand
where the demand intercept is uniformly distributed on , with . Investors require a zero expected return. For a payoff of the demand realization write
At demand the monopolist produces and earns the monopoly profit
that is if and otherwise. The project's net present value is .
Under equity, investors receive a fraction of profits; break-even is (5). Under debt with promised repayment , investors receive : the full when the venture is solvent (), the whole monopoly profit under the debtor-in-possession arrangement when , and nothing when . The entrepreneur keeps . The repayment breaks even when
In Lean these are expect, pim, npv, equityShare, debtInv and debtEnt in the namespace TokenFinance.Debt.
If , then
and every such satisfies
Uniqueness is asserted among all nonnegative repayments, which implies the paper's uniqueness in .
Propositions 1 and 2 establish that, absent agency problems, equity and debt finance exactly the positive-NPV projects and leave the entrepreneur the entire surplus. This is the benchmark of the paper: Proposition 3 shows that a carefully designed token pre-sale matches it, while naive token contracts (revenue sharing, plain output pre-sales) distort output and fail to finance some profitable projects. Corollary 1 of the paper is the conjunction of Propositions 1–3. The debt repayment characterized here also reappears in the moral-hazard analysis (§IV), where the ranking of debt, tokens and equity depends on the size of relative to the low-demand state.
On the formal side, the results are proved in the paper with short calculus arguments, and nothing about them is machine-checked. The mission produces a checked model of uniform-demand monopoly financing in which expectations are genuine integrals of realized payoffs, the cubic reduction of the break-even condition, and the uniqueness argument for the repayment. These are the pieces the token missions of the series build on.
The central step is the passage from (7) to the cubic (33). The investors' payoff changes form at and at the solvency threshold , so the expectation must be split at points that depend on and may fall outside for large ; only for does the threshold stay inside the demand range. Uniqueness over all also needs the regime , where the investors receive the whole profit and the break-even condition reduces to . A naive argument that solves the cubic in and stops gives uniqueness only inside .
All objects are plain functions of real parameters; there is no probability space. Demand enters only through , the expectation under (open or closed endpoints make no difference). Case distinctions of the paper are encoded with and , so the break-even condition (7) is a single integral of the realized repayment rather than the paper's split integral with limits; the split form is a theorem (milestones 2 and 5). The standing assumptions are and ; is the paper's "positive marginal cost" (p. 22) and is kept throughout the series although Proposition 2 itself needs only . "All positive NPV projects" is the hypothesis on the integral-defined NPV.
A trivializing formalization is ruled out: the NPV, the investors' break-even condition and the entrepreneur's payoff are expectations of realized payoffs, never their closed forms, so neither (3) nor the reduction to (33) is true by definition.
The definitions file also declares the token objects of Proposition 3 (the revenue share , the realized token payoffs and condition (16)), identical across the four missions of this series so that they can be merged later; they are not used here. Out of scope: the secondary token market, bankruptcy costs, consumer welfare and the institutional discussion of the paper. Useful infrastructure includes lemmas for integrals of piecewise polynomials on intervals and a reusable "strictly increasing continuous function with a sign change has a unique root" argument.
Grocery chains and restaurants that promise delivery within an hour or less must decide, at each dispatch epoch, which drivers to send out and along which routes. Liu and Luo (arXiv:2107.13058v3; Manufacturing & Service Operations Management, 2023) model this as a finite-horizon dynamic program and solve its per-period approximation with a logic-based Benders decomposition: a master problem chooses how many drivers to commit to future periods, and a routing subproblem then picks the routes that serve the current orders.
The routing subproblem is a set-partitioning integer program over an exponentially large route set. The paper solves it with a route enumeration algorithm, which generates only the routes that can still appear in an optimal solution. The pruning rule that makes this work is Lemma 2 (p. 19): a route whose LP reduced cost exceeds the gap between an upper bound and the LP bound cannot appear in any optimal solution. Rules of this kind, reduced-cost fixing for set-partitioning formulations, are a standard component of exact vehicle-routing algorithms (see, e.g., Baldacci, Christofides, Mingozzi 2008). This mission formalizes Lemma 2 for the paper's own subproblem.
Fix a period and a solution of the master problem. The data are:
Write , the number of drivers the master solution allows to remain occupied in period .
The routing subproblem SF1 (pp. 16–17) is
Its LP relaxation RF1 replaces by and the partitioning rows by covering rows ; denotes its optimal cost. The dual variables are for the occupancy rows, for the fleet row and for the covering rows. The reduced cost of a route with respect to a dual solution is
An upper bound of SF1 is a number at least as large as the optimal cost of SF1.
Let be an upper bound of SF1, the optimal cost of RF1, a dual optimal solution of RF1, and . If
then in every optimal solution of SF1.
For a route , let , let be the routes that cover only locations in , and let SF1 be SF1 on and with right-hand sides and ; RF1 (75)–(79) is its LP relaxation, and its optimal cost.
The result. Lemma 2 turns one LP solve into an elimination test for every route at once. The route enumeration algorithm of §5.3 generates only routes whose reduced cost is at most a gap , raises until it reaches , and at that point the enumerated route set is guaranteed to contain every optimal solution of SF1. Without the lemma the algorithm would not certify optimality. The same algorithm also solves the single-period problems in the offline estimation stage of the paper's policy, so its correctness underlies all the computational results.
Formalizing it. The lemma is proved in the paper's Online Appendix (Appendix G, p. 42) in a few lines that rest on unstated conventions: the signs of the dual variables, the right-hand sides of SF1, and the equality of with the dual objective of a dual optimal solution, which is LP strong duality. The formalization pins each of these down. The strong-duality step is available on the platform as LinearOptimization.lp_strong_duality (proved, for general-form LPs indexed by Fin), included as a reference item. No part of this mission is formalized elsewhere.
The elimination test (74) and the dual bound are short combinatorial and weak-duality arguments. The step that does not go through by algebra alone is (80) ⇔ (81): it requires that the dual objective of the dual optimal solution equals . Treating this equality as a hypothesis would make the step trivial and is excluded; the hypothesis is only that the dual solution maximizes the dual objective over the dual feasible set. Deriving the equality means applying LP strong duality to RF1, whose data are indexed by arbitrary finite types rather than by Fin, so a transport to the platform's general-form LP is needed. A second point is the passage from SF1 to SF1: removing a route from an optimal solution must yield a feasible point of SF1, which depends on the reduced right-hand sides and on the partitioning rows of SF1 forcing the other routes to avoid 's customers.
All statements live in the namespace OnDemandDelivery.RouteElim. Routes, locations and future periods are arbitrary Fintypes; route vectors are functions to ℝ; and are natural numbers and is computed in ℝ. The standing assumptions are , and (pp. 15–16, (17), (21)).
Conventions committed to:
IsLeast), not an arbitrary real.EReal, when SF1 is infeasible, and (74) is stated in EReal.Trivializing formalizations are ruled out: is not a free real, the dual solution is optimal and not merely feasible, no hypothesis states equals the dual objective, and the conclusion concerns optimal solutions of SF1.
Needed infrastructure: weak duality for the two LPs (elementary), and a bridge from RF1 to LinearOptimization.GeneralFormLP for strong duality, which is reusable for any LP stated over finite index types. Contributions of such a transport lemma are welcome.
Establish the separation exponent for total Boolean functions, improving on the depth-20 specialization of OpenAI's construction.
Precisely, for every and every integer , construct a function with and .
A finite certificate is sufficient: supply a function and an input with , , , and , then apply the shared certificate theorem. Sharper estimates, improved parameters, and different constructions are all eligible; direct family proofs are also welcome.
This is an open research target. The preceding benchmarks are classically and approximately from the depth-20 seed. Numerical searches guide discovery but do not replace certified bounds. Intermediate improvements are welcome as separate campaign entries.
The RangeDivisor problem asks whether an integer has a divisor in a specified short interval. It is the decision problem connecting number theory to the two item periodic joint replenishment model studied by Schulz and Telha. Their Appendix starts with Partition, the problem of splitting a list of positive integers into two groups of equal sum, and constructs a RangeDivisor instance from primes chosen near carefully scaled powers of two. The equivalence between the two yes instances is the mathematical target here. Schulz and Telha, Appendix, pp. 16–17
The route has a history. Karp included Partition among classical combinatorial decision problems in 1972. Shor discussed an NP complete variant of factoring in 2011, and Schulz and Telha adapted that connection to their joint replenishment setting. The paper cites a 2016 conditional short interval result of Dudek, Grenié, and Molteni to obtain primes that can be sampled near the requested powers. That prime existence claim motivates the reduction, while this mission starts with primes satisfying the specified windows. Karp, 1972 Shor, 2011 Schulz and Telha, p. 16
A Partition input is an indexed list of natural numbers. It is a yes instance if some index set has . Indices matter: equal entries may occur more than once and can be assigned separately. For this reduction, , , and each entry lies in . The total is assumed even. Write , so is then an integer even though its Lean definition is real valued. Schulz and Telha, Appendix, p. 16
Set and . The input also includes a real constant and a prime for each index. Every prime lies in the open interval
and the paper's quantitative small window condition holds for every . Define , , and . The RangeDivisor instance uses the integer endpoints and . A valid instance has and ; it is a yes instance if some divisor of belongs to . These conditions are part of the target, not conventions left to the reader. Schulz and Telha, pp. 12, 15–17
The goal states the full correctness of the rounded numerical construction. Under the prime windows above and the paper's condition , the triple is a valid RangeDivisor instance and
The milestones follow the Appendix's stated intermediate claims: the elementary power estimate, the chain of prime windows, the equivalence for a subset sum and its subproduct, the unrounded divisor equivalence, the numerical interval condition, and the paper's rounding assertion. The unrounded equivalence is a separate milestone because it isolates the number theoretic claim from the integer endpoint convention. Schulz and Telha, pp. 15–17
The result turns equal sum partitions into divisors in a controlled interval of a product of primes. This is the first mathematical half of the paper's route from Partition to the periodic joint replenishment decision problem; Lemma 3 supplies the second half. The present theorem identifies exactly which numerical statements that route needs, including validity of the rounded interval. Without the equivalence, the constructed integer might have a divisor in the interval for reasons unrelated to the original Partition input. Schulz and Telha, §3 and Appendix
The paper proves its reduction on paper. This mission asks for machine checked proofs of the reduction's arithmetic assertions, not a new complexity result. The reusable pieces are finite product bounds for real powers, the description of divisors of a finite prime product as subproducts, and a rounding result for the RangeDivisor side condition. Such pieces can support other reductions that encode additive choices by products of nearby primes.
The prime bounds are stated one index at a time, while a divisor of may combine any number of factors. Controlling the product through a strict interval must account for every subset size, including the empty subset and repeated primes. The converse has an additional discrete issue: a product close to the target power should correspond to the exact integer half sum, not merely to a nearby real value. After that, changing real endpoints to integer endpoints must preserve both the divisor question and the numerical promise required by RangeDivisor. A statement only about divisors in the unrounded interval leaves the eventual decision instance incomplete.
Lean represents inputs as functions Fin n → ℕ, index subsets as finite sets, primes with Nat.Prime, and exponents and interval endpoints in the real numbers. The real powers use real exponentiation; uses real division, not truncated natural division. The general Partition and RangeDivisor predicates are separate definitions. The Appendix's , , , and are derived definitions of the particular input, so a theorem cannot choose convenient values for them. Strict window inequalities remain strict, and the goal retains the printed sampling window rather than assuming only the later multiplicative bound. It explicitly asserts the rounded instance condition as well as the yes instance equivalence.
The printed converse needs an even total: if the total is odd, is half integral and a subset one half unit away can produce a product inside without being a Partition solution. A computational reduction can send an odd total to a fixed no instance; this theorem covers the nontrivial even branch. The prose condition that is sufficiently large is replaced by the paper's displayed inequality , and the printed endpoint condition is stated directly. The proof must not gain a vacuous equivalence by allowing zero indices, by selecting the primes existentially to fit the answer, or by dropping the sampled prime windows.
This mission formalizes the correctness of the reduction behind Theorem 2; polynomial running time, randomized prime sampling, the conditional prime count, the padding of arbitrary Partition inputs to a fixed bit range, and the NP hardness assertion are outside its Lean statement. The Riemann hypothesis is needed by the paper to justify finding suitable primes efficiently, not as an assumption of the arithmetic equivalence once those primes are given. Contributions that establish the product, divisor, or rounding milestones are welcome. Schulz and Telha, pp. 15–17
Fair division of indivisible goods asks how to split a set of items among agents with different tastes so that nobody has a strong reason to complain. Fairness notions such as envy-freeness up to any good (EFX) and the maximin share (MMS) have been studied extensively as algorithmic targets: given the agents' valuations, compute an allocation satisfying the notion. In practice the valuations are private, and an agent may misreport them to obtain a better bundle. Truthful mechanisms are too weak for this setting: for two agents, no truthful mechanism without payments produces EFX (or even EF1) allocations when there are more than four goods (Amanatidis, Birmpas, Christodoulou, Markakis, EC 2017).
Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644, Mathematics of Operations Research 2024) take a different route. They let agents bid strategically and ask how fair the pure Nash equilibria of a non-truthful mechanism are with respect to the agents' true valuations. For two agents they study a modified version of the classical cut-and-choose protocol, due in this form to Plaut and Roughgarden (SIAM J. Discrete Math. 2020). They show that it always has equilibria and that all of them are MMS, and hence EFX. As an algorithm run on truthful values, the same mechanism guarantees no more than a fraction of the maximin share.
There are two agents and a set of indivisible goods. Agent has a non-negative value for each good and values a bundle additively, . There is no free disposal, so an allocation is a partition of .
Mod-Cut&Choose (Mechanism 2) works as follows:
In the Lean development these objects are val, IsBestResponse, IsPNE and rank (namespace StrategicAlloc.RRFair, shared with the sibling missions) and IsEFX, mu, IsApproxMMS, cut and modCutChoose (namespace StrategicAlloc.CutChoose).
For every instance with two agents and non-negative additive valuations,
Both halves are part of the goal. Existence alone, or fairness of equilibria alone, is a weaker statement.
LittleCharity.MMS.mms_le_average, used here as a reference.The theorem identifies a simple mechanism whose strategic outcomes are as fair as the best allocations that exist for two agents: every MMS allocation is EFX, and an MMS allocation always exists for two agents. The mechanism achieves this without any truthfulness requirement. It is the positive counterpart to the impossibility results for truthful mechanisms. It is also the starting point of §4.2 of the same paper, which asks how much of this guarantee survives for every mechanism whose equilibria are always EFX (Theorems 4.5 and 4.7).
The result is proved in the paper. As far as the platform's catalogue shows, none of it is formalized. This mission produces:
The fairness half is short once its ingredients are available. The weight lies in Lemma 4.1: the cut phase is a greedy procedure over a bid-sorted order, and showing that every partition of can be produced requires explicit bids and an invariant along the greedy loop. The case where both sets have at least two goods needs carefully calibrated values. The tie-breaking rules (lexicographic sorting, ties to in both phases) enter the argument, and the formalization fixes them exactly.
A natural shortcut is to restrict agent 1's strategies to orderings of the goods, or to assume that any cut is reachable. Either one turns Lemma 4.1 into an assumption. The existence half needs no compactness argument: the set of possible cuts is finite, so a best cut for agent 1 exists, but this has to be connected with deviations over the continuum of real bid vectors.
Fin 2 (agent 1 is 0) and goods are Fin m, indexed in the order that lexicographic tie-breaking refers to.Fin 2 → Fin m → ℝ. Non-negativity of is a hypothesis of every theorem, and every bid in a profile or deviation is required to be non-negative.mu v i reuses the published LittleCharity.MMS.mms with two bundles and .LittleCharity.MMS.IsEFX is not used.The statements rule out the trivializing formalizations. Deviations are not restricted to a subset of bids (rankings, truthful bids, a finite menu). MMS and EFX are measured with the true valuations, never with the bids. The mechanism's tie-breaking is fixed rather than arbitrary.
A complete development needs basic finite-sum and finite-supremum facts and a proof that the greedy cut covers with disjoint bundles. The model layer (val, IsEFX, IsPNE over all non-negative bids) is shared with the four sibling missions on Round-Robin and on mechanisms with EFX equilibria. Proofs of any milestone, and of mms_le_average, are welcome.
The joint replenishment problem (JRP) is the multi-item extension of the economic order quantity (EOQ) model. Each item is reordered periodically and pays its own ordering and holding costs, and a joint ordering cost is shared by items ordered at the same time. Before this work no hardness result was known for the periodic JRP (p. 10), even though no exact polynomial-time algorithm was known either (Schulz and Telha, arXiv:2007.09045; Operations Research, 2024, as Integer Factorization: Why Two-Item Joint Replenishment Is Hard).
The paper explains this through number theory. In the periodic JRP the joint cost is incurred every periods, so the objective contains a greatest common divisor of the decision variables. The paper's Theorem 2 states that, assuming the Riemann hypothesis, the two-item periodic JRP is NP-hard under randomized reductions. The proof composes two reductions:
This mission formalizes Lemma 3. Mission 4 of this series formalizes the Partition half; missions 1 and 2 formalize the integer-factorization reductions behind Theorem 1.
A period is a positive integer . An item with ordering cost and holding cost costs
per unit time. The two-item periodic JRP (objective (3), p. 10) minimizes, over ,
As a decision problem (p. 13), it asks whether some has cost at most a threshold .
An instance of RangeDivisor (p. 12) is a triple of integers satisfying
it is a yes-instance when has a divisor with .
Given such a triple, the instance sets
and the threshold is , where . Once item 2 is fixed at , item 1 solves problem (5):
In Lean these objects are JRPHard.Aperiodic.eoq, JRPHard.Periodic.periodicCost, JRPHard.Periodic.coefK2, JRPHard.Periodic.coefH2 (shared with missions 1 and 2), and IsRangeDivisorInstance, HasDivisorIn, coefK0, rangeCost, threshold, obj5 and fConv in the namespace JRPHard.RangeDiv.
For every RangeDivisor instance ,
Lemma 3 is the step that carries hardness from number theory to inventory theory. With Shor's result it shows that, under the Riemann hypothesis, no polynomial-time exact algorithm for the two-item periodic JRP exists unless NP problems can be solved in randomized polynomial time. The paper concludes (p. 15) that no algorithm for the two-item problem may be simultaneously exact and polynomial on all inputs, so some concession, such as heuristics, must be made.
The result is proved in the paper; it has not been machine-checked. The mission produces a checked statement of the reduction's correctness with every coefficient explicit, and it corrects two imprecisions in the printed lemma (the threshold and the unspecified "sufficiently large" coefficients of item 2; see below). The objects (eoq, periodicCost) are the same ones used in mission 2 of this series.
Each step is elementary, but the statement mixes integer and real reasoning. The objective of (5) is not monotone or convex in : its value jumps between at divisors of and at least elsewhere. The argument must show that the gap between these two curves exceeds the window around , and this is exactly what RangeDivisor's condition provides. Without that condition a non-divisor can be cheaper than (for , , , the period has objective ). The pinning of also has to beat the slack against , which is where is used.
This mission formalizes the correctness of the reduction behind Theorem 2 (its JRP half, Lemma 3); polynomial running time is not formalized. Theorem 2 itself, Shor's NP-completeness of RangeDivisor under randomized reductions, and "one can construct in polynomial time" are not stated. What remains of the polynomial-time claim is the explicit coefficients and the bound (bit length at most ).
Conventions:
Real.sqrt exactly as printed;Two disclosed departures from the printed lemma:
A formalization that drops the positivity of periods, states the threshold as on the full two-item cost, or leaves existential does not capture Lemma 3 and is ruled out.
No library beyond Mathlib (Nat.gcd, Real.sqrt) is needed. Proofs of the milestones, and alternative proofs of the goal, are welcome.
Video-game consoles, streaming services and messaging apps share two features: users value a platform more when more people use it (network effects), and some users buy access to more than one platform (multihoming). In the standard Hotelling model where every consumer buys exactly one good, network effects intensify competition: a stronger network effect makes demand more price-sensitive, and the equilibrium price and profit fall in (the paper's single-homing benchmark, §3.1). Foros, Kind and Stähler (SNF Working Paper 16/21, NHH Bergen, 2021; published in Management Science, 2025, doi:10.1287/mnsc.2022.00613) show that this intuition reverses when consumers can multihome: firms then price the incremental value of their good (Kim and Serfes, 2006; Anderson, Foros and Kind, 2017), and the network benefit of the rival's users feeds back into that incremental value.
This mission formalizes the paper's Proposition 3, which describes how the symmetric multihoming equilibrium price and profit respond to the strength of network effects over the whole admissible range. It is the third of three missions on the paper; the first treats weak network effects with asymmetric firms (Proposition 1) and the second the comparison with the no-network-effect benchmark (Proposition 2).
Two firms sit at the ends of a Hotelling line of unit length, populated by a unit mass of consumers, uniformly distributed. A consumer at distance from firm pays a mismatch cost with . Each good carries exclusive features (the same number for both firms in this mission) plus features common to both goods, which cancel from every object below. Buying good gives a network benefit , where is the network-effect strength and the expected number of users of good ; the paper assumes (Assumption 1(i)).
A consumer buys a second good when its incremental value exceeds its price. Under fulfilled expectations (), the multihoming demand for good at prices is (14)
Maximizing gives the reaction function (15), , whose symmetric fixed point yields the price and profit (26)
In the Lean development these are demandM t μ e pi pj, reactM t μ e pj, pM t μ e and piM t μ e in the namespace Multihoming.Hump. Partial multihoming means that some consumers buy one good and some buy both.
Assume partial multihoming. Then and are hump-shaped in on : there are peaks with
The goal leaves the peaks unnamed; that is the paper's statement.
The result. Proposition 3 says that firms benefit from weak network effects and are harmed by strong ones. As the goods become as if undifferentiated, competition for consumers becomes Bertrand-like, and ; combined with this means firms would prefer a market without network effects once these are strong enough. This non-monotone response is the paper's main qualitative message on pricing under multihoming, and the comparison of Proposition 2 (where the profit curve crosses its level) depends on the same shape.
Formalizing it. The result is proved in the paper by sign analysis of explicit derivatives; it has no machine-checked proof. A formal proof certifies the two derivative factorizations, the location of each peak strictly inside , and the passage from derivative signs to strict monotonicity on closed intervals that the appendix states in one sentence. It also makes explicit the parameter range on which the statement holds, which the printed proposition leaves to the phrase "partial multihoming".
The derivatives of and are rational functions whose numerators are quadratics in with square-root roots; showing that exactly one root lies in requires inequalities between square roots and polynomials in that hold only under . The appendix asserts "it is straightforward" and "it can be shown" at these steps. A second obstacle is the passage from "the derivative vanishes at one point, is positive at and negative at " to strict monotonicity on each closed piece: this needs the sign of the derivative on the whole open subinterval, not only at the endpoints. Showing only that a maximizer exists on is trivial for any continuous function and is not the claim.
HasDerivAt; all functions are smooth near under the hypotheses, and every denominator (, , , ) is positive where it is used, so no statement relies on Lean's convention or for .HasDerivAt, strictMonoOn_of_deriv_pos) and real-closed-field arithmetic are needed. Contributions of any milestone, alternative proofs of the hump via the derivative factorizations, and proofs that identify the price peak explicitly are welcome.