Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In an impulse control problem a controller does not steer a process continuously: at times of its choosing it shifts the state by a finite jump, paying a fixed cost plus a cost proportional to the jump. Such models describe central-bank interventions on an exchange rate, inventory replenishment and cash management. Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) study nonzero-sum games in which two players control the same diffusion by impulses. They prove a verification theorem for such games and apply it to a linear game whose Nash equilibria are explicit.
The paper's interpretation of the linear game is two central banks with different targets for an exchange rate. An explicit equilibrium gives explicit intervention thresholds, and Section 4.4 of the paper asks how these thresholds respond to the fixed cost of intervening. This mission formalizes that comparative-statics question: when intervening becomes more expensive, do the players intervene less?
The game of Section 4.1 has a discount rate , a volatility , running payoffs and with , and intervention costs: a player who shifts the state by pays and the opponent receives . The standing assumptions of the section are
All parameters except the fixed cost are held fixed. Set and , both positive. For the function
has a unique zero . With
and a parameter , the paper's formulas (4.20) are
for , with and . In the Nash equilibrium of the paper's Proposition 4.7, player 1 intervenes when the state falls below and moves it to ; player 2 intervenes above and moves it to . The interval is the continuation region, where nobody intervenes. The equilibrium payoffs , are explicit as well (4.27).
The continuation region therefore widens strictly as the fixed cost grows. The statement concerns the explicit functions (4.20); that they are equilibrium thresholds is mission 2 of this series.
Proposition 4.13 is the rigorous form of the economic intuition that costlier intervention makes players more patient. Together with Proposition 4.12 it describes the whole range of costs: the region of inaction grows strictly and invades the real line as , where the payoffs converge to those of the uncontrolled Brownian motion. Proposition 4.14 adds that, when the fixed gain vanishes, the targets move away from the centre . The paper's numerical section shows that without the targets need not be monotone.
The results are proved in the paper, in a few lines each, by differentiating the implicit function . None of them is formalized. The mission produces a machine-checked treatment of a parametrised implicit function, defined by a transcendental equation: smoothness, explicit derivatives, and the asymptotics at both ends. On top of it, it gives a fully verified comparative-statics result for an explicit game equilibrium.
The thresholds depend on only through , which has no closed form, and through , a sum of terms in and . Monotonicity of alone does not settle the goal: is a ratio of two increasing functions, and its direction is decided by how fast grows compared with , uniformly on , including near , where has no zero and degenerates. The limits as need more than : grows linearly in , so the rate at which decays decides whether the targets diverge and whether the payoff coefficients vanish.
The parameters are bundled in a structure, and the standing assumptions not involving in a predicate , , , , , . and are computed from as in (4.21), not taken as free parameters. All quantities are real numbers.
is defined as . Milestone 1 proves that this is the paper's unique zero for every . For the set is empty and the definition returns the placeholder . Every statement therefore restricts to , to , or to , and no statement can be satisfied through a junk value. On one has , so the square roots in (4.20) are the paper's. "Increasing" and "decreasing" are read strictly, as the proofs give. is ContDiffOn ℝ ∞, and is deriv ξ. Limits at use the right neighbourhood filter.
Two departures from the page are disclosed in the items:
A complete development needs the intermediate value theorem and strict monotonicity on an interval, a differentiable implicit (or inverse) function theorem in one variable, and asymptotic estimates of near and near . These one-variable lemmas about implicitly defined functions are reusable beyond this mission. Proofs of the milestones in any order are welcome.
Many economic and engineering systems are steered by agents who act at discrete instants rather than continuously: a central bank intervenes on an exchange rate, two energy producers adjust a shared stock, a firm rebalances inventory. Each action has a fixed cost, so continuous control is not realistic. The mathematical model is impulse control: the state follows a diffusion, and a controller may shift it at chosen stopping times by paying a cost. The single-controller theory is classical (Øksendal and Sulem, Applied Stochastic Control of Jump Diffusions, 2007). When two controllers with different objectives act on the same state, the result is a nonzero-sum stochastic differential game with impulse controls.
Before Aïd, Basei, Callegaro, Campi and Vargiolu, the literature on games with impulse controls was almost entirely zero-sum: Cosso (SIAM J. Control Optim., 2013) characterised the value of zero-sum impulse games through a double-obstacle quasi-variational inequality in the viscosity sense. Their paper (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) gives the first general formulation of the nonzero-sum case together with a verification theorem: a system of quasi-variational inequalities (QVIs) whose sufficiently regular solutions are the equilibrium payoffs. Its Section 4 then computes Nash equilibria in closed form for a one-dimensional game.
A -dimensional Brownian motion on a filtered probability space satisfying the usual conditions drives the state equation
with globally Lipschitz and . The game takes place in an open set and ends at the exit time of the state from . Each of two players has a nonempty impulse set and a continuous impulse map : an intervention with impulse moves the state from to .
A strategy of player is a pair with open and continuous. Player intervenes as soon as the state leaves , with impulse at the current state . Player 1 has priority on ties, and several interventions may happen at the same instant. This defines the controlled process , the intervention times and impulses of each player, and the states just before each intervention. The payoff of player is
where , , is a running payoff, the cost of one's own interventions, the gain from the opponent's, and a terminal payoff on . A pair of strategies is -admissible, , when these four terms are integrable, has all moments, and the interventions do not accumulate before . A Nash equilibrium is a pair in from which no player gains by a unilateral admissible deviation.
Given candidate payoff functions on , let be the unique maximiser of over . Define , , the continuation region and the generator . The QVI system is
Suppose solve the QVI system, with polynomial growth, is a Lipschitz surface near which has locally bounded first and second derivatives, , and the threshold pair is -admissible. Then
The goal follows from Steps 1 and 2 and their mirror images for player 2.
The theorem turns the search for Nash equilibria of nonzero-sum impulse games, an infinite-dimensional fixed-point problem over strategy pairs, into a deterministic problem: find functions satisfying a system of coupled QVIs with prescribed regularity. The regularity conditions become smooth-pasting conditions, hence a system of algebraic equations; Section 4 of the paper solves it explicitly for a one-dimensional game with linear payoffs. A further consequence is structural: equilibrium payoffs need only be on the opponent's continuation region, which is what lets non-smooth, piecewise-defined candidates qualify.
The result is proved in the paper; no machine-checked version exists. A complete formalization would be the first verified verification theorem for impulse control, single-player or game, and would expose every convention of the model: priority on ties, simultaneous interventions, the treatment of exit, and the integrability of the payoff. Several of these conventions need correction on the page, as listed below.
The heuristic argument applies Itô's formula to and uses the QVIs term by term. This fails on two counts. First, is only across the free boundary , so Itô's formula does not apply directly. The paper mollifies (following Øksendal's proof of his verification theorem for optimal stopping) and must control the second derivatives near a Lipschitz boundary. Second, the sums over interventions may be infinite and the horizon unbounded, so expectations and limits do not commute. The passage to the limit needs the integrability built into and the polynomial growth of . The stochastic-calculus infrastructure itself (Itô's formula for continuous semimartingales stopped at random times, strong solutions of Lipschitz SDEs restarted at stopping times) is largely missing from Mathlib.
The Lean model is pathwise. A realization is a sequence of diffusion pieces, each solving the state equation from the random restart time with the restart value. The Itô integral is the published relation EthierKurtz.HasBrownianItoIntegral, and the stochastic basis uses the published You2015.Shared.UsualConditions and IsFBrownian. Times take values in with , and the state space is EuclideanSpace ℝ (Fin d). asks for one admissible realization, while the Nash inequalities and the payoff identity hold on every admissible realization; strong uniqueness makes these readings equivalent.
The following deviate from the page and are disclosed in the items:
The payoff is a Bochner expectation only inside , which requires the conditions of (2.7) and the integrability of each payoff. A non-integrable deviation therefore never receives the junk payoff , and the Nash inequality cannot hold vacuously.
Contributions are welcome on the stochastic-calculus layer this needs (Itô's formula, strong existence and uniqueness for Lipschitz SDEs, optional stopping for stochastic integrals) and on the mollification lemma for functions that are with piecewise bounded second derivatives across a Lipschitz surface. These are reusable well beyond this mission.
The Schur number is the largest such that can be partitioned into sumfree sets, sets with no such that ( allowed). Schur's argument gives , where the triangle Ramsey number is the least such that every colouring of the edges of with colours has a monochromatic triangle (Fredricksen–Sweet 2000, inequality (2)). Only are known (Heule 2018). For six colours the published range is ; the upper bound is with (DS1, rev. 18).
Timeline.
The first target is a centred-interval bound: if , then . With the recursive bound gives , and the centred bound gives ; with it gives only . The mission formalizes what a Schur colouring of with six colours would have to look like under .
All numbers are natural numbers, , and .
Schur colourings and covers. A colouring with colours is a map . It is a Schur colouring of (SchurColoring N c) if there are no with and , the case included. The cover form uses SumFree S and CoveredBySumFree X n ( lies in the union of sumfree sets); for the two bridge theorems pass between the two forms in both directions.
Triangle Ramsey property. (TriangleRamsey k r): every colouring with at most colours of the pairs of a finite set of at least naturals has a monochromatic triangle. For it is the inequality .
Neighbourhoods. The difference colouring gives a pair the colour . For a Schur colouring of it has no monochromatic triangle on , since . Write
colorNbhd c V v i);centralNbhd c m), which contains ;endpointNbhd c m i).The frontier. The frontier hypotheses are , , , and a Schur colouring of with colours. From the first two, holds, and the centred bound excludes Schur colourings of with colours; is the frontier interval. Six colours: , , , , .
Example. For , , , (and ), the classes , , form a Schur colouring of , with and endpoint neighbourhoods and , both closed under .
where , and :
The goal is a structure theorem under the hypothesis . It does not prove , and it does not assert that a Schur colouring of with six colours exists; whether such a colouring, or the structure it would force, exists is open. The goal is the six-colour instance of the general theorems below.
For a colouring of ordered pairs, a finite set , a point and a map with , on and on :
The result itself. Under , , and the goal constrains a six-colour Schur colouring of as listed above. In particular, each of its five endpoint neighbourhoods is a set of pairs whose difference colouring uses at most four colours, is invariant under and, like that of every subset of , has no monochromatic triangle. So such a colouring yields five colourings of with at most four colours, no monochromatic triangle and a fixed-point-free colour-preserving involution. A proof that this configuration cannot occur would give under the same hypothesis. Whether it can occur, and whether , are open.
Formalizing it. All 12 theorems of the tree, the goal included, are proved in Lean 4 with Mathlib over the bundles ClassicalSchurBasic, ClassicalSchurRamsey and ClassicalSchurColoring, with the axioms propext, Classical.choice and Quot.sound only. Independent Claude agents checked the Lean: one rebuilt the frontier theorems, re-ran their axiom audit and checked their statements against the argument; another checked every statement of the tree against the mathematics. The mathematics is in the paper if : a centred Schur bound and the structure at the frontier (A. McKenna, Zenodo, 2026, doi:10.5281/zenodo.23156099), and the Lean code is in its repository; the paper has not been refereed. is not formalized in the mission.
The centred bound counts, for one colour class, the points around the centre of the interval. At the frontier every such count is tight: each colour has elements in , and inside each colour other than has degree , the largest value that allows. So no single counting step gives a contradiction, and the theorems describe the tight case instead of excluding it. The first exclusion that the structure gives, parity, works only for odd ; at six colours .
The reflection is not a property of Schur colourings in general: the colouring , , of has but . At the frontier the theorem asserts it only for the with , so an argument that assumes a fully symmetric colouring proves a different statement. A direct search is no substitute: already needed a large certified SAT computation (Heule 2018), and with six colours is a much larger instance.
ℕ → Fin n on all of ; SchurColoring N c constrains only , with allowed. Distances are Nat.dist.Finsets. lies in range (2 * m + 2) , so the point is a candidate member; the centre never is.TriangleRamsey k r takes colours from any Finset of at most naturals; the pair colouring ℕ → ℕ → ℕ is constrained only on the pairs of the vertex set, which is any finite set of naturals. TriangleRamsey k 0 and TriangleRamsey k 1 are false.CoveredBySumFree X n uses Fin n → Set ℕ; the sets need not be disjoint or lie in .Bundles: ClassicalSchurBasic (SumFree, CoveredBySumFree) and ClassicalSchurRamsey (TriangleRamsey) are already public; ClassicalSchurColoring holds SchurColoring, colorNbhd, centralNbhd and endpointNbhd. Reusable: the colouring–cover bridges, the pigeonhole step, the centred bound for every , and the automorphism-extension lemma (arbitrary types). Welcome beyond the targets: a formal proof of TriangleRamsey 4 61, and results on whether the configuration of five paired -point sets exists.
Provenance: the centred-interval argument was first written by an AI agent based on ChatGPT (OpenAI) in a project discussion on 2026-09-27, and a Claude (Anthropic) agent audited it. The balance, saturation and reflection argument was proposed by an AI agent based on ChatGPT (OpenAI) in a project discussion; Claude checked each step and restated it with explicit hypotheses. Claude wrote the Lean proofs of both parts; the independent checks are described under Formalizing it.
Optimization over sets of matrices of fixed rank comes up in low-rank matrix completion, model reduction, and the low-rank approximation of solutions of large matrix equations. A standard approach treats the constraint set as a Riemannian manifold and runs gradient or Newton-type methods on it (Absil, Mahony & Sepulchre 2008). Each iteration takes a step in the tangent space and then has to return to the manifold. A map that does this to first order is called a retraction, and its cost is often what decides whether a manifold method is practical.
Absil and Malick (2012) study retractions defined by projection: step to in the ambient space, then take the nearest point of the manifold. Their Proposition 3.2 shows that for any submanifold () this projective retraction is a retraction. Section 3.2 makes it explicit for the manifold of fixed-rank matrices: near any matrix of rank , the nearest matrix of rank exactly is the truncated singular value decomposition (Proposition 3.3). Section 4.4 also gives a closed form for a second retraction on the same manifold, the orthographic retraction (Proposition 4.11).
Fix natural numbers , and . The space of real matrices carries the Frobenius norm (3.6). The fixed-rank set is
a smooth submanifold of . It is not closed: its closure is the set of matrices of rank at most .
A singular value decomposition (3.5) of is a factorization in which and are orthogonal and is zero off its diagonal. The diagonal of holds the singular values of in nonincreasing order,
and for . A matrix has rank exactly when . The truncated SVD of rank is (3.7).
For a set and a point , the projection is the set of nearest points: the with for all . For a set that is not closed, may be empty or contain several points.
Let . For every with and every singular value decomposition ,
The projection exists, is unique, and is the truncated SVD. The radius and the strict inequality are those of the paper.
The paper's proof goes through four claims, which are the milestones in attack order:
Write (4.7), with the positive diagonal of nonzero singular values, and a tangent vector (4.8). If is invertible, the orthographic retraction is
Here is the nearest point to of .
The result. Proposition 3.3 reduces the projective retraction on to one truncated singular value decomposition. With Proposition 3.2 this gives an explicit, computable retraction for Riemannian optimization on fixed-rank matrices. It is used, for instance, in low-rank matrix completion algorithms. The point is local: is not closed, so far from the nearest matrix of rank exactly need not exist, and the proposition gives an explicit radius on which it does exist and is unique. Proposition 4.11 gives a second retraction that needs only products of matrices and one inverse.
Formalizing it. All results here are proved, on paper. To the best of a search of Mathlib and the Prove2Me catalog, none is machine-checked. Mathlib has singular values of linear maps between finite-dimensional inner product spaces (LinearMap.singularValues), but no singular value decomposition in matrix form, no Weyl perturbation inequality for singular values, and no Eckart–Young theorem. A complete development would add these, and the Eckart–Young theorem with its uniqueness case is a standard result of numerical linear algebra in its own right.
The proof in the paper is short only because it cites three facts, and each of them is a real piece of matrix analysis.
A further subtlety: Proposition 3.3 must hold for any singular value decomposition of . Singular vectors are not unique, so the proof has to show that the truncation does not depend on the choice under the gap (3.8).
Matrices are Matrix (Fin n) (Fin m) ℝ with Mathlib's Frobenius norm (open scoped Matrix.Norms.Frobenius). The projection is the published platform predicate RandomGradFree.Nonsmooth.IsMetricProjection, and is the set {Y | IsMetricProjection (rankSet r) X Y}. The set equality with a singleton states existence, uniqueness and the formula together.
Conventions committed to:
sv X i is , 1-based as on the page. It is Mathlib's 0-based singularValues of Matrix.toEuclideanLin X at i - 1, so the index is meaningless and every statement uses indices .IsSVD X U S V is the predicate of (3.5). The singular value decomposition is a hypothesis of the theorems, never a choice made inside them, so the theorems hold for every singular value decomposition.truncSVD r U S V is , written with the diagonal of S. That these entries are the singular values is a fact to be proved, not part of the definition.Fin r ⊕ Fin p and Fin r ⊕ Fin q. The tangent vector and the normal space are taken in the form the page gives, and invertibility of is an explicit hypothesis. In the paper's proof it comes from " in a neighborhood of the origin".A formalization in which the radius is replaced by a smaller one, the projection is taken onto the matrices of rank at most , or the singular value decomposition is chosen inside the statement is a different theorem and is ruled out.
Wanted contributions, all reusable beyond this mission:
singularValues;Resource-constrained project scheduling with minimum and maximum time lags is the model behind make-to-order production, process-industry batch planning and large engineering projects. When the objective is the project duration or another regular function (nondecreasing in every start time), an optimum can be found among schedules that cannot be shifted to the left. Many objectives in practice are nonregular: net present value, earliness–tardiness costs, resource levelling and resource investment. For these, delaying an activity can pay, and "shift as far left as possible" no longer identifies a finite set of candidate schedules.
Neumann, Nübel and Schwindt (Math. Methods Oper. Res. 52, 2000) answered this with classes of schedules defined by the absence of pairs of opposite shifts: stable, semistable, pseudostable and quasistable schedules, the mirror image of active, semiactive, pseudoactive and quasiactive schedules. Section 3.2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), shows that these classes are exactly the extreme points of the feasible region and of its natural convex pieces. The classification of objective functions in §3.3, and every enumeration scheme of the later chapter, rests on that correspondence.
A project has activities with . Activity is the project beginning and the project completion. Activity has an integer duration , with and otherwise. The project network has node set and arcs with integer weights , each encoding a temporal constraint . A prescribed deadline is included as the backward arc of weight . Renewable resources have capacities , and activity uses units while it runs.
A schedule is a vector of start times. The time-feasible region collects the schedules with , and on every arc; it is a polyhedron, and a polytope when every activity precedes as in Remarks 1.1.2. A schedule is resource-feasible if at every time the running activities use at most units of every resource. The feasible region is . It is in general neither convex nor connected.
A schedule induces the strict order . For a strict order , the order polytope is . The order is feasible if . The schedule polytope of is .
A shift moves a schedule to . It is global if both are feasible, local if in addition a continuous path inside joins them, order-preserving if , and order-monotone if and are comparable. Two shifts from to and are opposite if with . A feasible schedule is stable, semistable, pseudostable or quasistable if no pair of opposite global, local, order-monotone or order-preserving shifts, respectively, starts at it. It is antiactive if no global right-shift starts at it.
For every feasible schedule :
The theorem makes four shift-defined classes computable objects: extreme points of explicit polytopes, or of a finite union of them. Together with Proposition 3.2.13, it gives each class of nonregular objective functions in §3.3 a finite candidate set of schedules among which an optimum can be sought (§3.2, p. 207). Theorem 3.2.18 gives the certificate for quasistable schedules: a spanning tree of the schedule network, which the later sections use to enumerate vertices.
The results are proved in the book, except Lemma 3.2.9, whose proof is cited to Neumann, Nübel and Schwindt (2000). As far as a search of the platform shows, none of them has been formalized. A formalization supplies the missing details, among them that connected and path components of coincide and the degenerate vertices behind the tree description. It also produces a reusable library of schedule classes on real-valued start times.
Part (b) is close to the definition, since a pair of opposite global shifts is a segment through with feasible endpoints. The content is elsewhere. In (c) the definition speaks of continuous trajectories and the right-hand side of connected components, so the proof needs local path-connectedness of a finite union of polytopes. In (d) the feasible region is not convex: an order-monotone shift keeps and in a common order polytope, but and may lie in different ones. The segment through has to be moved into a single order polytope with , and that is Lemma 3.2.9. Proposition 3.2.16 and Theorem 3.2.18 need the passage from linearly independent tight constraints to a spanning tree. They must allow degenerate vertices, where several trees describe the same point, and must represent the nonnegativity constraints by arcs of the network.
Activities are Fin (n + 2); start times are real vectors Fin (n + 2) → ℝ with the pointwise order. Durations, capacities and requirements are natural numbers, and time lags integers. The deadline is the arc of weight , which is always present, as §3.1 prescribes. Resource constraints are imposed for every , not only for as (3.1.2) writes; the proofs use the first reading. Extreme points are Mathlib's Set.extremePoints ℝ, maximal points are Maximal for the pointwise order, and components are connectedComponentIn. A local shift carries an explicit continuous map from unitInterval into . Strict orders are asymmetric, transitive relations on . A spanning tree is an arc set of size whose underlying simple graph is connected. Its arcs must be arcs of , resp. of , with their network weights, so an arbitrary equation system does not count.
The schedule classes are defined through shifts and nothing else. Defining "stable" as "extreme point", or "pseudostable" as "local extreme point", would make the goal and Lemma 3.2.8 tautologies, and such encodings are ruled out. Proposition 3.2.16 carries the book's standing convention (§1.2, p. 8) that every node is reached from by a walk of nonnegative length. Without it the statement is false.
The definitions duplicate, under this mission's namespace, the model of the book's Chapter 2 missions (order polytopes, shifts, active classes). They are written to be merged with those once published. Contributions on the geometry of finite unions of polytopes, and on spanning-tree bases of difference constraint systems, are reusable beyond this mission.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve, Cauchy–Schwarz and Schnirelmann's original sumset inequality from the entry, and improves the first moment:
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It is the argument behind the entry, unchanged up to the last step: the explicit Selberg sieve and Cauchy–Schwarz give for , . The only change is to take the smallest admissible in Schnirelmann's inequality: first holds at (rather than the rounded ), so and .
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Consumers judge a price against a reference price, an internal standard formed from the prices they have seen before. A price below the reference feels like a gain and raises demand; a price above it feels like a loss and lowers demand. The effect is documented empirically in marketing and behavioural economics (Kalyanaram and Winer 1995). It forces a pricing firm to plan dynamically: today's price is tomorrow's reference point.
This makes the shape of an optimal price path the practical question. Should a firm launch high and cut prices over time (skimming), launch low and raise them (penetration), keep prices constant, or alternate between high and low? For linear demand models, Kopalle, Rao and Assunção (1996) and Fibich, Gavious and Lowengart (2003) showed that optimal prices move monotonically towards a steady state. Popescu and Wu (2007) study a general, nonparametric reference-dependent demand model. They show that the reference price path always converges monotonically, but the price path need not be monotone: high-low pricing can be optimal even for loss-neutral consumers. They then give three alternative sufficient conditions under which every optimal price path is monotone. This mission formalizes that result, their Theorem 3 (Global Price Monotonicity).
A monopolist chooses a price in each period from the interval , . Consumers hold a reference price that evolves by exponential smoothing with memory :
Demand is . Here is the base demand, and is the reference effect of a perceived gain , with . With zero cost, the per-period short-term profit is . The base profit is , the reference profit is , and is the slope of the reference effect at zero.
With discount factor , the value function is
the supremum over all price sequences in . It satisfies the Bellman equation with
The optimal pricing policy is the largest maximizer of over . The reference price policy is . From , the state path is and the pricing path is . A steady state is a price with .
The standing assumptions are the paper's Assumptions 1–3. Assumption 1: demand is nonnegative, bounded and continuous, decreasing in and increasing in , and is increasing in . Assumption 2: is twice differentiable. Assumption 3: (a) is nonmonotonic and concave; (b) is strictly decreasing; (c) is concave in and supermodular in .
Suppose, in addition, that at least one of the three alternative conditions of Lemma 3 holds:
Then there is a unique steady state . It is the unique solution in of
and for every initial reference price the optimal pricing path is monotone and converges to it:
Theorem 3 limits the optimal strategies to skimming, penetration and constant pricing. It also shows that the paths do not cross: raising the initial reference price shifts the entire optimal price sequence upward. It extends the price-monotonicity results of Kopalle et al. and Fibich et al. from linear additive-difference models to every demand that is convex in the reference price, and to all models when consumers have one-period memory. Without it, a monotone reference-price path could coexist with oscillating prices, and the paper shows by example (its Figure 4) that this happens when the conditions fail.
Formalizing the result produces a reusable Lean account of a deterministic infinite-horizon pricing problem with a continuous state: a sequence-problem value function, a largest-maximizer policy, state and price paths, and steady states. It also yields monotone-comparative-statics arguments applied to a Bellman objective. The paper's proofs are informal: they cite Topkis' monotonicity theorem, a convexity-preservation result of Smith and McCardle, and standard dynamic-programming facts (Stokey, Lucas and Prescott). None of these statements has a machine-checked proof on this platform.
The obvious route does not reach the price path. Monotonicity of gives monotone reference paths, but the price is a difference of two monotone sequences, which need not be monotone. Monotonicity of itself requires to be supermodular in . involves the value function evaluated at , and supermodularity of alone does not carry through that composition. Under (b) the missing ingredient is a curvature property of that is not visible from the Bellman equation. Under (c) it is a lower bound on the second derivative of , which needs to be twice differentiable. The existence of a steady state also needs work. The limit of a monotone state path must be shown to be a fixed point of the largest-maximizer policy. That policy is not continuous in general, so this step requires continuity of and upper hemicontinuity of the argmax, which the paper leaves implicit.
Everything is over . The data are and , with and . The committed conventions:
Set.Icc 0 pbar of the discounted tsum. It is not an arbitrary solution of the Bellman equation.sSup of the argmax set, which is the paper's largest maximizer. Nonemptiness of the argmax is not assumed.r ∈ P ∧ optPrice r = r.Differentiable ℝ d, makes in Assumption 3(b) and in (3) a genuine derivative.Condition (c) is kept as printed. On it can seldom hold, because vanishes as while strong concavity demands . A near-vacuous disjunct only weakens the hypothesis. The theorem's content comes from (a) and (b), and the hypotheses are jointly satisfiable: , , satisfies all of them. A formalization that conjoined the three conditions, or assumed the argmax nonempty or to satisfy a Bellman equation, would be a different and weaker theorem, and is ruled out.
A complete development needs:
Topkis' theorem and the dynamic-programming facts are reusable beyond this mission, and contributions of them as independent lemmas are welcome. The optional condition (c) branch is expected to be the hardest part.
A seller who does not know how demand responds to price must learn it from sales while it sells. Each price it charges earns revenue, and each price also reveals something about demand. Choosing prices that serve both purposes is the learn-and-earn problem of dynamic pricing. Its standard yardstick is regret: the expected revenue lost, over a horizon of periods, relative to a seller who knew the demand curve from the start.
Keskin and Zeevi (Operations Research 62(5), 2014) study linear demand with unknown intercept and slope. They show that no policy can have worst-case regret of order below , and that simple least-squares-based policies attain . They then consider a variant that is common in practice. A seller has charged one incumbent price for a long time and knows the expected demand at that price. Only the slope of the demand curve remains uncertain, and the incumbent price is the only price that carries no information about it. In this variant the achievable regret drops to order . This mission formalizes the lower bound: no policy does better than (Theorem 3 of the paper). Earlier single-parameter models (Broder and Rusmevichientong, Operations Research 2012) assumed the intercept is known exactly, so that the only uninformative price is zero. The incumbent price model instead has a strictly positive uninformative price, and a seller that charges it stops learning.
Prices are chosen from an interval with . The seller knows an incumbent price and an incumbent demand . The unknown slope lies in a compact interval with . The expected demand at is , which is the incumbent price relation . Write the price in period as , where is the price deviation. Demand in period is
where the demand shocks are i.i.d. with .
The single-period revenue of a deviation is . It is maximized at the optimal deviation
The model assumes that the optimal price lies strictly inside for every .
A pricing policy is a sequence of measurable functions. The first price is a constant, and the price in period is a function of the observed history , with values in . A policy never observes or the shocks. The regret of under slope over periods is
The worst-case regret excludes the slopes at which the incumbent price is itself optimal:
The accumulated information is measured by ; the Fisher information of the history about is .
In Lean these objects are Model (with fields l u pHat DHat bMin bMax σ and the standing assumptions), Policy, pricePath, dev, regret, worstRegret, sqErr and expInfo, all in the namespace KeskinZeevi.IncumbentLowerBound; the i.i.d. shocks are the shared definition RobustBooking.Shared.GaussianNoise.
There is a finite positive constant , depending only on the model, such that for every pricing policy and every horizon ,
The constant is not fixed; the statement asserts only the logarithmic rate, uniformly over policies.
Theorem 3 identifies as the minimal asymptotic loss rate of the incumbent price problem. Together with the matching upper bound (Theorem 4 of the paper, a separate mission in this series), it separates two regimes. When both demand parameters are unknown the rate is . When the demand at one strictly positive price is known it is , even though an uninformative price exists and a myopic seller can stop learning. The lower bound is what makes "asymptotically optimal" meaningful for the semi-myopic policies the paper proposes. The paper places it next to the logarithmic lower bound of Broder and Rusmevichientong (2012, Theorem 4.5), whose binary-response model has no uninformative action; the incumbent price model adds one.
The result is proved on paper and, as far as the platform's corpus shows, not formalized anywhere. A formal development would produce a reusable model of history-dependent policies driven by i.i.d. noise, a scalar Van Trees (Bayesian Cramér–Rao) inequality for adaptively collected Gaussian data, and a template for minimax regret lower bounds that quantify over all policies. The companion missions of this series (the lower bound, and the two upper bounds) share the model.
The bound quantifies over every non-anticipating policy, including policies that adapt their exploration to the observed history. A frequentist Cramér–Rao bound does not apply, because a policy's prices are neither unbiased estimators nor fixed designs, and the information depends on the unknown through the policy's own choices. A two-point argument that compares two slopes controls the error at one pair of parameters. It does not by itself give the per-period trade-off between information and pricing error that must be summed over . The set over which the worst case is taken also excludes the slope at which the incumbent price is optimal. The lower bound must therefore come from slopes where the seller is forced to deviate from , and every deviation earns information but also costs revenue.
The model is a Lean structure carrying all standing assumptions as fields: , , , , , and interiority of the optimal price for every . Two of these are corrections that make implicit hypotheses explicit. The first is : p. 1148 calls the uninformative price "within the feasible price domain", and the proof uses . The second is . With the optimal price is known and the theorem is false. The paper's reading is , and is the weaker hypothesis the proof needs.
The optimal deviation is the closed form, which equals the maximizer (21) under the interiority assumption. Policies are deterministic. The rule of period is a Borel measurable map from histories encoded as Fin t → ℝ × ℝ into . The price process is defined by recursion from the shocks on an arbitrary probability space , which realizes the law of the history under and . Lean periods start at (Lean period is the paper's period ). Expectations are Bochner integrals of bounded measurable functions. The worst-case regret is a real supremum over the subtype , which is nonempty and on which the regrets are uniformly bounded. The constant is quantified before the probability space, the noise, the policy and the horizon. A statement whose constant may depend on or , whose supremum is over an empty or unbounded index set, or whose policies can read would be trivially true or false, and none of these is the theorem stated here.
A complete development needs the scalar Van Trees inequality, Fisher information of the Gaussian location-scale history density, measurability of the price process, and harmonic-sum estimates (Real.log against partial sums of ), on top of Mathlib's gaussianReal, iIndepFun and Bochner integration. The Van Trees inequality and the policy/price-process model are reusable beyond this mission. Proofs of the milestones individually, and a general Van Trees inequality in Mathlib style, are welcome.
Airlines, hotels and railways sell a fixed stock of capacity on several resources at once: a passenger flying from Boston to Los Angeles through Chicago uses a seat on two flight legs. Network revenue management decides which requests to accept, and the standard control is a bid price per leg: accept an itinerary if its fare exceeds the sum of the bid prices of the legs it uses. A good bid price is the marginal expected value of one more unit of capacity.
Talluri and van Ryzin (Transportation Science 33(2), 1999) proposed the randomized linear programming (RLP) method: simulate demand scenarios, solve a linear program with perfect knowledge of each scenario's demand, and average the optimal dual prices. Their main result (a companion mission) says the average is an unbiased estimate of the gradient of expected perfect-information revenue when that gradient exists. This mission is about their §3, the case where it does not: when the LP is degenerate with positive probability, the expected revenue has kinks, averaged dual prices estimate only a supergradient, and the right object is the directional derivative. Proposition 2 of the paper computes it as the expectation of an auxiliary LP value, which again gives an unbiased simulation estimator, now one direction at a time.
There are legs and itineraries. The incidence matrix has if itinerary uses leg ; every column is nonzero. Fares are , ; capacities are . For a demand vector , , the perfect-information LP value is
the best revenue obtainable if the demand were known in advance. With a random vector on a probability space , the perfect-information approximation of the value function is .
The Lagrangian of the capacity constraints is
and an optimal vector of dual prices is a minimizer of over . Since is concave on , its superdifferential at is
(the paper calls its elements subgradients). For a direction let
and let be the one-sided directional derivative of . In Lean these are piValue, JPI, lagr, IsDualOpt, superdiff and u in the namespace RLPBidPrice.Directional.
For with every , measurable with almost surely, and every direction ,
No condition on the distribution of is imposed, which is the point: this is the nondifferentiable case.
The result. In the differentiable case the RLP bid prices are the averaged dual prices. When degeneracy has positive probability, which happens for discrete demand and for many network structures, Proposition 2 is what remains true: the marginal value of capacity in any direction, in particular in the direction of an itinerary (the displacement cost of accepting it), is the expectation of a scenario-wise LP quantity. Averaging over simulated scenarios is an unbiased estimator of it. Milestone 3 and Proposition 1 say what the plain RLP average estimates in this case (a supergradient), and why the choice of LP algorithm matters for whether it converges at all.
Formalizing it. The paper's argument is a short paragraph; its printed version is not correct as stated (see the scope section), so a machine-checked proof also settles which version holds. The mission produces a formal theory of the parametric LP value in its right-hand side: concavity, the Lipschitz bound, the identification of its superdifferential with the Lagrangian dual optimal set, and its directional derivatives, together with the interchange of a one-sided limit and an expectation. As far as a search of the platform shows, none of this, and no revenue-management gradient result, is formalized yet; the platform's LP sensitivity theorem is for standard-form LPs with a full-row-rank matrix and does not cover this model.
The pointwise facts are classical convex analysis and LP duality, but they have to be proved for a supremum defined over a polytope, not quoted, and Mathlib has no LP duality theorem in this form. The identification of the superdifferential needs strong duality for the LP with the box , and the box is exactly where the paper's own formula (22) goes wrong: the dual variables of cannot be dropped.
The step from the pointwise derivative to the expectation is a dominated convergence argument for one-sided difference quotients, which needs a bound uniform in and measurability of . The obvious route, differentiating under the integral sign as in the differentiable case, is not available: is not differentiable, and a two-sided limit is false. The measurability of is not given by a formula; it has to come from being a limit of measurable difference quotients.
Capacities, demands and fares are real vectors indexed by Fin m and Fin n; is a real matrix with 0/1 entries and nonzero columns (IsIncidence A); . The paper's remaining-time index is notation only and is dropped. is a real sSup over the feasible objective values: for , it is the LP maximum, and otherwise it is , so every statement assumes or and (almost surely), and the superdifferential is taken over only. Optimal dual prices are defined through the Lagrangian (13)–(14); they are the -parts of the optimal solutions of the LP dual. is a real sInf, which would be on an empty set; for the dual optimal set is nonempty and bounded, so is an attained minimum and the goal is not vacuous. Directional derivatives are one-sided limits (nhdsWithin 0 (Set.Ioi 0)). Expectations are Bochner integrals; no integrability of is assumed or needed, since and are bounded.
The following corrections to the printed text are part of the statements, each with a counterexample to the printed version:
A statement of the goal with the printed (22), or with defined over an arbitrary or empty set so that sInf returns , or with a two-sided limit, is ruled out: the first two are false or vacuous for the reasons above, the third is false.
A complete development needs LP duality for , concavity and the Lipschitz bound of the value function, the directional derivative of a finite concave function on an open set, and dominated convergence (Mathlib's MeasureTheory.tendsto_integral_filter_of_dominated_convergence); Proposition 1 uses ProbabilityTheory.strong_law_ae. The LP duality and parametric value-function results are reusable for any mission about LP-based bid prices or two-stage stochastic programs. Contributions of any milestone separately are welcome.
Airlines, hotels and railways sell fixed capacity on networks of resources. In network revenue management a request for an itinerary that uses several flight legs is accepted or rejected in real time, and the dominant industrial control is the bid-price control: every leg carries a price, and a request is accepted only if its fare is at least the sum of the bid prices of the legs it uses. A good bid price is the marginal expected value of one more seat on the leg, which is a gradient of an expected-revenue function with respect to capacity.
The classical way to compute bid prices, the deterministic linear program, replaces random demand by its mean and reads off the dual prices of the capacity constraints. It ignores all distributional information and gives a zero bid price to every leg whose mean demand is below capacity. Talluri and van Ryzin (Transp. Sci. 33(2), 1999) studied the randomized linear programming (RLP) method instead: simulate demand vectors , solve one linear program per sample with the realized demand as an upper bound, and average the dual prices. Their Theorem 1 asserts that this average is an unbiased estimator of the gradient of the expected perfect-information revenue. For one leg and one fare class it recovers Littlewood's rule, (Littlewood 1972, cited on p. 209 of the paper).
A network has legs and itineraries. The incidence matrix has exactly when itinerary uses leg , and every column is nonzero. Fares are and capacities are a real vector . Demand to come is a random vector on a probability space .
The perfect-information LP value is
the revenue obtainable if the demand were known in advance, and the perfect-information approximation of the value function is . The Lagrangian dual function of the capacity constraints is
and an optimal dual price vector is a minimizer of over . In Lean these are piValue, JPI, lagr and IsDualOpt in the namespace RLPBidPrice.Unbiased.
Two conditions govern the result. Condition C1′: whenever lies in the linear span of a set of columns of (columns of and unit vectors ), that set spans . Condition 2: every distribution function is continuous. The components are also assumed mutually independent.
Under C1′, Condition 2 and independence,
In Lean (theorem1_unbiased_gradient) this is three clauses: is differentiable at almost surely; is Fréchet differentiable at with derivative the expectation of the pathwise derivatives; and for every measurable, almost surely optimal dual selection , has gradient at .
The theorem justifies a widely used method: it says that the simple procedure of averaging simulated LP dual prices targets the gradient of a well-defined expected-revenue function, and by the strong law of large numbers the average is also consistent. It separates the RLP method from the deterministic LP, whose dual prices are gradients of a different function, and it isolates exactly when that justification fails (degenerate LPs with positive probability, discussed in §2.2 of the paper and treated by directional derivatives in its §3).
The printed statement is false, and the formalization records that. Condition 1 of the paper looks only at the columns of and ignores the slack columns of ; the paper's Condition 2 is marginal and does not rule out dependent demands whose sum hits capacity. The corrected statement, with C1′ and independence, is the one this mission targets. No machine-checked version of this result, or of LP sensitivity analysis under random right-hand sides of this kind, is known to exist; formalizing it gives a checked statement of the hypotheses under which the RLP estimator is unbiased.
The pathwise facts are LP duality; the delicate step is the almost-sure uniqueness of the dual prices. Degeneracy of an LP is a condition on finitely many bases, but the set of dual optima depends on , and the natural argument that fixes a direction and shows that has probability zero does not work as written: the direction depends on , and a direction that improves the Lagrangian may leave the orthant . This is precisely where the printed Condition 1 fails. A second difficulty is the passage from almost-sure differentiability of to a full Fréchet derivative of on , with the measurability of the random derivative and of the dual selection.
Legs and itineraries are Fin m and Fin n; is a real matrix with entries in and nonzero columns; capacities are real vectors. The paper's remaining-time index is notation only and is dropped. is a real sSup over feasible objective values; since the feasible set is empty when or has a negative entry (the value is then ), every statement assumes and almost surely, and derivatives are taken where is interior (C1′ forces ). Optimal dual prices are minimizers of the Lagrangian (13) over , which are the -parts of the optimal solutions of the LP dual of (6)–(8). Gradients are Fréchet derivatives on Fin m → ℝ, encoded by the linear functional (gradCLM g). Condition 2 is continuity of ; independence is iIndepFun. is measurable; no integrability of is assumed, since .
Every correction is labelled in the statements. C1 → C1′: with having rows , , and i.i.d. uniform on , Conditions 1 and 2 hold but has one-sided slopes of about and in the second coordinate at . Independence added: with one leg, , fares and , uniform on , the LP is degenerate almost surely. Implicit hypotheses made explicit: , , (Lemma 2's bound needs ), nonzero 0/1 columns.
The goal is not trivialized by a selection: it states the selection-free identity , and the dual-price form quantifies only over measurable selections that are optimal almost surely; it assumes neither almost-sure differentiability, nor almost-sure uniqueness of the dual, nor a joint density, nor nondegeneracy.
A complete development needs LP duality for bounded-variable LPs in Lagrangian form, concave polyhedral functions and their superdifferentials, a finite enumeration of bases of , and differentiation under the integral sign for Lipschitz integrands (Mathlib has hasFDerivAt_integral_of_dominated_loc_of_lip). The LP duality and sensitivity results are reusable for other revenue-management and stochastic-programming missions. Contributions of any milestone, of the counterexamples as formal statements, and of alternative proofs are welcome.
Airlines sell the seats of one flight leg in several fare classes over a booking horizon of weeks. Each time a request arrives, the booking agent must decide whether to sell a seat now at the requested fare or keep it for a later, possibly higher-paying, customer. Real reservations are also cancelled, and some ticket holders fail to show up at departure, so airlines deliberately overbook and pay a penalty when more passengers show up than the airplane can carry. The question this mission formalizes is what an optimal accept/reject rule looks like when all three effects (multiple fares, cancellations, no-shows) are present.
For the model without cancellations and no-shows, Lee and Hersh (Transp. Sci. 27(3), 1993) showed that the optimal rule is given by booking limits: in each period and for each fare class there is a threshold on the number of seats sold, and a request is accepted exactly when the current bookings are below it. Subramanian, Stidham and Lautenbacher (Transp. Sci. 33(2), 1999) extend the model to state-dependent cancellations and binomial no-shows with a convex overbooking penalty. Their §1 shows that booking limits, now depending on both the stage and the fare class, are still optimal. The structural step behind this is the concavity of the value function, in the style of Lippman and Stidham's analysis of admission control to a queue (Oper. Res. 25(2), 1977).
There are fare classes and stages , counting the periods remaining: stage opens reservations, stage is departure. The state is the number of seats reserved. At each stage exactly one event happens:
Accepting a class- request at stage earns . At departure each reservation holder independently shows up with probability (), so the number who show up is . If , an overbooking penalty is paid. Here is non-negative, convex and nondecreasing on , and for , the capacity. Starting empty and accepting at most one request per stage, the states reachable at stage are , and is assumed on that range.
The value functions are defined by the recursion (2)–(3):
The first branch of each maximum is "accept", the second "reject". The booking limit of class at stage is Eq. (7):
with when there is no such . The difference is the opportunity cost of one more booking. In Lean all of this is AirlineYieldMgmt.BookingLimits.Model with Model.U, Model.p0, Model.Standing and Model.bookingLimit.
For every stage , fare class and reachable state ,
The optimal rule accepts a class- request exactly while fewer than seats are booked.
The result. Booking limits are how single-leg seat inventory is controlled in practice. The theorem says this simple class of rules loses nothing, even with cancellations whose rate grows with the number of bookings and with random no-shows at departure. The limits depend on the stage, and they need not be nested across classes (Remark 3 of the paper). The same concavity property identifies as the optimal bid price for the leg. The companion mission (II, equivalent charging) reduces a model with class-dependent refunds to this one-dimensional recursion, so a formal proof of the present goal is the input needed to carry booking-limit optimality over to that model.
Formalizing it. The paper proves neither the concavity induction nor Lemma 1. It cites Lippman and Stidham (1977, Theorem 1) for the first and Shaked and Shanthikumar (1994, Example 6.A.2) for the second. The authors note that the cited induction carries over to their recursion (p. 151), but neither source states the result for exactly this recursion, with its state-dependent cancellation term and range-restricted probabilities. A machine-checked proof would therefore supply an argument the paper only points to, not just its bookkeeping. To our knowledge none of these statements has a machine-checked proof.
The goal follows quickly once milestone 3 is available. The work is in milestone 3. The obvious induction pushes concavity through each term of the recursion. It fails at the cancellation term : a product of a concave nondecreasing function and a concave nonincreasing one is not concave in general, so the term is not concave by itself. The null-event term has the same problem, because its coefficient depends on the state. Only the combination of the two terms, together with on the reachable range, keeps the result concave. That constraint holds only on the range, not for every : in the linear case it fails for large . This interaction between the range and the induction has to be handled with care. Lemma 1 is a separate, self-contained piece of discrete probability about binomial sums.
Fin m; the paper's class is i.val + 1. Stages and states are ℕ; probabilities, fares, , and values are ℝ.Model.U is defined by structural recursion on the stage, for every . Every theorem restricts its hypotheses and conclusions to the paper's range .WithTop ℕ, with ⊤ meaning .Consumers judge a price against a reference price, an internal standard formed from the prices they have seen before. A price below the reference is perceived as a gain and stimulates demand; a price above it is perceived as a loss and depresses demand. Prospect theory (Kahneman and Tversky 1979) adds that losses loom larger than gains of the same size: this is loss aversion. A firm that sets prices over many periods therefore faces a dynamic trade-off, because today's price moves tomorrow's reference price and with it tomorrow's demand.
Popescu and Wu (Operations Research 55(3), 2007) analyze this problem for general nonlinear demand. Earlier work of Kopalle, Rao and Assunção (1996) and of Fibich, Gavious and Lowengart (2003) had treated linear or piecewise-linear reference effects with explicit solutions. Popescu and Wu replace explicit solutions by structural arguments (supermodularity, monotone policies, comparison of value functions), which is what makes the results reusable for any demand model satisfying their assumptions. Their headline result for loss-averse consumers is that the long-run prices form a whole interval rather than a single point, and that optimal prices outside the interval move monotonically to its nearer endpoint.
A monopolist chooses a price from , , in each period . The reference price follows exponential smoothing,
from a given initial reference price . Demand is , where is the base demand and is the reference effect of the perceived gain , so that . The per-period profit (zero unit cost) is , the base profit is , and denotes the slope of at .
For a discount factor , the value function is the supremum of discounted profit over all price sequences in :
The Bellman objective is . The optimal pricing policy is the largest maximizer of over , and is the next reference price. The state path is and the price path is . A steady state is a price with .
The standing Assumption 1 requires to be nonnegative, bounded and continuous, decreasing in , increasing in , and increasing in . For a smooth (loss-neutral) , Assumptions 2–3 require to be twice differentiable, to be nonmonotonic and concave, to be strictly decreasing, and the reference profit to be concave in and supermodular.
Under loss aversion the reference effect is kinked: for gains and for losses . Assumption 4 makes and twice differentiable and increasing in , makes single crossing, and imposes . Assumption 5 requires the gain and loss profits to satisfy Assumption 3. The problems , and are the pricing problem with reference effect , and , respectively, and uses for .
There exist prices such that is the unique steady state of , is the unique steady state of , and
Moreover, the following hold:
In attack order, the milestones are:
The theorem separates loss-averse markets from loss-neutral ones. With a smooth reference effect, Theorem 2 gives one long-run price. Under loss aversion, every price in is self-sustaining: a firm that starts there gains nothing by moving. Prices therefore exhibit stickiness, an interval of rigid prices, which is the dynamic counterpart of the kink in the reference effect. The paper uses this result to derive price monotonicity under loss aversion (its Proposition 4) and the behavior of myopic firms (its Proposition 5).
The result is proved in the paper; nothing here is open. What the mission adds is a machine-checked proof, and that proof has to supply steps the paper passes over quickly. Among them are the existence of steady states in Theorem 2 (the paper argues it in two sentences) and the largest-maximizer bookkeeping when steady states are transferred from to .
The bulk of the work sits in the infinite-horizon dynamic program itself. The value function is a supremum over infinite price sequences. Before any comparative statics can be done, one must show that it satisfies the Bellman equation (2), that it is continuous, and that the argmax is nonempty, so that the largest maximizer is well defined and actually maximizes. The monotonicity of does not follow from supermodularity of alone, because the policy maximizes current profit plus a continuation value evaluated at a state that itself depends on the price.
For the kinked problem, is not differentiable at , so the first-order analysis behind Theorem 1 does not apply to . A first-order condition with one-sided derivatives is the natural first idea. It yields inequalities that every steady state must satisfy, but it establishes neither that steady states exist nor that the whole interval consists of steady states. The set equality also depends on the largest-maximizer convention, since a price that is merely a maximizer of the Bellman objective is not a steady state under the paper's definition.
All declarations live in the namespace ReferencePricing.LossAversion.
d : ℝ → ℝ and reference effects R : ℝ → ℝ → ℝ, with demand d p + R (r - p) r. is a field of Assumption 1.value takes the per-period profit as a parameter and is the real supremum ⨆ over sequences ℕ → Set.Icc 0 pbar of the tsum of discounted profits. It is not a function assumed to solve (2).optPrice is sSup of the set of maximizers in of the Bellman objective, following the paper's largest-maximizer convention. Nonemptiness of that set is to be proved, never assumed.IsSteadyState r is r ∈ P ∧ optPrice r = r.A complete development needs:
The first two are reusable beyond this mission, and contributions of either as general lemmas are welcome.
Airlines, hotels and railways sell a fixed stock of perishable capacity (seats on flight legs, room-nights) to customers who arrive over a finite selling horizon. Network revenue management decides, at each moment, which products to keep open for sale. In the classical independent-demand model each product has its own demand stream. In practice customers choose among the products on offer, and closing a cheap fare shifts some of its demand to a more expensive one. Talluri and van Ryzin (Management Science 2004) modelled this with choice-based demand on a single resource: the firm chooses an offer set , and an arriving customer buys product with probability .
On a network the exact dynamic program has one state per vector of remaining leg capacities, and cannot be solved at realistic sizes. Gallego, Iyengar, Phillips and Dubey (CORC Technical Report TR-2004-01, 2004) proposed replacing it with a linear program over the time allotted to each offer set, the choice-based deterministic linear program (CDLP). Liu and van Ryzin (MSOM 2008) analysed this LP. Their first result has two parts: the CDLP value is an upper bound on the optimal expected revenue, and the bound is asymptotically tight when capacity and horizon are scaled up together. For the independent-demand deterministic LP the analogous statement goes back to Gallego and van Ryzin (Operations Research 1997) and Cooper (Operations Research 2002). This mission targets the choice-based version.
A choice-based network instance has legs and products , and consists of:
and are the same in every period. Each offer set has an expected revenue and a capacity-consumption vector .
The dynamic program. With remaining capacity , an offer set is allowed if for all (no overbooking). The empty set is always allowed. The value with periods left is and
The optimal expected revenue over periods from capacity is (dpValue).
The CDLP. Its variables are times , one for each , and
(cdlpValue).
Scaling. For , the -scaled problems have capacities and horizon . Write and .
for every instance, every and every . It is stated as two Tendsto statements along in .
The goal follows from the three milestones.
The result. Proposition 1 makes the CDLP a certified upper bound on what any control policy can earn, whatever the choice model. Numerical studies use it to benchmark heuristics. Proposition 2 says the bound is exact to first order in large systems, so policies driven by the CDLP solution (time allocations, bid prices from its dual) lose only a vanishing fraction of revenue. It is the justification for the whole family of CDLP-based controls that the paper and later work study (column generation, decomposition, and later the affine and piecewise-linear relaxations of the choice-based network problem).
Formalizing it. The result is proved in the paper. No machine-checked version exists: no revenue-management DP with choice-based demand on a network, no CDLP, and no fluid-limit argument of this kind is on the platform. The existing RevenueManagement material from the Talluri–van Ryzin textbook covers single-resource and dynamic-pricing models. Formalizing the result produces a reusable network-RM DP with an offer-set action space, the CDLP as a Lean object, and a checked asymptotic-optimality theorem that other deterministic-approximation results (independent demand, bid-price heuristics) can follow.
The upper bound compares a stochastic dynamic program with a linear program. The natural route builds a feasible LP point from the optimal policy (expected times each set is offered), but the DP here is a recursion over capacity vectors, not a policy class with a notion of "expected time offered". That connection has to be made from the recursion itself.
The lower bound is harder. The paper's policy offers each set for a fractional number of periods and caps accepted demand at its mean after customers have chosen. Neither is an action available in the DP, where the firm can only pick an allowed offer set each period and must accept whatever the customer picks. The obvious transcription therefore does not type-check against the model: one needs a genuine DP policy whose revenue is while it respects capacity on every sample path. The no-overbooking rule forbids offering a set once any of its products would exceed remaining capacity. Negative revenues are allowed, and may be or .
Legs are Fin m, products Fin n, offer sets Finset (Fin n). The instance is a structure ChoiceNetwork m n carrying (entries in , each or ), , and with the three choice-model axioms. The DP and CDLP use one and one for every period, matching the paper's time-homogeneous model. Capacities and horizon are natural numbers; CDLP times and all values are real. ranges over , because must be a whole number of periods, and the limits use real division by .
is defined by the Bellman recursion (1), which the paper states is equivalent to the stochastic control problem (4). No measure-theoretic policy class is built. The maximization runs over the offer sets allowed at the current capacity, so the DP can neither overbook nor pick products outside an offer set. The paper's boundary condition is not imposed separately: it follows from the recursion whenever every product uses a leg, and imposing it on top could contradict the recursion. is sSup of the objective over the feasible set. That set is nonempty () and bounded (), so the value is the LP optimum.
The goal is the limit equality with both capacity and horizon scaled. A statement with only the upper bound, only capacity scaled, or a DP that ignores capacity or chooses products freely would be a trivializing formalization, and the definitions rule each of these out. Milestone 3 is the paper's conclusion stated on the DP value, not on the paper's informal policy. It is not a repair.
A complete development needs: LP duality or a direct feasibility construction for Proposition 1; the scaling identity for the CDLP; and, for the lower bound, a concrete DP policy together with a law-of-large-numbers or concentration estimate for sums of per-period sales (Mathlib's ProbabilityTheory.strong_law_ae and Hoeffding-type bounds are available). A policy-evaluation lemma that bounds the DP value below by the expected revenue of any feasible offer-set policy is reusable beyond this mission, as is the CDLP scaling lemma. Contributions to either are welcome.
Retailers that sell many substitutable products must set all their prices at once, and a customer's reaction to one price depends on what else is on the shelf. The nested logit model captures this by grouping similar products into nests, so that raising one price shifts demand mostly to close substitutes. The -level nested logit model extends the familiar two-level version to a whole taxonomy tree of depth (for example category → brand → size). It is consistent with random utility maximization (McFadden 1978) and is widely used in demand estimation.
Pricing under logit-type models is harder than it looks. Already for the multinomial logit model, which is the one-level case, Hanson and Martin (1996) point out that the expected revenue is not necessarily concave in the prices. For the two-level nested logit, Gallego and Wang (2014) show that the expected revenue is not concave and can have several local maxima. Li, Rusmevichientong and Topaloglu (Oper. Res. 63(2), 2015) treat the general -level model. Their pricing result, Theorem 7.3, is the target of this mission. It shows that a simple gradient-free iteration, the push-up-then-push-down (PUPD) algorithm, produces prices that converge to a stationary point of the expected revenue.
The products are the leaves of a rooted tree , all at depth . A further leaf, node (the no-purchase option), hangs directly from . Every other node is a nonleaf node with a nonempty set and a parameter . The standing assumptions are for nonleaf and . Each product carries parameters and , and node carries .
Given a price vector , where the no-purchase price is fixed at , the preference weights are computed bottom-up:
The expected revenues are , , and
at a nonleaf node. The expected revenue of is . A customer walks down from , choosing a child with probability proportional to its weight. The probability of ending at product is the product, over the levels , of , where is the ancestor of in level .
Top-down, the scalars are and . A stationary point of is a price vector at which the gradient of is zero.
The PUPD algorithm starts from . Given , it sets and, for every other nonleaf node,
It then updates for every product .
The whole sequence converges and its limit is stationary. No rate is claimed, and none is asked for.
The result itself. Theorem 7.3 turns a nonconcave, many-product pricing problem into an iteration that needs no gradient evaluations and no step size. Each iteration costs one bottom-up and one top-down pass over the tree. The paper's numerical experiments (§8) report that it reaches a stationary point much faster than gradient ascent. Lemma 7.1 gives the gradient of the expected revenue in closed form for any depth. Corollary 7.2 turns stationarity into a fixed-point equation in the prices, which is what makes a price-update scheme like PUPD natural.
Formalizing it. The proofs of Lemma 7.1 and Theorem 7.3 are in the paper's online Appendix E. The acknowledgments (pp. 340–341) record that an error found in an earlier version led to a new proof that the revenues under the PUPD algorithm are always bounded. A machine-checked proof would settle the convergence claim independently of that history. No nested logit or multinomial logit pricing result, and no part of this one, has a machine-checked proof on Prove2Me.
Lemma 7.1 is a chain-rule computation through a tree of power means, and it is technical rather than deep. The hard part is Theorem 7.3. The obvious fixed-point iteration suggested by Corollary 7.2 is not the algorithm. PUPD replaces by the scalars , which involve a maximum, and the update direction is in general not parallel to the gradient. So neither contraction arguments for the plain fixed-point map nor the standard ascent analysis of gradient methods applies directly. is not concave and may have several stationary points, so convergence of the whole sequence, not only of a subsequence or of the gradient norms, is the substance of the claim.
The node type is Option (Fin n) ⊕ Inner. Sum.inl (some l) is product , indexed by
Fin n, so the paper's products are . Sum.inl none is node .
Inner is a finite type of nonleaf nodes containing root, with a parent map into Inner
and a level function that encodes the levels. Every nonleaf node has a child. Prices are
Fin n → ℝ, so node has no price coordinate, and all products are priced (there is
no assortment decision). The conventions:
Real.rpow. Since ,
and it is never used. Division is Lean's, but every denominator is positive under the
standing assumptions.HasDerivAt of
with at . "Stationary point" is HasFDerivAt R_root 0 p (the gradient is
zero). This is the unconstrained gradient, as on p. 335, with no boundary condition, and
it is the same notion in Corollary 7.2 and in the goal.pupd) with and the max-based
, and . The goal is not stated for
an arbitrary start point or for the -based iteration.A trivializing formalization is ruled out: convergence is Filter.Tendsto of the full
sequence to a point at which HasFDerivAt holds with derivative . It is not a statement
about limit points, gradient norms, or an arbitrary sequence satisfying a hypothesis.
A complete development needs derivatives of Real.rpow compositions over a finite tree,
positivity of the weights and choice probabilities, and a convergence argument for the PUPD
iteration. The weight and revenue recursions over a finite rooted tree could be reused for
the assortment half of the same paper and for other tree-structured choice models.
Contributions to any milestone, and alternative proofs of Lemma 7.1, are welcome.
This mission formalizes J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651 (doi:10.4171/GGD/201; arXiv:0905.1118v7, whose page numbers are used): if Thompson's group has Følner sets at all, they are larger than any tower of exponentials.
Whether Thompson's group is amenable is a long-standing open problem, the goal of the F-amenability mission on this platform. By Følner's criterion a finitely generated group is amenable exactly when it has Følner sets, finite sets almost invariant under translation by the generators, of every precision. Moore's theorem is unconditional: for every finite symmetric generating set there is a constant such that every -Følner set has at least elements, a tower of exponentials. If is amenable, its Følner function therefore outgrows every tower, and would answer negatively Gromov's question whether some primitive recursive function dominates the Følner functions of all amenable finitely presented groups (Moore's Question 1.2, from Gromov 2008, p. 578).
Timeline.
Thompson's group (CannonFloydParry.F, published) is the group of order-preserving homeomorphisms of that are piecewise linear with finitely many breakpoints, all dyadic rationals, and all slopes powers of . Moore multiplies elements as " followed by "; that group, the opposite of the group of maps under composition, is MooreF, and it acts on the right.
A finite set is -Følner with respect to a finite (IsFolnerSet Γ A ε) when , where . The tower function is , (ThompsonAmenability.towerExp, published). The Følner function (folnerFunction) is the least size of a -Følner set, and if there is none.
The proof works with finite rooted binary trees, recorded as the sets of addresses of their leaves (IsTree), on which acts partially by acting on the addresses (treeAct), and with weighted Følner sets and marginal sets for partial actions of a group (IsWeightedFolner, IsMarginal). These are defined in the two definitions items.
For every finite symmetric generating set of there is such that, for every ,
The goal is the published F-amenability milestone ThompsonAmenability.exists_const_forall_isFolner_le_card, for the product of maps by composition and left translates; a milestone states the same theorem in Moore's conventions, and another states its second sentence, that is not eventually dominated by any .
Every numbered result of §§3–5 (Lemmas 3.4, 3.5, 3.9–3.12, 3.14, 3.15, 4.1, 4.2, 5.2, 5.4, 5.5, 5.7, 5.9, 5.10, 5.12, 5.13, Remark 3.8 and Claim 5.14), the unnumbered facts about trees and tree diagrams stated in §2, and the word-length bound Moore cites from Burillo, Cleary and Stein.
The result. The theorem constrains any proof that is amenable: Følner sets of , if they exist, cannot be found by any search whose size is bounded by a tower of fixed height. If is amenable, it answers Gromov's question negatively. If is not amenable, the bound is vacuous but its method, controlling how Følner sets distribute over tree diagrams, is one of the few quantitative tools on the problem.
Formalizing it. None of the paper is formalized. The general theory of §3 (partial actions, weighted Følner sets, marginal sets) applies to any group acting partially on a set and is reusable; the partial action of on binary trees is the natural model for combinatorial arguments about .
The difficulty is quantitative. A Følner set is defined only by an inequality between counts, and nothing in that inequality forces its elements to be large; yet the bound must hold for every Følner set, with a single constant for all , while the height of the tower grows with . Any argument can therefore afford to lose only a constant factor in the Følner constant for each level of the tower.
Lean representation and conventions.
(CannonFloydParry.F)ᵐᵒᵖ, so products and right translates match the paper; the goal is stated for CannonFloydParry.F with left translates.List Bool). Tree diagrams, their maps on sequences, equivalence and reducedness follow Moore's §2; a tree diagram describes an element of the published through the dyadic intervals of its leaves, and Moore's sentence defining as the reduced tree diagrams is a milestone.Option-valued function, and the action of is defined on all finite sets of sequences; on trees it is Moore's action.What is left out, and deviations.
What a development needs. Tree diagrams, normal forms and generation of are published and proved on this platform (the Cannon–Floyd–Parry missions on tree diagrams and the normal form and the two presentations of ); Følner's criterion is published by Garrido's first mission. New are the combinatorics of binary trees as leaf sets, the bridge between them and the published tree diagrams, and the theory of §3. Proofs of any milestone are welcome.
Among queueing control problems, a small class admits efficiently computable optimal policies: a single server choosing among several customer streams (Klimov 1974). These problems can be recast as multi-armed bandit problems, whose optimal policies are given by Gittins indices (Gittins 1979), and those indices are computable in polynomial time. The most studied generalization that could have extended this tractability is the restless bandit problem of Whittle (1988), in which bandits that are not played also change state and incur cost. Whittle's index heuristic and its asymptotic optimality (Weber and Weiss 1990) made the model a standard tool in scheduling, sensor management and resource allocation.
Papadimitriou and Tsitsiklis (1999) settled whether restless bandits are as easy as ordinary bandits. Their Theorem 4 shows that finding an optimal policy is PSPACE-hard, even when every transition is deterministic. The same paper shows that general queueing network control is EXP-complete (Theorem 1, the subject of a companion mission).
A restless bandit instance with deterministic transition rules consists of:
A policy is a map . At each time it plays the bandit ; then and for every . The cost at time is
and the average cost of is
The classical multi-armed bandit is the case , . The paper's general model has transition probability matrices; the deterministic case is a special case, so hardness for it implies hardness in general.
The decision problem RESTLESS BANDITS asks whether there is a policy with .
Problems are sets of instances, and instances are bit strings under a fixed binary encoding. A problem is in PSPACE if a multi-stack Turing machine decides it on every input using a number of stack cells polynomial in the input length. It is PSPACE-hard if every PSPACE language reduces to it by a polynomial-time many-one reduction: a map computable in polynomial time that sends yes-instances to yes-instances and no-instances to no-instances. It is PSPACE-complete if it is also in PSPACE.
The proof starts from an auxiliary problem, CIRCULAR-TAPE HALTING. The input is a circular tape with squares holding values in , a rule with , and an initial configuration . At time the head points at the square , replaces its value by and moves on; every other square keeps its value. The process halts if at some time every square holds . The question is whether the process halts.
In Lean: PSPACEHard Instance.enc restlessBandits. Every language in PSPACE reduces to the decision problem in polynomial time.
In Lean: PSPACEComplete TapeInstance.enc circularTapeHalting, meaning the problem is in PSPACE and PSPACE-hard. The paper claims completeness at this point. The goal uses only the hardness half.
In Lean: PolyReduces TapeInstance.enc circularTapeHalting Instance.enc restlessBandits. This is the existence of a polynomial-time reduction. It is not a statement about the specific construction in the paper.
The result. Theorem 4 shows that the index theory of multi-armed bandits does not extend to restless bandits. The index-based approach has no efficient exact counterpart unless P = PSPACE, even with no randomness at all. It is why the restless-bandit literature works with heuristics (Whittle's index) and asymptotic optimality results, not exact polynomial-time algorithms. It is also one of the standard hardness results cited for average-cost Markov decision problems whose state space is a product of many small components.
Formalizing it. The paper's argument is informal. It assumes the simulation of polynomial-space machines by circular-tape processes, and it describes the bandit construction in prose. A complete formalization produces a machine-checked PSPACE-hardness proof for a controlled-dynamics problem. It also produces a reusable space-bounded computation layer on Mathlib's Turing machines, which has polynomial time but no space measure. No part of this result has a machine-checked proof yet.
The obvious first idea is to encode a space-bounded machine's configuration in the bandits' joint state. The difficulty is that a policy sees only the product state and plays exactly one bandit per step. The rules and are shared by all bandits, so no bandit knows its own index. The reduction also has to be exact for the average-cost criterion. A policy that simulates the computation correctly for a long but finite time, then deviates, must not reach average cost zero. A policy that halts must reach it. Milestone 1 needs its own work as well: a polynomial-space machine has to be recast as an in-place computation on a circular tape whose local rule sees only a square and its predecessor.
Conventions fixed in Lean:
01), sign-magnitude integers, (numerator, denominator) rationals, and tables listed in index order after their dimensions. The encoded length is polynomial in the instance's bit size and vice versa. Mathlib's Encodable/Nat.pair encodings are not used.Turing.TM2ComputableInPolyTime. PSPACE is defined here: a Turing.FinTM2 that halts on every input with the correct output bit, and in which every reachable configuration has total stack length at most . The input stack is counted.limsup of . The running averages are bounded, so the limsup has no junk value.Fin n, Fin M, Fin n, Fin A (0-based). Square is index , and the value is index .Excluded trivialization. The goal quantifies over every PSPACE language and asks for a reduction computable in polynomial time on a compact encoding. Exhibiting one hard instance, stating the correctness of the paper's construction for the constructed instance, or measuring against a padded encoding would not prove Theorem 4.
Theorem 4 is stated as hardness only. The proof's last sentence and the introduction say "PSPACE-complete", but membership in PSPACE is not argued in the paper.
Infrastructure. A complete development needs: closure of polynomial-time TM2 computations under composition, which gives transitivity of and turns the two milestones into the goal; a space-bounded simulation of TM2 machines by circular-tape processes; and the bandit construction with an average-cost analysis of eventually periodic deterministic trajectories. The encoding and PSPACE layer can be reused by any complexity result on the platform. Contributions to the polynomial-time composition lemmas are especially welcome.
Multiclass queueing networks model manufacturing lines, computer systems and communication networks. In these systems jobs of several types move between shared resources, and a controller decides where to send a job next (routing) and which waiting job a free resource works on (sequencing). The central design question is to find a control policy that maximizes long-run throughput. For decades this was attacked with heuristics, approximations and performance bounds (Walrand 1988; Bertsimas, Paschalidis and Tsitsiklis 1994; Kumar and Kumar 1994, all cited in the introduction of Papadimitriou and Tsitsiklis 1999). No general exact algorithm faster than solving a Markov decision process over all network states was found.
Papadimitriou and Tsitsiklis (1999) explained why. For closed networks with exponential service times, computing an optimal policy is EXP-complete, and therefore provably requires exponential time, independently of whether P equals NP. The paper describes this as, in its authors' experience, the first intractability result of this strength for a practical optimization problem that had been attacked for decades. This mission formalizes that theorem, Theorem 1 of the paper.
A network of queues has a finite set of customer classes and a finite set of servers. Each class has a single server that can serve it, a mean service time and a weight . Service times are independent and exponentially distributed with the prescribed mean. The classes are partitioned into and . When a class- customer completes service it changes to a new class : the controller chooses from a given nonempty set if , and is drawn with given rational probabilities if . The network is closed: no customer arrives or leaves.
The state records the number of customers of each class waiting, and the class (if any) being served at each server. A policy makes decisions as a function of the current state. At time and at every service completion it routes the completing customer (if its class is in ), and then lets each free server either idle or start a waiting customer of one of its own classes. Service is nonpreemptive. Under a fixed policy the state evolves as a continuous-time Markov chain. Let be the number of class- completions up to time from the given initial state. The weighted throughput is
NETWORK OF QUEUES is the decision problem: given all these data (with the initial counts in binary) and a rational , is there a policy with ?
EXP is the class of problems solvable in time for a polynomial , on inputs of length . A problem is EXP-complete if it lies in EXP and every problem in EXP reduces to it by a polynomial-time many-one reduction.
The reduction source in the paper is STOCHASTIC IN-PLACE ACCEPTANCE (SIPA). A stochastic Turing machine has nondeterministic and stochastic states, each with two continuations. Its computation tree is evaluated bottom-up, taking the maximum at nondeterministic nodes and the average at stochastic nodes, and the machine accepts if the value exceeds . SIPA asks, for a machine and an integer in unary, whether accepts zeroes without leaving the input squares.
In Lean, EXPComplete Instance.enc networkOfQueues. The problem is in EXP, and every language reduces to it in polynomial time.
Milestones 2 and 3, Lemma 1, and the transitivity of polynomial-time reductions together give the goal.
The result. Theorem 1 separates what can be computed exactly for queueing networks from what cannot. Since EXP strictly contains P by the time hierarchy theorem, no algorithm computes optimal throughput policies for all closed exponential networks in polynomial time. Unlike NP-hardness, this is unconditional. The result justifies the literature's turn to approximations, bounds and asymptotic regimes, and it motivated the complexity analysis of restless bandits in the same paper. The stochastic-machine characterization of EXP, polynomial space with stochastic and nondeterministic states, is a tool of independent interest.
Formalizing it. The theorem is proved on paper, with a reduction that the paper itself presents in sketched form. It has no machine-checked proof. The formal work includes an exponential-time Markov decision process solver expressed as a Turing machine, a simulation of alternating polynomial-space machines by stochastic ones, and the queueing-network gadget with its optimality argument. It also produces a reusable layer: EXP and polynomial-time reductions over Mathlib's Turing.FinTM2, and a controlled continuous-time Markov chain for closed queueing networks.
The membership half needs an exponential-time decision procedure for the average-reward criterion. This is a multichain Markov decision process with instantaneous transitions, and it must be implemented and timed on an actual Turing machine rather than argued about informally. The hardness half is harder. The network has to encode a stochastic machine's configuration. In the paper, one customer per tape square carries the square's bit and a single test customer carries the machine's state and head position. The weights are chosen so that an optimal policy is forced to simulate the machine faithfully. The paper argues optimality through the average-reward optimality equation with explicit error bounds, and it states several steps (the normal forms of the machine, the padding to linear space) as standard. Every one of these has to be made precise. Finally, composing reductions needs the composition of polynomial-time Turing machines, which Mathlib states only as proof_wanted TM2ComputableInPolyTime.comp.
All declarations are in the namespace OptimalQueuingComplexity.Network. The following conventions are fixed:
Fin nC and servers Fin nS. SIPA's is in unary. Encodable and Nat.pair are not used: their exponential padding would make membership in EXP trivial.ProbabilityTheory.expMeasure). The is taken in EReal. The inequality is strict.TM2ComputableInTime with time bounded by . Reductions are TM2ComputableInPolyTime. Hardness quantifies over every EXP language, not over one constructed instance.A statement about the paper's specific gadget (its servers, router and weights) is a proof step and not a target. Contributions welcome beyond the targets include composition of polynomial-time machines, a decision procedure for finite average-reward MDPs, and structural facts about the throughput (finiteness under well-formedness, attainment by stationary policies).
Average cost Markov decision chains model systems that run indefinitely and are judged by their long-run cost per step: admission and routing control in queues, inventory replenishment, machine maintenance. For a finite state space the classical tool is the average cost optimality equation (ACOE)
whose solution gives both the minimum average cost and an optimal stationary policy. To be useful the equation has to be solved numerically, and the method used in practice is value iteration: compute the minimum -horizon costs and extract and from their growth. This mission formalizes Sections 6.4–6.6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037): when the minimum average cost is constant, the ACOE holds, any solution of it is optimal, and value iteration converges, provided the optimal policies are aperiodic. When they are not, a transformation of the model makes them so.
Related classical work includes Blackwell's discrete dynamic programming (1962) and Schweitzer–Federgruen's analysis of undiscounted value iteration (1977); Sennott's treatment derives the ACOE from the discounted value function as , which is the route that extends to countable state spaces in later chapters of the book.
A Markov decision chain (MDC) has a finite state space ; in each state a finite nonempty action set ; nonnegative costs ; and transition probabilities . A policy may use the whole history and randomize; a stationary policy always chooses in state and induces a Markov chain with transitions .
For a policy and initial state : is the expected cost of the first steps, the expected -discounted cost, and the average cost. The value functions are the infima over all policies: , and the minimum average cost . A policy is average cost optimal if .
Section 6.2 of the book provides a stationary policy that is discount optimal for all close to (a Blackwell optimal policy), and Section 6.3 builds from it a relative value function . For a distinguished state put
For a distinguished state the finite horizon relative value function is .
A positive recurrent class of a Markov chain is aperiodic if for , where is the steady state distribution. Assumption OPA ("optimal policies are aperiodic") requires every positive recurrent class of every average cost optimal stationary policy to be aperiodic. The aperiodicity transformation with keeps states and actions, scales costs by , and sets for , .
If and Assumption OPA holds, then for any distinguished state
solves the ACOE, and every limit point of the finite horizon optimal stationary policies is average cost optimal.
The ACOE with constant is the standard certificate of optimality for finite average cost models, and Proposition 6.5.1 is what allows any numerical solution of it to be trusted. Proposition 6.6.3 is the correctness theorem of the value iteration algorithm (VIA 6.6.4 of the book), and Proposition 6.6.6 removes its one extra hypothesis at the price of a model transformation. Chapter 8 of the book runs this algorithm on a sequence of finite truncations to compute optimal policies for countable-state queueing models, so these results are the base of the book's computational method.
All results in this mission are proved in the book; none has a machine-checked proof. Existing formalizations on the platform treat average reward models under a unichain hypothesis with a single action set type; this mission assumes only a constant minimum average cost (multichain models allowed) and uses the general policy class throughout.
The ACOE itself is not the obstacle; convergence of is. Theorem 6.4.2 bounds but does not make it converge, and Example 6.6.1 of the book (a two-state periodic chain) shows that without aperiodicity oscillates. The naive argument, passing to the limit in the finite horizon optimality equation, assumes the limits exist, which is exactly what is in question. Chain structure is the obstruction: a multichain optimal policy has several recurrent classes, and the Cesàro-type convergence that suffices for the ACOE itself is weaker than the pointwise convergence value iteration needs. The policy statement is also delicate, since the finite horizon minimizers need not converge.
S is finite ([Fintype S]); actions are a type Act with per-state nonempty Finset action sets. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞, and all value functions are defined in [0,∞] as infima over all history-dependent randomized policies, then converted to ℝ (they are finite for finite ).min_a is Finset.inf' over . Limit points of policy sequences follow Definition B.1 (a subsequence agreeing eventually in every state). Finite horizon optimal policies are any minimizers of .In many inventory systems, demand that cannot be met from stock is lost rather than backordered: a customer who finds the shelf empty buys elsewhere. For such lost-sales systems with positive lead times the optimal replenishment policy is known to be complex and to depend on the whole pipeline of outstanding orders (Karlin and Scarf, 1958; Morton, 1969). In practice, firms nonetheless use base-stock (order-up-to-) policies, which reorder every period whatever was sold. Choosing such a policy comes down to choosing one number, the base-stock level . How easy that choice is depends on how the expected cost behaves as a function of .
Earlier work had established convexity in for backordered demand (Healy, 1992, for policies) and for lost sales with deterministic lead times (Downs, Metters and Semple, 2001). Nahmias (1979) observed in simulation that the cost surface looked convex for lost-sales systems with random lead times, but had no proof. Janakiraman and Roundy (2004) proved convexity for lost-sales systems whose lead times are stochastic but do not cross. On every sample path this holds when holding cost is charged only on the inventory position. In expectation it holds for the full cost under the lead-time model of Kaplan (1970). This mission formalizes the finite-horizon part of that paper (Sections 3–4).
Periods are indexed . The demand in period is . The order placed in period has a lead time and arrives in period . The arrival index is
the index of the latest order that has arrived by period , with when no order has arrived (in particular ). Assumption 1 (orders do not cross) requires to be weakly increasing in .
Under an order-up-to- policy, the system starts with units on hand and nothing on order. Each period it orders what was sold in the previous period. With orders , the quantities of period are:
For a discount factor and cost rates , the discounted cost (3.1) is
Here is charged on the inventory position (on hand plus in transit), on stock physically on hand, and on each lost unit.
In the Kaplan lead-time model (Assumption 2) the arrival index is random: and for , where is an i.i.d. sequence of nonnegative integer-valued random variables. The same dynamics, driven by , give random quantities , , and . is the expectation over with the demands held fixed.
Under Assumption 2, for every realization of demands , every and all ,
Theorem 5 shows that, when the only holding cost is charged on the inventory position, the discounted cost of every noncrossing sample path is convex in . It therefore stays convex under any distribution of noncrossing lead times and any demand process independent of them. Theorem 8 extends convexity to storage costs on stock on hand, which matter whenever payment is due on arrival. A sample-path statement cannot do this. On a sample path the extension fails: the paper's Example 1 exhibits a concave kink at when . Both results make the choice of the best base-stock level a one-dimensional convex minimization, so bisection or simulation-based search methods are guaranteed to converge to a global optimum. The paper's Example 2 shows that noncrossing cannot be dropped.
The results are proved in the paper. As far as is known, none has a machine-checked proof. A formalization adds a precise, reusable model of periodic-review lost-sales dynamics with stochastic lead times, and a checked account of exactly which hypotheses (noncrossing, on sample paths, the Kaplan structure in expectation) each convexity claim needs.
Individual per-period quantities are not convex: , , and are piecewise linear with slopes in and are neither convex nor concave in . The obvious approach, proving each term of the cost convex and summing, therefore fails. Convexity appears only in the weighted sums, and only for nonnegative, weakly decreasing weights. The recursion defining refers back to earlier orders through a window that moves with the lead-time path, so an induction on has to carry a family of weight sequences rather than one fixed sum.
In expectation, the storage-cost term is not convex path by path. Convexity of its expectation depends on the distributional structure of the Kaplan model, namely that the lead time of the order placed in period is independent of the state of the system at that time. Stating this correctly requires a genuine probability space, not a sample-path argument.
orderQty, onHand, sales, endOnHand, invPosition, lostSales). The sample-path results use arrivalIndex L (via Nat.findGreatest). The Kaplan results use kaplanIndex ρ, the recursion of Assumption 2 with . The discounted cost (3.1) is discountedCost.MonotoneOn (fun n => n + L n) (Set.Iic N). Demands satisfy for . Weight sequences are β : ℕ → ℝ with 0 ≤ β n and Antitone β. Costs satisfy and , the paper's Section 3 standing assumptions. "Increasing" and "decreasing" are weak, as the paper states.ConvexOn ℝ (Set.Ici 0) / ConcaveOn ℝ (Set.Ici 0): the base-stock level is an initial stock, .iIndepFun ρ P, and IdentDistrib (ρ n) (ρ 0) P P for all . is the Bochner integral . For the integrands are bounded and depend on finitely many coordinates, so they are integrable and the integral is the paper's expectation. Measurability of is the field's standing convention.ConvexOn/ConcaveOn), integrals of bounded functions of finitely many independent discrete variables, and the independence and identical distribution facts of the Kaplan model. The dynamics and the Kaplan index are reusable for any further analysis of base-stock lost-sales systems, including the paper's infinite-horizon results. Proofs of the milestones in any order are welcome, as are auxiliary lemmas identifying the Kaplan index as the arrival index of a noncrossing lead-time path.The 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. The question is how large a comparison constant is needed to make this inequality hold.
For every real , the optimal Hlawka constant for complex diagonal matrices is already proved in Lean. This mission asks whether that same constant works for all complex matrices, including rectangular ones. The statement is a conjecture. Accepted diagonal result
Audenaert and Kittaneh's Problem 7 asks for the best constant in the Schatten-norm setting, if one exists. Existence of some finite dimension-independent constant for every real is already settled by the project's Lean theorem. The task here is to establish the specified sharp candidate in the range . Audenaert–Kittaneh, §8.2, proved existence result
For a complex matrix with singular values , its Schatten norm is
There is no normalization by dimension. For three matrices of the same shape, define
Formal Schatten-norm definition
The shared cyclic candidate is
The fraction is the deficit ratio for the coordinate triple . For , its denominator is positive on the displayed interval and the supremum is attained. Cyclic definitions and attainment
The goal asks whether for every real and every triple of complex matrices of every finite shape. One constant for each exponent must work across all dimensions and triples. The endpoint 256, noninteger exponents, zero dimensions, singular and zero matrices, unequal norms and zero pair deficit are included.
Lean states the goal for complex-linear maps between any two finite-dimensional complex inner-product spaces, allowing different dimensions. No positivity, self-adjointness, commutativity or common diagonalization assumption is imposed.
The singular values determine a matrix's own norm. However, the separate singular-value lists of three matrices do not determine the norms of their pair sums and total sum. The diagonal theorem therefore does not supply the seven matrix norms needed in this inequality. Their relative directions matter as well.
The existing existence theorem supplies a constant, but does not identify it with . A proof here needs the exact cyclic constant. A proof only for even integer exponents or a restricted class of matrices would not settle this goal.
If the conjectured bound holds, it is automatically optimal uniformly over all finite matrix shapes: diagonal three-dimensional examples already require at least . Thus the missing step is that this constant works for arbitrary matrices. A counterexample would show that the diagonal constant is insufficient somewhere in the stated range. Cyclic lower bound, diagonal Schatten identity
Either outcome addresses this range of exponents; it would not settle the optimal general-matrix constant for every .
The foundation mission establishes the optimal diagonal constant for every real . The cutoff-90 mission has since extended the diagonal result in Lean to every real . The diagonal campaign invites contributors to lower that cutoff below 90.
This mission keeps and asks whether the same optimal constant works for arbitrary complex matrices, including rectangular ones. It can be pursued independently of improvements to the diagonal cutoff.
Its three linked milestones are already-proved background: existence, the sharp diagonal result, and the diagonal norm identity. The main general-matrix goal remains open. No complete proof is supplied for it.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b.
Existence and diagonal librariesThe r-algorithm of N. Z. Shor is a variable-metric method for minimizing functions that are not differentiable everywhere, such as maxima of smooth functions, penalty functions and Lagrangian dual functions of integer and decomposition problems. It combines a subgradient step with a space dilation along the difference of two successive almost-gradients, and the book reports it competitive with the best variable-metric and conjugate-gradient methods on "gully"-shaped test problems (Shor 1985, §3.6, pp. 68–77). Its convergence theory is limited. Section 3.7 of Shor's book gives a convergence proof only for an idealized version with exact directional minimization, on a class of piecewise smooth functions, and the book itself calls a weakening of the assumptions and rate estimates desirable (p. 85). This mission formalizes that section.
Timeline. Shor and Zhurbenko introduced the r-algorithm in 1971 (Kibernetika, no. 3, 51–59). Shor analysed the convergence of its exact-line-search version in 1975 (Kibernetika, no. 4, 48–53). Section 3.7 of the 1979 Russian monograph, translated in 1985, gives that analysis for piecewise smooth functions. The book states on p. 85 that weaker assumptions and rate estimates would be desirable.
Let be -dimensional Euclidean space with inner product , . For a unit vector and the operator of space dilation is .
Widths. For a compact convex set and a unit vector , the width in direction is . The width is and the diameter is . With put (or when ) and .
The class . is partitioned into closed sets , each the closure of its interior, whose interiors are disjoint and homeomorphic to an open ball or open halfspace; is continuously differentiable on an open set containing ; and on . At a point , the set of almost-gradients is the set of gradients of the pieces with . For , is the closed convex hull of all , , together with the -balls around the elements of .
The -algorithm. Fix , . Start from , and a nonsingular . At iteration choose with ; set , , , , , and with such that does not increase along the step and some almost-gradient at makes a non-acute angle with in the transformed metric. The standing assumption is as (3.50).
Assume (3.50) and (3.52). If is an isolated local minimum, the component of containing also contains , and no other point of that component has linearly dependent , then
Theorem 3.13 is the only convergence theorem the book gives for the r-algorithm. Theorems 3.11 and 3.12 hold for any function of the class , convex or not, and say that iterates of the exact version cannot stall at a point where the local almost-gradients are linearly independent: linear dependence of is a generalized stationarity condition that includes . Lemmas 3.2 and 3.3 are statements about widths of convex bodies under linear maps and single dilations, and apply to any analysis of space-dilation methods, including the ellipsoid method.
All four results and the goal are proved in the book, the goal as a corollary without a written proof. None of them is formalized. The formalization adds a machine-checked definition of the class and of the algorithm as a relation on sequences covering every admissible choice of almost-gradients and stepsizes, a verified proof of the book's argument, and a check of the corollary step, which the book leaves to the reader.
The obvious argument for descent methods is that the function value drops by a fixed amount at every step unless the gradient is small. That argument fails here. The r-algorithm can make null steps, with while and change, and its steps are measured in a metric that degenerates as the dilations accumulate (). A small step does not certify near-stationarity, and a large accumulated dilation does not certify progress.
The difficulty is to relate the geometry of the transformed almost-gradient sets to the decay forced on . This needs width estimates for convex bodies under linear maps and single dilations, which Mathlib does not have. Theorem 3.12 also needs a uniform lower bound, near a compact level set, on the Gram determinants of the piece gradients, and the book's proof of it is only sketched. Theorem 3.13 is stated as a corollary with no proof at all. Deriving it requires showing that the iterates cannot leave the prescribed component of , and that their accumulation points reduce to .
EuclideanSpace ℝ (Fin n) with ; operators are continuous linear maps; is the adjoint. and are valued in , so is represented exactly. Widths are sInf/sSup of support values, equal to the book's minima and maxima on nonempty compact sets.The question of the largest area that can be moved around a corner has been studied since the late 1960s. Leo Moser posed it in 1966, and F. H. Hammersley gave the lower bound and the upper bound in 1968. Joseph Gerver constructed a shape of area approximately in 1992 and described four constants , , , satisfying four equations, from which the shape is built. Dan Romik rewrote those equations in exact form as equations (1)-(4) in 2018 and reported high-precision values of the constants. Jineon Baek proved in 2024 that Gerver's shape is optimal: no larger shape can be moved around the corner. The proof was autoformalized in Lean 4 by Dean Cureton and AI agents in 2026, as the repository deancureton/MovingSofa, building on Dawid Trela's formalization of Gerver's constants and motion, Jonathan Ho's Brunn-Minkowski development, the Jordan-curve developments of R. Kirov and the TauCeti project, and Google DeepMind's formal-conjectures statement.
Timeline: Moser poses the problem (1966); Hammersley gives the lower bound and the upper bound (1968); Gerver exhibits the shape and its differential equations (1992); Romik gives the exact equations and numerics (2018); Baek proves optimality (2024, arXiv:2411.19826); Cureton et al. complete a Lean 4 proof of optimality, existence and uniqueness of the constants, and movability of Gerver's shape (2026).
Work in the plane . The hallway is , the union of its horizontal and vertical sides. A moving sofa is a nonempty closed connected set in the horizontal side together with a continuous path of plane isometries indexed by the unit interval, starting at the identity, keeping the image of inside the hallway at all times, and ending with the image inside the vertical side. Motions take values in the full isometry group ; continuity together with forces the path to lie in the orientation-preserving component. The sofa constant is the supremum, in the extended nonnegative reals, of the areas over all moving sofas. The supremum is finite, at least , and attained.
Gerver's shape is defined from a rotation path. For constants , , , , let be the piecewise function with breakpoints , , , from Romik's Theorem 2, let and be its cosine and sine integrals, and let be the associated translation path. The sofa for those constants is the intersection over angles in of the correspondingly rotated and translated hallways, with the endpoints using the horizontal and vertical sides. The four equations ABphiThetaSpec cut out the constants. They have exactly one solution with and , . The same Lean development uses the identical notation as the formal statements, so prose and code read as one document.
For every , , , satisfying ABphiThetaSpec,
The goal leaves unfixed which solution of the spec is used; by uniqueness all choices give the same shape up to the proved identification, so this is the stable form of Baek's Theorem 1.1. It asserts that the supremum equals the area of Gerver's shape, hence that no moving sofa has larger area and that the supremum is attained.
The first is Gerver's Theorem 2 in Romik's equation form on the closed domain. The second says every such shape admits a hallway motion. Together they supply the constants and the witness that the supremum is attained. The live mission records a root sketch composing the upper-bound half (every moving sofa is bounded by Gerver's area) with the movability witness into the supremum equality.
The result itself closes a problem open since 1966. It identifies the maximum area, shows the maximum is attained by an explicit shape, and determines that shape from four equations whose solution is unique. Consequences include the numerical enclosure proved by interval arithmetic, the finiteness of the supremum, and the reduction of future improvements to the analysis of the functional on caps. Without it the exact maximum remains unknown.
Formalizing it adds a machine-checked proof that makes no classical area assumption: the Green-type curve-area identity and the Minkowski-type mixed-area facts quoted by the paper are proved, the paper's 11 proof gaps and 33 misprints are repaired, and the numerical certificate is kernel-checked. The hallway, motion, cap, convex-body, and surface-measure infrastructure is reusable for related isoperimetric and kinematic formalizations. Status honesty: the underlying paper proof is complete and has been formalized in the source repository; on this platform the three statements above are open targets awaiting proofs, and the uniqueness of the maximizer up to rigid motion remains open and is not part of this mission.
The obvious argument bounds the area of an arbitrary sofa by the area of a circumscribed cap, but caps need not satisfy the injectivity condition that makes the functional an upper bound, and need not be concave on the full space of caps. Maximizing sequences of polygons need not converge to a sofa, and limits need not be connected or attain the supremum. The naive idea of taking a supremum over all connected closed sets and extracting a convergent subsequence fails until compactness of motions, closedness of the moving-sofa predicate, and a balanced maximum with rotation angle are established. Each step fails for general sets and only holds after the polygon approximation and monotonization constructions.
Lean represents the plane as EuclideanSpace ℝ (Fin 2) with its standard orientation, hallway sides as explicit sets, motions as I → E(2) where E(2) is ℝ² ≃ᵃⁱ[ℝ] ℝ² with the topology induced from continuous maps, and area as MeasureSpace.volume. The supremum is in ℝ≥0∞. Statements target the c5ea003 (Lean v4.30.0) environment, an older supported revision against which the development was verified locally. The spec uses non-strict inequalities, which makes uniqueness stronger than the strict-inequality literature form. The functions , , , take the constants as explicit arguments rather than reading global chosen constants, so the definition bundle stays independent of the existence proof; given uniqueness this implies the source statements. Boundedness and measurability are not assumed; every moving sofa is proved compact in the source development. A submission that drops closedness or connectedness, that allows a discontinuous motion, or that hard-codes the numerical value instead of proving equality with the volume of the defined shape, does not satisfy the statements. Contributions welcome: direct proofs of the three targets, sharper enclosures of the volume, and reusable hallway and motion lemmas. Out of scope: uniqueness up to congruence, the certificate details beyond the stated lower bound, and the 20 unformalized numbered environments listed in the source NOTES.md that none of the three targets depends on.
FormalConjectures/Wikipedia/MovingSofa.lean at ddfbaf90. https://github.com/google-deepmind/formal-conjecturesA QMA verifier receives a quantum witness and checks it with a circuit generated efficiently from the input. An acceptance probability separated by an inverse-polynomial gap is enough to define the class, but applications often need the probability of a wrong answer to be exponentially small. Repeating the verifier on many supplied witness registers achieves this error reduction while allowing the witness to grow. Marriott and Watrous proved the stronger statement that the same error reduction can be obtained without increasing the number of witness qubits Quantum Arthur–Merlin Games, Section 3.
The existing Lean development verifies the copy-based theorem, including soundness for witnesses entangled across the copies, and constructs a uniform circuit family with polynomial resources. This mission asks for the separate witness-preserving theorem. The paper already proves that mathematical statement; the open work here is its formalization in the stated QMA circuit model.
At each input length , a verifier has witness qubits, a finite work register, a designated output wire, and a quantum circuit. A uniformly generated family has a polynomial-time classical procedure that emits the complete circuit description, including the witness and work-register sizes. On yes-instances, some normalized witness makes the verifier accept with probability at least . On no-instances, every normalized witness is accepted with probability at most . The thresholds satisfy and for a polynomial .
The existing formalization represents witnesses as complex amplitude functions on bit strings, requires normalization explicitly, and uses layered circuits over its specified finite gate set. It also represents efficiently available real thresholds by polynomial-time procedures that output dyadic approximations. These are part of the formal statement's interface and must be made visible to users of the mission.
For every polynomial error exponent and every source verifier satisfying the conditions above, construct a uniformly generated, well-formed, polynomial-resource verifier for the same language, with completeness at least and soundness at most , while keeping the witness count exactly at every input length:
This is the witness-preserving strong error-reduction result of Marriott and Watrous (Theorem 4). The existing copy-based result corresponds to the weaker QMA class inclusion in Theorem 3 and will be linked as a proved background result. The mission goal must state the witness-count equation explicitly so that a copy-based amplifier cannot satisfy it.
Witness-preserving amplification lets a QMA protocol demand much stronger reliability without asking the prover for a longer message. That matters whenever witness size is itself a resource being compared or bounded. The copy-based theorem shows that the QMA class is robust under error reduction, but does not establish this fixed-message guarantee.
Formalizing the stronger result would add a reusable account of a verifier that reuses one witness, proves soundness for every normalized input state, and compiles its behavior into an ordinary uniform circuit family. Those components can support later formalizations that reason about repeated quantum verification under a fixed witness budget.
The completed copy-based proof uses three independent verifier blocks in each amplification round and bounds arbitrary entangled witnesses across those blocks. Its circuit resource analysis therefore allows the witness count to grow. A witness-preserving argument cannot use that construction. It must analyze repeated verification on one register and establish exponentially small error without assuming the input witness has a special spectral form. The formal circuit model currently exposes final-output measurements; any additional measurement behavior used in the analysis must be justified in that model and shown implementable by a finite, uniformly generated circuit.
The central audit point is the exact witness-length equation. A theorem that merely returns another polynomial-size witness, or that changes the source verifier's witness definition, is a useful class-level result but does not prove this mission's target.
The goal is parameterized by input-length-dependent completeness and soundness thresholds with an inverse-polynomial gap, and by a polynomial target exponent. Every witness quantifier is over normalized states. The output verifier must satisfy the same well-formedness and polynomial-resource conditions as the completed copy-based development. The platform statement uses its existing ShiClassQMAU.UniformQMA circuit-family encoding, which includes the witness and ancilla counts separately. A final proof should be kernel checked with only Lean's standard logical axioms and should not assume an amplification transducer or an unproved measurement lemma.
The paper quantifies over the class poly of unary-time constructible functions. This proposal represents the gap denominator and target exponent as literal Polynomial ℕ values, matching the checked copy-based development. It therefore formalizes a polynomial-parameter instance of Theorem 4 rather than the paper's full function-class generality. The threshold functions are supplied by polynomial-time dyadic approximators in place of the paper's informal efficient-computation convention. These interface choices are explicit in the Lean goal and should not be read as a proof of the broader formulation.
The local copy-based proof is complete and audited, but it has not yet been transplanted to Prove2Me. Its publication is preparatory work for this mission, not evidence that the witness-preserving goal is already solved. The proposal should reference the published copy-based endpoint and include only a few substantial milestones, so each item is meaningful to audit.
For let denote the -th prime. Brocard's conjecture, named after Henri Brocard, asserts that for every there are at least four primes strictly between and (Wikipedia). It belongs to the family of "primes between consecutive squares" problems together with Legendre's conjecture, and it is a concrete, elementary-looking question about short-interval prime distribution that remains open.
Primes are listed in increasing order. In the Lean development the list is 0-indexed: Nat.nth Nat.Prime k is the -th prime counting from , so nth 0 = 2, nth 1 = 3, nth 2 = 5, and so on. For an index write n.nth Nat.Prime and (n+1).nth Nat.Prime, two consecutive primes. The quantity of interest is
Milestone (Ferreira): for all sufficiently large indices ,
Goal (Brocard's conjecture): the same inequality for every 0-indexed , i.e. for every pair of consecutive primes starting from .
A proof of the goal settles Brocard's conjecture outright. Given Ferreira's asymptotic result, the remaining work splits into making the threshold effective and closing the finite range below it, both of which would be new formal content; the milestone itself (formalizing Ferreira's analytic argument) is a substantial analytic-number-theory formalization project.
Unconditional results on primes in short intervals only reach exponents well above , while the interval has length about where can be small (e.g. twin primes), i.e. length on the order of the square root of its endpoint. Standard short-interval theorems therefore do not apply uniformly, and Legendre's conjecture — which would only give two primes here — is itself open.
Everything is stated with Mathlib's Nat.nth Nat.Prime, Finset.Ioo (open interval, endpoints excluded) and Finset.filter Nat.Prime, followed by Finset.card. The hypothesis 1 ≤ n in the goal is the 0-indexed form of the source's ""; it is necessary, since for index (primes ) the interval contains only the two primes . The milestone uses Filter.atTop ("for all sufficiently large "), with no explicit threshold. No custom definitions are required.
BrocardConjecture.lean.