Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order , but the variance is unknown, so the bound cannot be evaluated from data.
Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).
For a vector of reals, the sample mean and sample variance are
Let be a probability distribution on a set , and a class of hypotheses (loss functions) . For , its risk is and its variance is , with . For a sample , and are and of the vector .
The complexity of enters through the growth function. For let , and let be the least number of sup-norm -balls centred in that cover . Then
For , sample variance penalization selects
With it is empirical risk minimization.
Fix , , and any . With probability at least in ,
The constants are the paper's. The goal is stated for an arbitrary comparator , so it covers an optimal one when one exists.
In the order of the proof:
Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as ; for a finite class does not depend on and the rate is . The paper gives a two-hypothesis example where empirical risk minimization cannot beat order (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.
All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a -normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.
Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for itself with the right dependence on , and is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.
The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.
Conventions:
i : Fin n.Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in " have laws giving zero mass outside .VarianceRegularization.Expansion.empMean. is a local sampleVar with the normalization. is Mathlib's variance.Metric.coveringNumber (closed balls, centres in the set, values in ).Added hypotheses and repaired statements, each disclosed in the item:
Ruled-out trivializations:
A complete development needs the following:
The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.
Controlled queues are the standard testing ground for Markov decision processes with infinitely many states: the state is a queue length, which is unbounded, and the holding cost grows with it. The classical theory of the average cost criterion (Ross, Applied Probability Models with Optimization Applications, 1970) produces an optimal stationary policy only when the relative discounted values are uniformly bounded, a condition that fails for almost every queue with unbounded holding costs. Linn I. Sennott's paper Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs (Operations Research 37(4):626–633, 1989, doi:10.1287/opre.37.4.626) replaced that boundedness by one-sided conditions that are checked in practice by a monotonicity argument and a single test function. Her conditions became the standard tool for queueing control and are the basis of Chapter 7 of her book Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999).
Timeline:
A Markov decision chain has states ; in state a finite nonempty set of actions; a cost ; and transition probabilities . A policy may depend on the whole history and may randomize; a stationary policy chooses in state . For , is the expected total -discounted cost from and , possibly infinite. The average cost of is
A stationary policy is average cost optimal if there is a finite constant with for every policy and every state .
The queue with variable service rates (Example 2). Time is slotted; is the probability of arrivals in a slot, independently across slots. The state is the number of customers at the beginning of a slot. When the queue is nonempty the server chooses one of finitely many decision variables and serves at rate , so that the customer in service leaves during the slot with probability ; there is no decision in state . From state the next state is with probability (), and from it is with probability . The cost structure: ; a polynomial of degree , nonnegative and increasing on ; and for . The arrival moments are and .
If , then
and
with the optimal average cost, , and bounded below.
Proposition 8 states that a queue in which at least one service rate exceeds the mean arrival rate has an average cost optimal stationary policy for holding costs of any polynomial growth, as long as the matching moment of the arrival distribution is finite. Bounded-cost results do not cover this case, which is the one used in practice. The general Theorem behind it is the standard vanishing discount theorem for countable-state models with unbounded costs; the Markov chain test of Propositions 4–5 and the Corollary reduces its hypotheses to a drift inequality for one policy.
All results of the paper are proved on paper. None is formalized: the platform has Sennott's discounted theory (Propositions 1–3, proved) and, as open statements, the book version of the Theorem (SennottDP.SEN.thm_7_2_3_sen_acoi), its existence part in a compact-action model (ArapostathisAC.SennottACOI.theorem_5_9), and the first half of Lemma A1 (SennottDP.SEN.lemma_7_2_1_acoi_bound). This mission states the paper's own version, with all conclusions of the Theorem, and its application to a concrete queue, which no platform item states.
The obvious route takes a limit of along a sequence and passes to the limit in the discount optimality equation. With unbounded costs and unbounded the sum is an infinite series of terms that need not converge uniformly, so the limit of the sums is not the sum of the limits. Only an inequality survives (Fatou's lemma, which needs the lower bound of Assumption 2), and the equation needs the integrable upper bound of Assumption 3*. For the queue, the hypotheses are not visible from the model: they come from a monotonicity property of and a Lyapunov drift computation whose leading term, , has to dominate a cost polynomial of the same degree.
The model is the published Markov decision chain of Sennott (1999), SennottDP.Discounted.MDC ℕ Act, with its policies, discounted costs and value functions, and the published average cost SennottDP.SEN.avgCost; Markov chains, steady state probabilities and first passage costs are the published SennottDP.MarkovCost objects. Conventions:
The second half of the goal is not "there exist and satisfying (6)": a pair solving (6) alone carries no optimality content, so the goal ties to the optimal average cost and and requires bounded below. The Theorem's milestones are stated for every limit point given by the Lemma, not for some stationary policy. The hypotheses of the goal are satisfiable (two-point arrivals , , one rate , , ), so the goal is not vacuous.
A complete development needs a discrete Tauberian inequality (already proved on the platform), Fatou's lemma for series, a compactness argument on , first passage identities and a Foster–Lyapunov criterion for positive recurrence. The Markov chain criteria (Proposition 4, the Corollary) and the Theorem are reusable for every countable-state queueing control model. Proofs of any milestone, and alternative arguments, are welcome.
Periodic-review inventory systems with lost sales and a positive replenishment lead time are a basic model of retail and spare-parts operations: demand that cannot be met from stock is lost, and an order placed today arrives periods later. Even with a known demand distribution the optimal policy depends on the whole vector of outstanding orders and is intractable for long lead times, so practice and theory fall back on base-stock (order-up-to) policies, which are asymptotically optimal as the lost-sales penalty grows relative to the holding cost (Huh, Janakiraman, Muckstadt and Rusmevichientong, Management Science 2009).
Computing the best base-stock level still requires the demand distribution. In many settings the distribution is unknown and, worse, demand is censored: the manager records sales, , and never sees the demand lost to a stockout. The paper behind this mission, Huh, Janakiraman, Muckstadt and Rusmevichientong, An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand (working paper of February 8, 2007; published in Mathematics of Operations Research 2009, DOI 10.1287/moor.1080.0367), gives an algorithm that learns the optimal base-stock level from sales data alone and bounds its regret against the best base-stock policy. It extended the zero-lead-time adaptive newsvendor analyses (e.g. Huh and Rusmevichientong, Math. Oper. Res. 2009) to positive lead times, where the inventory process is a Markov chain on .
Demands are i.i.d. copies of a nonnegative, continuous random variable with and distribution function . The inventory vector in period is
the outstanding orders and the on-hand inventory ; its inventory position is . Under the order-up-to- policy the manager orders , demand is realized, and
A period with on-hand inventory costs, in expectation, , with holding cost and lost-sales penalty . The long-run average cost of level is
and denotes a level minimizing it over . Write .
The algorithm runs in cycles of length ; . Cycle uses a fixed level . From sales data it computes a sample-path derivative by a recursion over the last periods, forms a gradient estimate from the last period of the cycle, and sets with . The inventory is carried over between cycles. The regret after cycles is
Under Assumption 1 ( and ) and infinite support of , for and , with and ,
with . At this is .
Lemma 5 (tail of ), Lemma 6 (the inventory position falls to ), Theorem 7 (existence, independence of the start, convexity and differentiability of , and existence of with ), Theorem 11 (projected stochastic gradient descent with biased gradients), Lemmas 12 and 13 (sums over cycles of length ), Lemma 14 (the regret from ) and Lemma 15 (the transient regret ).
The theorem gives a nonparametric, sales-only policy whose average cost approaches that of the best base-stock policy at an explicit polynomial rate, uniformly over demand distributions satisfying Assumption 1. Its ingredients are reusable: an explicit geometric ergodicity rate for the lost-sales base-stock chain, convexity of the long-run base-stock cost in , and a regret bound for projected gradient descent whose gradients are biased by Markov dependence.
The result is published; to our knowledge none of it has been machine-checked. The mission formalizes the regret bound, which requires Markov-chain ergodicity on a continuous state space, long-run averages, and stochastic approximation with biased gradients. It also repairs the printed constants: Theorem 10 and Lemma 15 are false as printed (see Formalization scope), and the formal statements make the dependence on explicit.
The obvious route treats the cycle's last-period derivative as an unbiased gradient of and applies standard online convex optimization. That fails: the estimate is computed from a Markov chain started at whatever state the previous cycle left, so it is biased, and the bias decays only as the chain mixes. Controlling the bias requires an explicit mixing rate for a chain on whose state includes the derivative process, uniformly over the levels in and over starting positions above . The ergodicity argument uses a coalescing demand pattern, which exists only when ; without that condition the chain need not be ergodic. A second obstacle is that the objective is defined as a long-run average, so its convexity and differentiability in must be established before any gradient argument applies.
Everything is stated in Lean 4 with Mathlib. The inventory vector is a pair (pipeline Fin (τ-1) → ℝ, newest order first; on-hand ℝ). Lean periods are -based (Lean period is the paper's ); cycles are numbered from . Demand is a sequence on a probability space that is i.i.d., nonnegative, integrable, with and an atomless law; infinite support is for all ; , . The long-run cost is a limsup of Cesàro averages from the empty start (Theorem 7 shows it is a limit from every start), and is any minimizer over . The algorithm is a deterministic function of the demand path; the sample derivative is the recursion the algorithm computes, not a derivative. Integrability of every expectation follows from boundedness of the inventory and is not assumed.
Corrections, all disclosed in the items: Theorem 10 carries instead of on the term, because the printed bound fails for , , , where the right side is and . Lemma 15 carries and . Lemma 14 keeps its printed constant; its proof appears to use the ergodicity theorem one period early. Theorem 11 is stated on an interval with the bias taken conditionally on the history. Lemmas 5 and 6 are stated for infinite support only.
A goal that bounds the regret by alone (costs at the steady state of ), or that lets the levels be any sequence in , is not the theorem: the regret here uses the realized inventory of the algorithm. Lean's conventions and of a nonpositive number cannot trivialize the bound, because infinite support and give . The source is the authors' working paper of February 8, 2007, whose printed page numbers equal the PDF's.
Not yet stated: Theorem 3 and Lemma 4 (ergodicity rate), Theorem 8 and Lemma 9 (bias bounds), Theorem 1 (sample derivatives). They need the joint chain and are welcome as contributions, as are the general pieces: geometric ergodicity via coalescence, and the biased projected-gradient bound.
A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.
The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.
Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).
At round , the outcome is for wet and for dry. The forecaster selects a probability from the finite grid , where is a positive integer. A forecast is represented by the binary probability vector ; the second coordinate is the forecast chance of rain. The forecaster chooses with probability . The Brier loss of that possible forecast is .
After rounds, counts the realized forecasts equal to , and is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is
A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score , in which the realized indicator that was chosen is replaced by its conditional probability . Its weighted count is , and its weighted wet frequency is when the denominator is positive.
For grid points and , the pairwise regret is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing by on rounds weighted by . The algorithm chooses its next distribution so that the regret flow out of each equals the flow into :
These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.
The target is Theorem 1: for every , choose and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies
The time after which the inequality holds may depend on the forecaster, Nature, and . The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.
The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on . Theorem 3's last constant is written as and the corollary's horizon as ; the printed constants are inconsistent with the paper's grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.
The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.
The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.
The weighted score is controlled by quantities known from the chosen mixtures, while depends on the actual random draws. A direct deterministic bound on therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.
The Lean model uses binary outcomes, grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index : the paper's in round is the regret over the preceding indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.
The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map is injective for . The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing by would change the claim.
Every theorem requiring the grid has the explicit condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency ; nonnegative weights make its numerator zero as well. At horizon , the weighted calibration score is . The probability event is measured with the history law's outer measure in . Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.
Retailers of seasonal goods, home builders selling out a development, and airlines and cruise lines selling promotional fares all face the same operational question: inventory is fixed, the selling season is finite, and the price can be changed only rarely. Menu costs, advertising commitments and customer goodwill often restrict a seller to a single price change. The question is then when to change the price, and, if both a lower and a higher price are available, in which direction.
Feng and Gallego (Management Science 41(8), 1995) answered this for Poisson demand. Their §4 treats a single markdown (Theorem 1) and a single markup (Theorem 2). This mission formalizes their §5, the markup-or-markdown problem: the seller starts at a middle price and has one opportunity to move either down or up. The paper shows that the optimal policy is again described by time thresholds that depend only on the remaining stock, now two per stock level. The paper builds on the deterministic and fluid analysis of Gallego and van Ryzin (1994), where arbitrarily many price changes are allowed, and is the starting point of a literature on limited-price-change revenue management surveyed by Bitran and Caldentey (2003).
There are three prices . At price demand is a Poisson process of intensity , and at of intensity , with
all prices and intensities positive. Lowering the price raises both the sales rate and the revenue rate. Salvage value is zero. Note that in this section is the lower price; the initial price is .
A seller with units and time-to-go sells at and may switch once, to or to . Write for the demand process at and for that at .
where is the set of stopping times of the history of with and almost surely.
Under the paper's assumption for every , there are strictly increasing sequences , with
such that , where for and otherwise. The excess equals on and on . Each solves
with and . The thresholds are and .
Theorem 3 says that the two-directional problem has the same simple structure as the one-directional ones. With units left and time-to-go , the seller marks down at once when falls below , marks up at once when exceeds , and otherwise keeps the price. Because the thresholds increase with the stock, the policy reduces to a table of numbers, which the paper computes for a housing example (Table 5). The theorem also quantifies the value of flexibility: in that example, allowing either direction adds about $1,500 over the markdown-only policy and about $7,000 over the markup-only policy.
Lemma 3 and the verification Lemma 1 are reusable beyond this mission. Lemma 3 is a sign-change property of differences of Poisson tail sums, of the kind that drives threshold results in revenue management. Lemma 1 is a sufficient condition for the value of an optimal stopping problem driven by a Poisson process. The paper's results are proved with pen and paper only; none of them has a machine-checked proof. The formalization adds a precise statement of Lemma 1, whose printed hypotheses are insufficient (see the scope section), and an explicit record of which threshold facts Theorem 3 depends on.
The value is the supremum over stopping times of a continuous-time process, and the obvious approach, dynamic programming over the stock, needs the value one stock level down. The thresholds at stock are defined through , so the structure must be propagated from one stock level to the next, and several properties have to propagate together. One must know that again has a single sign change, which requires to be increasing beyond . One must also know that is positive up to and eventually negative, so that is finite, and that . These facts concern three different price pairs at once: , and . A direct comparison of with the two one-directional value functions fails, because the optimal direction itself depends on the stock and the time-to-go. The verification step needs a pathwise fundamental theorem of calculus for the Poisson-driven process, which is where the regularity hypothesis on matters.
QueueingFundamentals_Foundations_ArrivalProcess. The rate enters through the hypothesis IsExpInterarrivals P lam T, and enters only through its law: the sum is written through its Poisson law. is the class of real-valued stopping times of the σ-algebras generated by the counts , , with and almost surely.HasDerivAt. Threshold sequences are indexed from . Every infimum is a real sInf paired with the nonemptiness of its set. , , , and the thresholds are existentially quantified and tied together by the theorem's equations, so the existential determines the paper's objects. The page's assumption is a hypothesis of the goal, as on the page.An airline may offer a low promotional fare while seats remain available, then raise the fare as departure approaches. The choice is dynamic: a sale changes both the number of seats left and the benefit of waiting. The same decision appears for hotel rooms and theater seats. Feng and Gallego study a policy with two fixed prices and at most one price change, while allowing the switching time to depend on actual sales rather than a calendar date chosen in advance. Their 1995 paper proves that this adaptive problem has an inventory-dependent threshold rule. This mission isolates the markup case, in which the second price is higher than the first.
The two-price restriction has a practical role. A seller may know the fare classes it can offer while still needing to decide when to close the promotional class. The result identifies a sequence of time thresholds that can be computed for the chosen price pair. It is therefore a structural claim about an optimal policy, not a choice of numerical prices or a claim that two prices optimize over every possible price menu.
There are items and units of time-to-go. At price , sales requests follow a Poisson counting process with rate . Each request sells one item while stock remains. The paper assumes that demand falls as price rises and that the lower price has the higher revenue rate. Thus the markup case has
The salvage value at the end of the horizon is zero. A fixed switch at time charges first and afterwards. Its expected revenue, denoted , is
The two counts in the last term are independent, so their sum has Poisson mean . This is the expression in §3 of the paper. In particular, is the revenue from increasing the price immediately.
An admissible switching time uses only the history of sales at ; it lies between zero and and cannot wait past stock exhaustion. The optimal value is the supremum of expected revenue over these stopping times. The stopping decision may react to sales before the change, but it cannot anticipate future requests. This distinction matters because a deterministic switch time generally has less information than an adaptive one.
The goal is Theorem 2 on pp. 1382–1383. Define the switching function
There are thresholds with , and is increasing. A continuation premium gives the value
For , below and is zero at or above it; . The function satisfies and the differential equation , where . The remaining thresholds are the first nonnegative zero of and the first positive zero of :
The milestones reproduce equation (17), the markup half of Lemma 2, and Lemma 1. Together they identify the Poisson derivative identity, the sign change of , and the verification criterion used to relate a candidate value to optimal stopping. The paper proves the mathematical result; the mission asks for machine-checked proofs of these formal statements.
The threshold sequence tells a seller when increasing the price immediately is optimal, conditional on the stock still available. The value formula also gives the benefit of continuing at the promotional price when time-to-go lies below the threshold. The statement preserves the paper's weaker word “increasing” for : it asserts monotonicity and does not require strict monotonicity of either sequence. The full theorem includes the recursive equations for and , so a proof of a threshold-shaped region alone would leave part of the source result unformalized.
Formalization would add a reusable optimal-stopping model built from a Poisson arrival process, a fixed-switch revenue function, and a verification lemma. The arrival process already has a published definition; the switching model and the theorem statements here are new drafts. The theorem is established in the 1995 article, while its Lean proof remains to be supplied.
The immediate-switch comparison has a single sign change, but the optimal decision also depends on revenue already earned and on the value of unsold stock after each possible sale. For , the relevant forcing term is , so the sign of alone does not locate the optimal switching threshold. A direct fixed-time comparison likewise does not establish optimality among stopping times that react to observed sales. These are the main obstacles the formal proof must address.
The Lean model uses natural-number stock, nonnegative real time, positive real prices and rates, and an imported counting process built from independent exponential interarrival times. A rate is attached to each price. The history of the first process defines the stopping-time class; the second process enters through its Poisson law after a switch. The supremum ranges over admissible stopping times, and the payoff is bounded and measurable under the stated process law. The definition writes sales before switching as , equal almost surely to for admissible times. The probability-measure assumption is explicit, though the exponential interarrival law entails it.
Lean assigns a default value to an empty real infimum. The theorem explicitly asserts that each defining zero set for , , and is nonempty; it also keeps in the definition of , since . Continuity of at zero connects its boundary value to its differential equation. Lemma 1 includes its missing initial, zero-stock, obstacle, and local-Lipschitz assumptions, all required by its printed proof. The paper's word “bounded” in Lemma 2 is retained in the milestone quotation but replaced by the positive lower bound it uses; is unbounded as stock grows. These choices are recorded for review in the moderation notes.
The goal derives optimality from the demand and price assumptions. It does not assume the verification conditions, the sign change, or the revenue identity as premises. Contributions to the Poisson tail calculus, stopping-time measurability and boundedness, threshold zero sets, and verification argument are within scope and can be reused in related finite-inventory pricing models.
Given a reference probability distribution and a set of probability distributions, the minimum discrimination information problem asks for the member of closest to in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations , and the classical answer is that the minimizer is an exponential family member, with density with respect to .
That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the .
Timeline:
All distributions (PD's) live on one measurable space . The I-divergence of from is
where is the density of with respect to ; it takes values in and vanishes only for . The variation distance is for any PD dominating both. If is a convex set of PD's containing some with , a with
is the I-projection of on .
Fix real-valued measurable functions on . For (Euclidean -space) the moment set is the set of PD's with , . Further:
If is open in , then for every point of the interior of the I-projection of on exists and
for some constant and some .
Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.
The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).
The obvious argument fails at the first step: the moment set is convex but not closed in variation when the are unbounded, since is not continuous in variation. A minimizing sequence therefore converges in variation to some (as in Theorem 2.1), but nothing places in : mass can escape to where is large. Ruling this out needs quantitative control of , which in turn requires knowing the form of before knowing is feasible; the interplay with the convexity of and the openness of is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.
Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions , , .Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. is allowed.sInf over a possibly empty set.A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) ), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.
Grover's algorithm (Grover 1996) finds a marked item among with queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).
Timeline:
A -query algorithm acts on vectors , where is the set of query strings, the set of answers (an additive group) and a finite workspace. A basis configuration with is querying ; is not querying. For an oracle the oracle operator is
The algorithm consists of a unit vector , unitaries that do not depend on the oracle, and a set of accepting configurations. With oracle its states are ; the acceptance probability is the squared norm of the accepting part of . The query magnitude of in is (Definition 3.2). The algorithm decides a property if it accepts with probability at least when the property holds and at most when it fails.
In the main theorem with bitwise addition, and the oracle is a uniformly random function . The question is whether belongs to .
The constant is existential, matching the theorem's hypothesis ; and do not depend on the workspace or the algorithm.
The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle ; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).
The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.
The obvious argument — each query reveals one bit about where the preimage is, so queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.
The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running steps is a -query algorithm: oracle answers on lengths other than are fixed and absorbed into the unitaries, as the proof fixes them, and the input is absorbed into . Queries return the full value ; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all functions; total variation distance is the paper's without the factor .
Corrections: Theorem 3.3 is printed with conclusion , which fails (one query string, , distance at ; machine-checked); the true bound is . Corollary 3.4 is printed with , which fails (16 strings, , ); the true bound is . The printed constant in the proof of Theorem 3.5 does not support the step even with the paper's own count; the goal states an existential constant, and works with the corrected Corollary 3.4. The closing probability- argument over countably many machines and the class statement about are not formalized.
A formalization in which algorithms query at every step on every branch (no sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.
Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.
The Euclidean traveling salesman problem asks for the shortest closed route through a finite set of points in the plane. Even when the points are placed independently and uniformly in a square, finding an individual shortest route is computationally difficult. A separate probabilistic question is whether the optimal length varies much from one random sample to another. In Chapter 11 of Talagrand's 1995 paper, this question motivates a concentration theorem for the tour length and for other geometric functionals with the same local regularity property.
The result is useful because a bound on fluctuations can be applied without computing the distribution of the optimal tour length. It separates the typical size of the length, which may need other geometric estimates, from the chance of a substantial deviation. The paper develops a more general concentration method for product spaces; the geometric chapter shows how its estimates can control an optimization problem whose response to changing one sample point depends strongly on the local configuration.
Let , and let be independent points uniformly distributed in , with . A configuration is the finite set ; repeated sample locations are represented once in . For any finite , write for the length of a shortest closed tour visiting every point of . The tour length of the random sample is . The empty set and a singleton have tour length zero.
The main theorem concerns a functional on all finite subsets of . A level dyadic square has side . Say that has regularity constant when, for every finite and every finite , if a point of lies within Euclidean distance of , then
The first inequality is monotonicity under adding points. The second limits the added cost when the new points lie in a small square near an existing point. Lemma 11.2.1 says that the shortest tour functional has this property with a universal constant. In particular, the functional in the main theorem is not an arbitrary real function on samples: it must obey this condition for every admissible square and pair of finite sets.
A median of is any real number for which both and are at least one half. The theorem applies to every median. This convention avoids selecting one median when the distribution has more than one.
For the intermediate geometric estimates, is the largest integer with . Given a deviation parameter , is the integer selected by the criterion (11.1.9) after the paper sets the auxiliary Poisson intensity to . The number counts level squares that contain at most distinct sample points. An isolation weight records the largest scale between and at which the square containing contains at most sample points, and equals if no such scale exists.
For each fixed , there is a constant , independent of and , such that every measurable with the regularity property above satisfies, for all ,
This is Theorem 11.2.2, the goal. Its constant may depend on the fixed regularity constant . Lemma 11.2.1 makes the tour length a direct instance. The milestone list also includes the quantitative sparse-square estimate of Proposition 11.1.4, the isolation-weight bound of Proposition 11.2.3, and the deterministic insertion estimate of Proposition 11.2.5. These retain the paper's specified thresholds and the dependency of their constants.
For , the result supplies a tail bound whose scale does not grow with the number of sample points. It says that the shortest tour length lies near a median with a Gaussian-form upper bound on the probability of a deviation. It does not identify the median or give an algorithm for finding the optimal tour. The abstract form also covers other finite-set functionals once their local regularity condition is established.
The paper proves these claims in ordinary mathematics. This mission asks for machine-checked proofs of the stated concentration, geometric occupancy, and tour-insertion results. The reusable outputs include a finite-set model of Euclidean tours and a precise interface for local regularity; the dyadic occupancy and isolation-weight definitions can support later sections on other geometric structures. No machine-checked proof of these specific chapter results is claimed here.
A naive bounded-differences estimate treats the effect of changing a sample point as if a single fixed worst-case insertion cost applied everywhere. That loses the paper's uniform fluctuation scale: a point can be unusually isolated, and its insertion cost can be much larger than the cost near a typical dense cluster. The central problem is to keep track of those irregular locations while retaining a bound uniform in . The chapter's dyadic-square counts and isolation weights make this difficulty explicit in the statements.
Points are pairs of real coordinates constrained to , represented as functions on Fin 2. Their distance is the Euclidean distance, defined explicitly; the default norm on a Lean function space would give a different metric. The random sample is a product of coordinatewise uniform probability measures. is the set of distinct sampled locations, so ties have a defined value. Tour length is the minimum cyclic tour cost over the finite set, using the published generic metric-TSP tour model as its base.
Dyadic squares are closed in the local regularity condition. For the single square assigned to a point in the definition of , the implementation uses half-open cells, with the right endpoint assigned to the final cell. This resolves only grid-line ties, which have probability zero under the stated sample law. Counts use distinct locations, as does the paper's set . All probability inequalities are compared in the extended nonnegative reals. The event bound is written with ENNReal.ofReal; a negative formal lower bound represents the paper's trivial probability lower bound. The main theorem explicitly assumes measurability of the sample functional, following the paper's convention that all relevant functions are measurable. Theorems in Section 11.1 retain and ; the main theorem covers every .
The formalization must not replace the square's uniform law by an arbitrary distribution, use a supremum-norm tour, or place the existential constant after or . Contributions toward the goal may develop measure-theoretic facts about the product law, finite Euclidean tours, dyadic occupancy bounds, or the insertion estimate. Those interfaces have uses beyond this chapter.
In 1952 Herbert Robbins asked how a statistician should draw a sample sequentially from two populations when the goal is the largest possible expected total, not a test or an estimate after the fact (Robbins 1952). This is the problem now called the two-armed bandit, and Robbins' paper is the usual starting point of the multi-armed bandit literature that underlies clinical-trial allocation, adaptive experimentation and online recommendation (Lattimore and Szepesvári 2020).
Robbins illustrated the problem with two coins. His first concrete rule, "stay on heads, switch on tails" (later known as win-stay, lose-shift or play the winner), uses only the outcome of the last toss, yet its long-run loss relative to an observer who knows the better coin is at most per toss, against for a rule that ignores the outcomes. The same rule was studied again in clinical-trial design as "play the winner" (Zelen 1969).
Timeline. 1952: Robbins computes the operating characteristics of the stay-or-switch rule and of the outcome-blind rule for two coins, and shows that a greedy rule with sparse forced sampling attains for arbitrary populations with finite means (Section 2). 1969: Zelen proposes the play-the-winner rule for clinical trials. 1985: Lai and Robbins give the logarithmic lower bound on regret and rules that attain it (Lai and Robbins 1985).
Two coins and have unknown head probabilities and , with . A head pays \1x_i\in{0,1}iS_n=x_1+\dots+x_nn0A(1-\alpha)\delta_0+\alpha\delta_11B(1-\beta)\delta_0+\beta\delta_1$.
A sampling rule chooses the coin for each toss from the outcomes of the earlier tosses. Two rules are studied.
Write for the probability of heads on the -th toss under the rule in use, and for the expected average payoff of the first tosses. The paper's two parameters are
so that is the expected payoff per toss of an observer who knows the better coin. Following the paper, and are assumed not both and not both ; then .
Under ,
and for every admissible pair of coins
with equality at and at (Eqs. (6), (8) and the text after (8), p. 531).
The result. The goal quantifies how much an extremely simple adaptive rule recovers. A rule blind to outcomes loses up to half a dollar per toss; one bit of memory cuts the worst case to about . Robbins used this comparison to argue that the sequential design problem has nontrivial, computable answers, and to motivate the forced-sampling rule of the same section, whose loss tends to . The closed forms (3)–(6) are the exact operating characteristics of the four-state Markov chain that generates.
Formalizing it. The results are classical and elementary on paper, but none of them has a machine-checked proof. The mission produces a verified chain from the canonical bandit measure to an explicit long-run payoff: the head probability of a fixed toss is computed from the law of the whole trajectory, the recursion is derived from the rule's kernels, and the Cesàro limit closes the argument. The same pattern applies to any finite-memory bandit rule, and the coin bandit and the two rules are reusable test cases for the platform's bandit library. No platform theorem states , its recursion or its loss; other two-state models on the platform (a Markov-renewal gain rate, an MDP gadget) are different objects.
The recursion (2) is a statement about the trajectory law, not about a Markov chain given in advance: the chain has to be extracted from the Ionescu–Tulcea construction of the bandit measure, where the coin of toss is a deterministic function of toss and the payoff is drawn from the chosen coin's law. The head probability alone is not a Markov chain: depends on the joint law of coin and outcome at toss , so a naive one-step argument on does not apply, and the affine form of (2) is a property of this particular rule. The maximization in (8) is over a two-dimensional region whose maximizers lie on the boundary or , and the excluded corners are exactly where the formula breaks down.
The bandit is the published BanditAlgorithm.StochasticBandit 2; the rules are policies of the published type BanditPolicy 2, and probabilities and expectations are taken under the published infinite-horizon measure banditTrajMeasure, whose coordinate is toss . Head probabilities are elements of unitInterval. The conventions committed to are:
The asymptotic loss is stated as the limit of ; defining by its closed form would make the goal a tautology. Likewise, the head probabilities are computed from the law of the rule on the coins: positing a sequence that satisfies (2) would drop the probabilistic content.
A complete development needs: the one-dimensional marginals of banditTrajMeasure (the law of coordinate given the prefix), the joint law of (coin, payoff) at each toss, linearity of expectation for bounded payoffs, a Cesàro-mean lemma, and a short two-variable optimization. The trajectory-marginal lemmas are reusable for every bandit mission on the platform; contributions that prove them in general are welcome.
In 1975 P. Brucker, J. K. Lenstra and A. H. G. Rinnooy Kan classified a large part of deterministic machine scheduling by computational complexity, using the then new theory of NP-completeness of Cook and Karp. Their report, Complexity of Machine Scheduling Problems (Mathematisch Centrum, Amsterdam, 1975; published in Annals of Discrete Mathematics 1, 1977), gives for many problems either a polynomial algorithm or a polynomial reduction from a known NP-complete problem. It drew the boundary between easy and hard scheduling problems that later surveys and the standard three-field classification build on.
This mission covers four reductions of the report's Theorem 4 that concern shops with several machines. A flow shop processes every job on machines in this order; a job shop lets each job follow its own route. For two machines and no further constraints, the flow shop is solved by Johnson's rule (Johnson, 1954) and the job shop with at most two operations per job by Jackson's extension of it (1956). The four reductions show that these positive results stop exactly where one more feature is added: one job with a nonzero release date, tree-shaped precedence constraints, a third operation per job, or a third machine.
A general shop instance has jobs and machines . Job consists of operations; its -th operation runs on machine for time units, and the tuple is the job's machine order (a machine may occur more than once). Each job has a release date , and some pairs of jobs carry a precedence constraint .
A schedule gives every operation a start time. It is feasible if no operation of starts before ; the operations of each job run in the order , each after the previous one completes; two operations on the same machine never overlap; and implies , where is the completion time of and the starting time of . The makespan is .
In the report's notation , means a flow shop and a job shop; may contain (only the last job has a release date), tree (the precedence graph is a branching: no directed cycle, and either every indegree or every outdegree is at most one) and (at most operations per job). The recognition version of a problem asks, for an instance and a number , whether a feasible schedule with exists.
KNAPSACK asks, for positive integers and , whether some has . A problem is reducible to () if every instance of can be transformed in polynomial time into an instance of with the same answer.
Each part is a polynomial-time many-one reduction between languages of binary strings. The other six parts of Theorem 4 (single-machine problems) belong to other missions of this series.
For positive with , and for each of the paper's four constructions with its threshold ,
with for (i), for (j), for (g) and for (h). The milestones are stated directly about the printed constructions, in the order (i), (j), (g), (h) of the report.
With the NP-completeness of KNAPSACK (Karp, 1972), the goal makes the four problems NP-complete. As the report notes, (i) and (j) together with the elementary reductions of its Theorem 1 make the general job shop NP-complete for every fixed . Parts (g) and (h) show that Johnson's two-machine algorithm admits neither release dates nor precedence constraints in general. Because KNAPSACK can be solved in pseudo-polynomial time, these results establish NP-hardness in the ordinary sense only; strong NP-hardness of some of these problems came later (Garey, Johnson and Sethi, 1976, for the three-machine flow shop).
The results are proved in the report; no machine-checked proof of any of them is known to exist. A formalization adds explicit constructions and complete equivalence proofs where the report is brief: in (h) it proves one inequality and states that the rest "is analogous to that of reduction (g)", and the forward directions are given by figures. It also produces a reusable formal model of general shops with integral start times, release dates, precedence and repeated machines.
Polynomial-time computability of the constructions is routine in principle but laborious in Cook's Turing-machine model, which is the setting of the goal: binary arithmetic for , and , and parsing of the KNAPSACK code.
The mathematical difficulty is the reverse direction of each equivalence. The report's arguments are phrased in terms of "a processing order on " and treat the jobs before and after an extra job as two blocks. A formal proof must derive such an order from arbitrary start times and must handle every interleaving, including idle time and the case where the extra job's operations do not fit the printed pattern. In (j) the printed bound for the case contains a minimum of two quantities whose justification is left to the reader. In (h) the printed case uses , so the positivity of the data matters, and the remaining cases are only said to be analogous to (g).
Jobs are Fin n and machines Fin m, both 0-based. A job's operations form a list of (machine, processing time) pairs, so machine orders may repeat machines, as in (i) does. Start times are natural numbers. The report computes schedules from processing orders on integer data, the makespan is a regular criterion, and release dates and precedence survive shifting operations left, so integral start times lose no value. is stated as for every ; no maximum over an empty set is formed. Precedence is between jobs: every operation of starts no earlier than . A branching is an acyclic precedence graph in which every indegree is at most one or every outdegree is at most one; the report's "either … or" is read for the whole graph. Job-shop classes require at least one operation per job. A flow-shop job has exactly the operations , with times allowed to be zero.
The following readings of the report are made explicit. "Reducible" is Karp reducibility, CookPvsNP.PolyReducible from the published definitions CookPvsNP_defs. The languages are over the four-letter alphabet with binary numbers of the published definition ProjSchedTW.Complexity.Encoding. Its subsetSumLang allows zero sizes, while the report's KNAPSACK is over positive integers, so KNAPSACK is defined locally with positivity in the language. "We may assume that " becomes a hypothesis of every equivalence; the goal's reduction must still handle the other inputs. The printed "value " of the forward directions is read as "", as Section 2 defines the recognition version. The remark that (h) is analogous to (g) becomes the full equivalence for (h). An instance outside the problem's class is not in its language. NP-membership is not part of the goal.
The formal two-stage flow-shop models of Johnson's paper (JohnsonFlowShop.TwoStage.IsFeasible) and the job-shop model of Jansen, Solis-Oba and Sviridenko (JobShopLTAS.Core.Instance) use real start times and have neither release dates nor precedence. They were consulted, but the model here is local.
Ruled out as trivializing: a goal without the polynomial-time condition (the bare equivalence of yes-instances), a target language that accepts instances outside the class, and equivalences about some instance rather than the printed construction.
Contributions are welcome on any milestone, on a general lemma that turns a feasible schedule into a processing order per machine, and on polynomial-time computability of list arithmetic in the Turing-machine model, which every reduction of this series needs.
Many problems in statistics and engineering ask for the level at which an unknown function takes a prescribed value : the dose at which a fraction of subjects respond, the setting at which a noisy device reaches a target output, the -quantile of a distribution that can only be probed by yes/no experiments. When the function can only be observed through noisy measurements, classical root-finding does not apply. Robbins and Monro (Ann. Math. Statist. 22 (1951) 400–407) proposed a recursive procedure that uses one noisy observation per step and proved that it converges in mean square. The paper started the field of stochastic approximation, which today underlies stochastic gradient descent, temporal-difference learning and adaptive control.
Timeline. Robbins and Monro (1951) prove mean-square convergence for bounded responses under conditions (5′) or (33)–(35). Kiefer and Wolfowitz (1952) adapt the scheme to finding a maximum. Blum (1954) proves almost-sure convergence under weaker moment conditions. Dvoretzky (1956) gives a general convergence theorem covering both schemes. Later work (Robbins and Siegmund, 1971; Ljung, 1977; Kushner and Clark, 1978; Benaïm, 1999) develops the supermartingale and ODE methods.
To each real level corresponds a random response with distribution function , and the regression function is
The responses are bounded: there is with for all (condition (4)). Fix constants and positive step sizes . The Robbins–Monro process starts at an arbitrary constant and sets
so is a fresh response observed at the current level . The quantity of interest is the mean squared error .
A sequence is of type if
is the standard example. The proof also uses , and .
If is of type , (4) holds, and is nondecreasing with and , then, whatever ,
Theorem 1 (p. 404: the same conclusion under (5′), for and for ); convergence in probability under the hypotheses of Theorem 2 (p. 401); the quantile estimator of §4, (48); and (30), that gives a sequence of type .
Theorem 2 is the first convergence theorem for a recursive root-finding procedure under noise. It shows that a procedure using no knowledge of or of the noise distribution, beyond a monotone crossing and a positive slope at the root, is consistent. Section 4 turns it into a distribution-free consistent estimator of a quantile from response/nonresponse data, the up-and-down designs of bioassay and sensitivity testing. Its step-size conditions, with a divergence condition, remain the standard conditions for stochastic gradient methods.
The theorem has been proved since 1951 and strengthened many times. As far as is known it has no machine-checked proof, and Mathlib has no stochastic approximation theory. Formalizing it requires conditional laws given by Markov kernels, integration against a composition of a measure with a kernel, and deterministic series arguments. A finished formalization would be a base for formalizing the almost-sure theorems (Blum, Robbins–Siegmund) and the ODE method.
The obvious argument fails at one step. Monotonicity of and a positive derivative at do not give a uniform positive lower bound on the slope : away from the slope can decay to , for example when is bounded, as (4) forces. So the drift towards is not uniformly strong, and the newcomer's first idea, a uniform contraction , is not available under (33)–(35). This is why the theorem needs the divergence condition (26), which is stronger than , and not only (6). On the formal side, the expectations come from integrating against the joint law of , and they need integrability bounds before any identity can be used.
Everything is in the namespace RobbinsMonroSA.Conv, over a probability space with IsProbabilityMeasure P. Indices are 0-based: Lean's x 0, a 0 are the paper's , , and Lean's bigA … n is the paper's . The committed conventions are:
Kernel ℝ ℝ with IsMarkovKernel H (each is a probability law, measurable in ).0 < C ∧ ∀ x, H x [-C, C] = 1. It is a hypothesis of every item that mentions an expectation, and it is what keeps the Bochner integrals defining , , and from defaulting to .HasDerivAt M M' θ with 0 < M'.The standing assumptions of §3, (4), (5) and (6), are hypotheses of Lemma 1, Lemma 2 and the displays of §3 whose proofs use them. In Theorems 1 and 2, (5) follows from (5′) or from (33)–(34), and (6) is part of "type ".
The goal cannot be trivialized. It mentions neither , , nor any constant, and the process must satisfy (8) for every . Without (8), would be arbitrary and the statement false; with it would be deterministic.
Contributions welcome: proofs of the milestones, reusable lemmas on integrating against μ ⊗ₘ κ, and a proof that satisfies (26).
Minimizing the total completion time of jobs on a single machine is one of the oldest problems in scheduling theory. When every job is available at time , processing the jobs in order of nondecreasing processing time is optimal (the shortest-processing-time rule), so the problem is solved by sorting. Release dates, times before which a job may not start, change the picture. In their 1975 report Complexity of Machine Scheduling Problems (Mathematisch Centrum Report BW 43/75; journal version in Annals of Discrete Mathematics 1, 1977), Brucker, Lenstra and Rinnooy Kan used the then-new theory of NP-completeness (Cook 1971, Karp 1972) to map which classical scheduling problems are polynomially solvable and which are NP-complete. Theorem 4 of that report lists ten problems to which KNAPSACK reduces. Part (a) shows that total completion time on one machine is already hard when a single job has a nonzero release date and all weights are equal.
The result is a sharp boundary. With all release dates zero the problem is easy; with one nonzero release date it is NP-complete. It is a standard entry in the complexity classification of single-machine problems that later surveys (Lawler, Lenstra, Rinnooy Kan and Shmoys, 1993) and the scheduling-complexity databases build on.
An instance of KNAPSACK consists of positive integers and ; with , it has a solution if for some .
In the scheduling problem there are jobs and one machine. Job has a processing time , a weight and a release date , all nonnegative integers. A schedule assigns each job a starting time ; the job completes at , and no two jobs are processed at the same time. The problem written in the paper's notation is the class of instances in which every weight is and every job except the last one, , has release date . Its recognition version asks, given such an instance and an integer , whether some schedule has .
A problem is reducible to (written ) when every instance of can be transformed in polynomial time into an instance of with the same answer. The paper's construction maps (with and ) to an instance with jobs in four groups , , and , with processing times , , and , the release date , and threshold , where , , , , are explicit polynomials in , , and .
stated as CookPvsNP.PolyReducible knapsackLang sumCLangMult: a polynomial-time computable map on binary strings that sends codes of solvable KNAPSACK instances, and only those, to codes of yes-instances of the scheduling problem.
Together with the NP-completeness of KNAPSACK (Theorem 2(b), quoted from Karp), Theorem 4(a) shows that is NP-complete; with general release dates the problem is then NP-hard as well. The hardness here is in the ordinary sense: the construction is polynomial only in the multiplicity encoding (see below), and the reduction is from KNAPSACK, which has a pseudo-polynomial algorithm.
The result is proved on paper. A formalization adds a machine-checked complexity reduction whose correctness proof is a sequence of delicate counting estimates with large explicit constants; the paper closes the converse with "as is easily seen", and the forward computation and claims (C), (D) contain displayed identities that a formal proof must verify exactly. The definitions (single-machine schedules with release dates, the schedule of a processing order, the multiplicity encoding) are reusable for the other single-machine reductions of the same paper and for later classification results.
The forward direction is a direct computation. The converse is where the difficulty lies: a schedule with is arbitrary, may contain idle time, and may interleave the groups. Such a schedule must be shown to be rigid (claims (A)–(D)), and the claims are statements about every schedule, not about a convenient one. Each step compares sums of the form against with an additive slack smaller than , so the constants must be tracked exactly; an estimate that loses a single breaks the argument. Extracting the knapsack subset at the end requires recognizing which jobs fill and why their extra lengths sum to exactly .
For the goal, the polynomiality of the reduction is not automatic: the constructed instance has and jobs, which is exponential in the length of the binary KNAPSACK input. The paper's Remark (p. 23) resolves this by encoding groups of identical jobs by their cardinality and one copy of their data, and the formal statement adopts that encoding.
CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (polynomial-time many-one reducibility in Cook's machine model). Numbers are coded in binary over the four-letter alphabet BSym with encNats from the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's formalization); its own subsetSumLang allows zero entries, so KNAPSACK over positive integers is defined here.Fin n, 0-based; the groups , , and are index ranges. Starting times are natural numbers: the paper computes them from processing orders on integer data (Section 3), and claim (D) is false for real starting times.CookPvsNP model.The Kolmogorov–Smirnov statistics measure how far the empirical distribution of a sample lies from a hypothesised distribution. They are the standard goodness-of-fit test for continuous data, and their tail probabilities are the basic tool for confidence bands around a distribution function. A test is only usable at a fixed sample size if those tail probabilities are controlled for every , not just in the limit.
Timeline.
Let () be independent, identically distributed real random variables with a continuous distribution function . The empirical distribution function is
and the centred, normalised empirical process is . The statistics are
In Lean the sample is X : Fin n → Ω → ℝ, independent (iIndepFun X P) with common law μ (HasLaw (X i) μ P), is cdf μ, and the statistics are Dplus μ X, Dminus μ X, Dtwo μ X. The parameter is written l.
The proof works with Smirnov's point probabilities , whose sum over is , with Csáki's density of the first passage of a Brownian bridge at level , and with the ratio .
For every and every , with ,
Here is the minimum. The constant in front of the exponential is the point of the theorem; the threshold on is the paper's.
The milestones follow the proof in the paper's order of attack:
The equality in law of and , Comment 1 ((1.4) whenever ), the reduction , and Corollary 1:
The result. Theorem 1 and Corollary 1 give non-asymptotic Kolmogorov–Smirnov bands with the asymptotic constants, and , which cannot be improved because of the limit laws. Corollary 1 is the form in which the DKW inequality is quoted throughout statistics and learning theory: confidence bands for distribution functions, sample-size calculations for quantile estimation, and as a building block in bandit and empirical-risk analyses. Comment 1 says that the one-sided test is never anti-conservative at levels up to 50%, whatever the sample size.
Formalizing it. The result is proved on paper but not machine-checked. A formal development would give a verified, constant-explicit DKW inequality that downstream statistical results can import as a black box instead of carrying an unspecified . The milestones also produce reusable pieces: Smirnov's exact law of the one-sided statistic, the Brownian-bridge first-passage integral, and a family of explicit elementary inequalities. The proof uses computer-checked numerics ((2.15), Lemma 2, ); turning those into checked certificates is part of the work.
The obvious route is to compare the exact sum (2.3) term by term with the integral (2.4). The local comparison is only nearly true: a corrective factor is needed, and it is largest on the tail, where the crossing time is close to . Controlling that factor uniformly in while keeping the leading constant exactly is what forces the delicate constants (, , , ). For small the analytic bounds are too weak, and the proof closes the gap with a Lipschitz bound on plus a finite numerical check over a grid; neither half suffices alone.
Conventions:
Fin n; is cdf μ with Continuous (cdf μ) assumed, as in Theorem 1.ENNReal.ofReal of the bound. Each supremum defining a statistic is of a function with values in , hence a genuine real supremum.Additions and corrections relative to the page, each disclosed in its item: the printed slips in (2.1) (range of ), (2.8) (swapped numerators) and Proposition 2(i) ("" for nonincreasing) are corrected; Claim 2 carries the hypothesis , without which the corrected claim is false; Lemma 3 uses strict inequalities ; Comment 1 makes the implicit explicit; (2.14) carries Proposition 2's standing range , .
The goal does not mention , , , the case split at , or the computer check; a formalization of the goal through those objects, or with the threshold read as a maximum instead of a minimum, would be a different and weaker statement.
Infrastructure a complete development needs: the empirical process of an i.i.d. sample and its reduction to the uniform law by the probability integral transform; Smirnov's exact one-sided law (a ballot-type combinatorial identity); Gaussian-type integrals on ; elementary but delicate real inequalities; and certified interval arithmetic for the numerical steps. The first two are reusable for any work on empirical processes. Contributions on any milestone are welcome, in particular formal proofs of (2.3), of the numerical steps, and of the companions.
Alan S. Manne's Linear Programming and Sequential Decisions (Management Science 6(3), 1960, pp. 259–267) is the first formulation of an infinite-horizon, average-cost sequential decision problem as a linear program. The illustration is a single-item inventory problem, but the construction, with unknowns indexed by a state and a decision and constraints expressing statistical equilibrium, became the standard state–action frequency linear program of Markov decision processes. Later LP approaches to average-cost Markov decision processes, including constrained ones, build on it.
Timeline of the LP approach to average-cost problems:
A positive integer bounds inventory accumulation; the stock levels are . At the start of a month the initial stock is observed and a production quantity is chosen; the available stock is . The month's demand is independent of everything else and has law . Backlogs are excluded, so the terminal stock is , which becomes the next initial stock. A finite set of admissible pairs , all with and containing for every , lists the decisions available at each stock level. Costs are three arbitrary real functions: of the initial stock, of the production quantity, and of the shortage level.
A stationary randomized decision rule is a conditional probability of producing at stock , supported on admissible pairs. It makes the initial stock a Markov chain. A statistical equilibrium of is a stationary distribution of that chain: the law of the terminal stock equals the law of the initial stock, (2). The expected monthly cost (1) of in the equilibrium is
the expectation taken under the joint law of (initial stock, production, demand).
The linear program has one unknown per admissible pair, the joint probability of (initial stock , production ). Its constraints are , (4) , and the equilibrium equations
and its objective (9) is with the cost coefficients (10)
The companion equation (8.0) for has right-hand side and is omitted from the constraints. A feasible is decoded into and .
The paper labels no theorem or lemma. The goal is assembled from §1 (third paragraph), §3 (N.B.), §4 (last two paragraphs), §5 and §7 (3), and every milestone is cited by section, display, table or footnote.
Assume for every admissible pair. Then the linear program has an optimal solution, and for every optimal solution , with decoding , is a stationary randomized rule, is a statistical equilibrium of , and
for every stationary randomized rule and every statistical equilibrium of .
The result turns an infinite-horizon control problem into a finite linear program. Equilibrium joint laws of (state, decision) under stationary randomized rules are exactly the feasible points of a polytope, and the average cost is linear on it. Consequences include computability by the simplex method; an economic reading of the dual variables (Manne's footnote 5 interprets them as the relative advantage of starting at a given stock level, related to Bellman's functional equation); and, in later work, the treatment of side constraints, which dynamic programming handles poorly.
The result is classical and proved in the paper (largely by inspection of the definitions). It has not been formalized. The formalization adds three things. First, a precise statement of what is optimized when the chain of a rule is not irreducible: the paper's §7 (3) concedes that a "decomposable" optimum makes the equilibrium depend on initial conditions, and the goal resolves this by optimizing over (rule, equilibrium) pairs. Second, an explicit treatment of the stock levels the equilibrium never visits, where the paper's quotient is undefined. Third, a machine-checked numerical example whose LP is derived from the general definitions, not entered by hand. Derman's later irreducible-case version exists on the platform as a separate open statement; this mission covers Manne's irreducibility-free version on state-dependent action sets.
Each step is elementary; the work is bookkeeping across three descriptions of the same object. The equilibrium is defined through the transition kernel of the controlled chain, the LP through the displayed sums over with conditions and , and the cost through the joint law of three variables. Identifying them needs a reindexing of the admissible pairs by stock level, the interchange of a finite sum with an infinite sum over demands, and . The naive argument "the LP constraints are the equilibrium equations, so the LP optimum is the optimal rule" skips two points. The constraints omit (8.0), so equilibrium at stock level must be recovered from (4) and the bound . And the decoding fails at unvisited stock levels unless a default action is supplied. Existence of an LP optimum requires compactness of the feasible polytope, not just its nonemptiness.
All statements live in the namespace ManneLP.Equilibrium. Conventions:
Finset (ℕ × ℕ) with and every ), a demand law with and HasSum p 1, and costs , . The shortage level is an integer; no convexity, sign or monotonicity of the costs is assumed.tsums; the demand is not assumed bounded. The goal and the cost identity assume the expected shortage cost at each admissible pair is finite (absolutely summable), which the page takes for granted.Trivializing formalizations are ruled out: equilibrium is not defined as (8) (which would make milestone 2 vacuous), (8.0) is not a constraint (which would make milestone 3 vacuous), the cost is not defined as (which would make milestone 5 and the goal's cost clause definitional), and the optimality comparison ranges over all rules and all of their equilibria, not over irreducible chains or pure rules.
Contributions welcome: proofs of the milestones and the goal; computations of the §6 example from the general definitions; reusable lemmas on stationary distributions of finite stochastic matrices and on the existence of LP optima over compact polytopes.
The simplex method and every other edge-following linear programming algorithm moves from vertex to vertex of the feasible region along its edges. The number of steps such an algorithm needs in the worst case is at least the combinatorial diameter of the feasible polyhedron: the largest distance, counted in edges, between two of its vertices. Klee and Walkup introduced the two functions that measure this worst case, for polyhedra and for bounded polyhedra of dimension with facets, and wrote that "represents, in a sense, the number of iterations required to solve the 'worst' linear program of inequalities in variables using the 'best' edge-following algorithm" (Klee and Walkup 1967, p. 54).
The Hirsch conjecture, reported by Dantzig in 1963, asserted . Its diagonal cases and are the general and the bounded -step conjectures.
Timeline.
A polyhedron in is a nonempty set ; a polytope is a bounded polyhedron. is a -polyhedron with facets when it has nonempty interior and none of the inequalities is redundant; then the rows are in bijection with the facets, and row is tight at exactly when lies on the -th facet. The vertices of are its extreme points. Two vertices span an edge when the segment is an extreme subset of . A path of length is a sequence of edges , and is the least length of a path from to . Then
is simple when every vertex lies on exactly facets. A face is itself or the intersection of with a supporting hyperplane, never ; its dimension is that of its affine hull. A -path from to is a sequence of faces with , , and . A -dimensional Dantzig figure is a -polyhedron with facets and two vertices such that exactly facets are incident to and the other to . A -polytope has property A when it has between and facets and the following holds: if its facets are split into two classes of at most facets each, and both sets , of vertices all of whose facets lie in , respectively , are nonempty, then some vertex of is joined to some vertex of by a path of length at most .
In two halves: every -polytope with facets satisfies for all vertices , and some -polytope with facets has two vertices with .
The result. By the paper's reductions, for a given is equivalent to the bounded Hirsch bound for every . So 4.3 gives for all , which is the column of the paper's Fig. 2. Since Santos's counterexample, the smallest with is a well-defined open number. This theorem was the first to show it is at least ; later computer-assisted work treated further small cases, including the bounded -step case (Bremner and Schewe 2011). Santos's construction starts from exactly the reduction to Dantzig figures (the "strong -step theorem" for spindles) that this paper uses.
Formalizing it. The result has been proved since 1967; no machine-checked proof of exists. The platform has the Hirsch bound in dimension (Hirsch.dimension_three_bound, Hirsch.klee_three_dimensional_bound), the Klee–Walkup wedge reduction at the level of inequality descriptions (Hirsch.balanced_hpoly_transfer), products (Hirsch.diamLE_prod) and Santos's counterexample. The mission adds the facial-path calculus of §3 and the property-A argument of §4. Both are reusable in any later formal treatment of small -step cases.
The obvious approach, a direct case analysis of -polytopes with facets, is out of reach: there are far too many combinatorial types, and nothing bounds the search. The paper first reduces to simple polytopes, and the reduction itself (2.8) rests on a perturbation lemma (2.6) whose proof is deferred to a separate paper by Walkup: simplicity must be gained without shrinking any distance. The facial-path results then pass between bounded and unbounded figures through truncation and the wedge (3.1), and a statement about all unbounded -dimensional figures is what yields one about bounded -dimensional ones. Finally the -face must be shown to have property A. That property fails for some simple polytopes of classes and (p. 69), so 4.2 depends on the dimension being and on the facet count being at most . Its proof uses Euler's relation and Balinski's theorem that the graph of a -polytope is -connected (posed on the platform as Balinski61.Connectivity.disjoint_paths_between_vertices).
Polyhedra are Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d); edges and walks are Hirsch.Adj and Hirsch.Reach from the published Hirsch_model and Hirsch_walk. The conventions are:
Hirsch.Reach P L x y, a walk of steps that may stand still. is an upper bound for every polytope plus a witness, never a supremum of reals. A version proving only the upper bound, or only the lower bound, is not the goal.Fin (2 * d) rows.Set.encard.The paper cites two inputs without proving them: Lemma 2.6 (Walkup's simple perturbation) and Balinski's theorem. A complete development needs face lattices of H-polyhedra, wedges and truncations, and the planar-graph arguments of 4.2. The face and facial-path layer is reusable for the companion mission on and for other diameter problems. Contributions are welcome at every milestone, including proofs of 2.6.
The linear complementarity problem asks, for a real square matrix of order and a vector , for a vector with
It is the common form of the Kuhn–Tucker conditions of linear and convex quadratic programs and of the equilibrium conditions of two-person non-zero-sum (bimatrix) games. In 1964 Lemke and Howson gave a constructive existence proof for equilibrium points of bimatrix games by following a path of adjacent extreme points of a polyhedron (Lemke–Howson 1964). In 1965 Lemke adapted that path-following technique to the general problem above, under a condition on that covers the positive semidefinite case treated by Dantzig and Cottle and the case (Lemke 1965). The resulting procedure, now called Lemke's algorithm or complementary pivoting, became a standard method for linear complementarity problems and a template for later path-following existence proofs (Cottle, Pang, Stone 1992).
Timeline:
Fix a finite index set of size , a real matrix and . Inequalities between vectors are componentwise and is the all-ones vector.
Suppose is non-degenerate and that for every
Then
The Corollary (p. 5: , gives an odd number of equilibrium points), Theorem 3 (p. 5: if for all , at most one equilibrium point) and Theorem 5 (p. 8: if moreover , has at least rays).
Theorem 4 is an existence theorem for a class of linear complementarity problems that contains convex quadratic programming (the case for all ) and strictly positive matrices, and its proof is an algorithm: the path followed is the sequence of pivots of Lemke's method. The parity statements (Theorem 2, the Corollary) are an early instance of the path-following parity arguments later abstracted in the complexity class PPAD (Papadimitriou 1994).
The theorem is classical and proved. To our knowledge neither Lemke's theorem nor the polyhedral path machinery of Theorems 1–2 has a machine-checked proof in Lean or Mathlib. This mission produces the vocabulary of non-degenerate complementarity polyhedra (the matrix , open edges, rays, adjacency paths), the parity theorem, and the existence theorem itself; the Farkas-type Lemma 2 (p. 4) is already available on the platform.
The algebraic part (Lemma 3 and (22)–(25)) is short. The difficulty is combinatorial-geometric: Theorem 1 requires that, under non-degeneracy, every extreme point of has exactly incident edges, that each point of is an extreme point or lies on an open edge, and that the edges contained in form paths whose end-points are exactly the equilibrium points; the parity of Theorem 2 then needs finiteness of the set of extreme points. None of this polyhedral structure (edges as zero-pattern classes, their closures and end-points) is in Mathlib. Moreover, the printed proof of Theorem 4 applies Theorem 2 to , whose non-degeneracy the paper obtains from an informal perturbation remark, and it sketches the step from the end of the augmented path to a ray of ; a complete proof of the goal must supply these steps or take another route.
Contributions welcome: the polyhedral lemmas for non-degenerate (extreme points have edges, finitely many extreme points), the parity argument, and any complete route to Theorem 4.
Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.
Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.
A short history of the model:
There are tasks . Task has a length and a preferred midtime . A schedule assigns every task a starting time such that no two tasks overlap on the single processor: for , either or . Idle time is allowed. The actual midtime of is , and the total discrepancy of is
The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times are interchangeable through .
Total discrepancy (the decision problem). Given and , is there a schedule with ?
Even-odd partition. Given positive integers , can they be split into two sets of equal sum so that each set contains exactly one of for every ?
The special case. For tasks with and one common preferred midtime , write and . A schedule is ordered if, on each side of , shorter tasks lie nearer to . The bracket is the schedule that puts at midtime and packs the listed tasks against it in the listed order.
The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.
THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at , the -th pair of lengths in the -th positions on either side, either member on either side. This characterization holds independently of the reduction.
The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with , so they must be restated for every . Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.
The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint never binds. In D the midtime is , exactly half the total length, and the reduction works because the constraint binds. The tasks before must fit in , and the extra task must sit at . Together these force the two sides to have equal total length. A proof that only cites the large- lemmas proves nothing about D. Conversely, dropping makes the reduction false: put the shorter element of every pair after .
The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of , double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.
Fin N from . In the special case is index , and the paper's () are the indices for .CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.
A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.
The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.
Let be the initial stock and the time to go. The seller first charges price and may change once to a lower price . Demands at the two prices are independent Poisson counts with positive rates and . A lower price produces more arrivals, so and . Feng and Gallego also assume that lowering the price increases the revenue rate: . There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.
Write for the observed sales count at the initial price by time . If the price changes at deterministic time , let be the expected total revenue. The count after the change is independent of , and their sum has Poisson mean . The optimal value allows the switch time to depend on the counts observed so far. An admissible lies between zero and , is a stopping time for the history of , and occurs before stock is exhausted almost surely. At , is the revenue from charging immediately. The paper defines these quantities in §3, pp. 1377–1379.
The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence of inventory-dependent thresholds. When , switching immediately earns the optimal value; when , a correction is added:
The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with . For , set , where is the Poisson-tail expression from §4.1. The threshold is the first nonnegative zero of . A function satisfies for positive time and ; is zero below and equals at and above it. If is the first zero of , the theorem also gives and for .
Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.
The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.
The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.
The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory depends on the correction at stock . Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of , the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.
The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.
Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.
The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.
For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.
Scheduling jobs on parallel machines under precedence constraints is the core model of project and parallel-processing scheduling: a job may start only after its predecessors have finished. Two criteria dominate the literature, the makespan (when does the last job finish?) and the total completion time (how long do jobs wait on average?). Knowing that one criterion is at least as hard as the other lets a hardness proof for one transfer to the other without a new reduction from a combinatorial problem.
Brucker, Lenstra and Rinnooy Kan's report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; later in Annals of Discrete Mathematics 1, 1977) collected the complexity status of the standard scheduling problems and stated a set of elementary reductions among them as Theorem 1. Part (l) reduces makespan to total completion time for identical machines with precedence constraints and bounded processing times.
Timeline.
An instance has jobs , a number of identical machines, a processing time for each job, and a precedence relation on the jobs: means that may start only after has completed. Each job is one operation, processed without interruption on any one machine. For a constant , the class requires for every job and an acyclic precedence relation.
A schedule assigns to every job a machine and a starting time ; the completion time is . It is feasible if two jobs on the same machine never overlap and implies .
Following the paper, each optimization problem is replaced by its recognition version. Problem asks, for an instance and a threshold , whether some feasible schedule has . Problem asks, for an instance of the same class and a threshold , whether some feasible schedule has (all weights ).
is reducible to , written , if every instance of can be transformed in polynomial time into an instance of with the same answer.
For every constant ,
The result. Theorem 1(l) makes the total completion time problem at least as hard as the makespan problem in the same class. Combined with Ullman's NP-completeness results and Theorem 1(b) (reducibility transfers NP-completeness), it shows that minimizing on identical machines with precedence constraints is NP-complete, already for two machines with and for unit processing times on machines. These are two rows of the paper's Table III.
Formalizing it. The result is proved on one page of a typewritten report; no machine-checked version exists. The mission produces a scheduling model for identical machines with precedence constraints, binary languages for the two recognition problems, and the reduction in Cook's Turing-machine model. The proof's displayed bounds contain a misprinted index range, which the formal statements correct.
The two criteria are not monotonically related: a schedule with a smaller makespan can have a larger total completion time than one with a larger makespan. So the obvious reduction, keeping the instance and asking for , is not an equivalence: a no-instance of can have a schedule with small total completion time. The instance has to be changed so that the total completion time is governed by the makespan, and the comparison of the two thresholds must be exact, including the strict inequality on the "no" side, which depends on integral completion times and positive processing times.
The main formal difficulty lies in the reduction itself. A polynomial-time Turing machine must decode the binary instance, check that it belongs to the class (including acyclicity of the precedence relation), compare with , and write out an instance with additional jobs and a quadratic-size precedence matrix. The size of that output is polynomial only because is a constant: a version with part of the input would make exponential in the input length.
Fin n, Fin m). Starting times are natural numbers; Section 3 derives all times from processing orders on nonnegative integer data, and both criteria are regular. "" is written as " for every ".CookPvsNP_defs; numbers are written in binary with the alphabet and code encNats of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). The unit-time model ResourceScheduling.Chain.Model (Błażewicz, Lenstra and Rinnooy Kan) has the same feasibility conditions but unit processing times and real start times, so the model here is defined anew.In a no-wait flow shop every job passes through the machines in the same order, and once it has started it may never wait between two machines. The constraint comes from processes in which the material changes state if it is left standing, such as hot metal rolling, chemical and food processing, and some pharmaceutical lines; see the survey of Hall and Sriskandarajah (doi:10.1287/opre.44.3.510). The question of how hard it is to schedule such a shop well is the question this mission formalizes.
Brucker, Lenstra and Rinnooy Kan settled it for the case in which the number of machines is part of the input. In their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977, doi:10.1016/S0167-5060(08)70743-X), Theorem 5 reduces DIRECTED HAMILTON PATH to the no-wait flow shop. Both minimizing the makespan and minimizing the total completion time are thereby NP-complete.
Timeline.
There are jobs and machines. Job needs processing time on machine . Write
for the time job spends on its first machines. Because a job never waits, a schedule is determined by the start times . The operation of on occupies , and job completes at . A schedule is feasible when no two distinct jobs occupy the same machine at the same time. The delay
is the least gap that lets follow on every machine.
A directed graph on has a Hamilton path if its vertices can be ordered with every .
From the paper builds an instance with jobs and machines. Each ordered pair of distinct jobs is assigned a middle machine , and the partial sums are perturbed from by or on the machines and just before the machines , depending on whether the pair is an arc. The parameters satisfy and .
where is polynomial-time many-one reducibility between the binary-coded recognition languages.
The result. Theorem 5, together with the NP-completeness of DIRECTED HAMILTON PATH, places both no-wait criteria among the NP-complete problems once is part of the input. The Gilmore–Gomory algorithm for two machines therefore cannot be extended to arbitrary unless P = NP, and heuristics and exact exponential methods for no-wait shops are justified. The reduction also gives a structural fact of independent use: every directed graph can be realized, up to two arc-weight values, as the delay matrix of a no-wait flow shop.
Formalizing it. The result has been proved for fifty years; to our knowledge no machine-checked version exists. This mission produces a checked no-wait flow shop model, a checked travelling-salesman reformulation of it, the correctness of the paper's construction, and a polynomial-time reduction in an explicit Turing-machine model. It also records a gap in the printed proof: the ordering the paper calls easy to construct does not exist for .
Three steps are not routine.
Jobs and machines are -based (Fin n, Fin m); cum p ℓ i is the paper's , and the machine indices are the paper's -based indices. Start times are natural numbers, and release dates are . Section 3 computes times from processing orders on integer data, and every criterion is regular, so real start times would not change the yes-instances. A zero-length operation occupies the empty interval. is stated as for every job. The delays, the partial sums of the construction and its processing times are computed in . The instance uses their conversion to , which is exact by milestone 4. The threshold of Theorem 5(b) is compared in , as printed.
The paper's loose phrases are made explicit as follows:
Directed graphs are Boolean adjacency matrices. A graph with or vertices has a Hamilton path, and a one-vertex graph has a Hamilton circuit iff it has a loop.
The goal is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs, with polynomial time measured on Cook's one-tape Turing machines. Instances are coded with the alphabet BSym and binary code encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). A graph is coded as followed by its adjacency matrix; a flow-shop instance as , , the matrix and the threshold .
Stating only the equivalences 6–7 and calling the result "reducible" would drop polynomiality; the goal therefore asserts PolyReducible. The target languages contain exactly the no-wait flow-shop instances, with no waiting allowed, so the reduction cannot land in a looser problem. The parameters always carry , .
Contributions are welcome at every level:
Many decision problems in control, finance and engineering must hold against an uncertain parameter whose distribution is unknown, while samples of (measurements, historical records, simulations) are available. The scenario approach replaces the uncertain constraint by the constraints of the observed samples and solves the resulting convex program. The open question is then how robust its solution is: with what probability does a new, unseen violate it?
The classical answer, due to Calafiore and Campi (doi:10.1007/s10107-003-0499-y, 2005; doi:10.1109/TAC.2006.875041, 2006) and sharpened by Campi and Garatti (doi:10.1137/07069821X, 2008), is an a-priori bound: it depends only on and the dimension , and it is tight for the worst problems. It is conservative for the many problems whose solution is determined by far fewer than samples. Campi and Garatti's wait-and-judge theorem (doi:10.1007/s10107-016-1056-9, Math. Program. 2018) replaces it by an a-posteriori certificate: after solving, count the samples that actually determine the solution and certify the solution at a level that depends on that count.
Timeline:
The decision variable is . A problem consists of a cost vector , a convex domain , convex constraint sets indexed by in a probability space , and convex tie-break functions . Given an i.i.d. sample with , the scenario program is
Ties are broken by minimising among the minimisers, then , and so on; the resulting solution is .
The variational problem (10) is: for a function ,
For every -valued , under Assumptions 1 and 2,
The level is evaluated at the observed number of support constraints. The goal fixes no particular , which keeps it stable under any later choice of levels.
Theorem 1 turns the number of support constraints, which is observed after solving, into a confidence statement that holds uniformly over all convex problems and all distributions. With Theorem 2's choice of , a user who finds support constraints obtains a level comparable to that of a -dimensional problem, which is far below the a-priori level for dimension . The classical bound (2) is recovered as Corollary 1, so Theorem 1 contains the earlier theory.
The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization produces:
The obvious approach bounds the probability for each value of separately by a binomial tail, then sums. This fails: the event is not known in advance, and summing the individual bounds over loses the uniformity that makes the result useful. The paper instead characterises every convex problem by the -tuple . It then maximises (17) over all tuples satisfying the infinitely many moment conditions (18), which is a generalized moment problem in measures, and solves it by duality.
Two steps carry most of the work. One is the almost-sure identity , which depends on the precise interplay of Assumptions 1 and 2 with the tie-break. The other is passing from the polynomial dual problems to the variational problem (10), which needs a density argument in . The bound itself is quoted from the earlier literature; it needs a Helly-type argument adapted to the lexicographic tie-break.
EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and samples are Fin N → Δ, indexed from . is a probability measure and is the product measure.ContDiffOn ℝ d on , with derivatives taken within . is a real infimum over a set that is nonempty () and bounded below by .ENNReal.ofReal.Ruled-out trivializations:
Contributions welcome:
Measure.pi;Minimizing total weighted tardiness on a single machine, written , is one of the basic problems of deterministic scheduling. A job that finishes after its due date is penalized in proportion to its lateness and its weight. Practitioners use this criterion to model penalty clauses and customer priority. In the theory it was a reference problem for branch-and-bound methods and dominance rules throughout the 1960s and 1970s.
Close relatives are easy: with equal weights and a common due date, shortest-processing-time order is optimal. Whether the weighted problem admits a polynomial algorithm was open until the report of Brucker, Lenstra and Rinnooy Kan in 1975. Their Theorem 4(d) shows that KNAPSACK reduces to it, so the problem is NP-hard. The unweighted case is listed there as open (Section 5) and was settled only later by Du and Leung (1990).
Timeline:
A KNAPSACK instance consists of positive integers and . It is a yes-instance if some subset satisfies . Write and .
An instance of consists of jobs. Job has a processing time , a weight and a due date , all nonnegative integers, and every job is available at time . A schedule gives each job a start time , and no two jobs may overlap on the machine. Job completes at and has tardiness . The instance with threshold is a yes-instance if some schedule satisfies . A processing order determines the schedule without idle time, in which .
Reducibility (Section 2 of the paper) is polynomial-time many-one reducibility between the recognition versions. A polynomial-time Turing machine must map codes of KNAPSACK instances to codes of scheduling instances so that yes-instances map exactly to yes-instances.
The paper's construction has jobs: for , , , ; for each of the dummy jobs, , , . The threshold is , with and . The proof is phrased in terms of , the amount by which the -th job of the order misses the common due date.
stated as CookPvsNP.PolyReducible SchedComplexity.OneMachine.knapsackLang wtLangMult. The scheduling side uses the multiplicity encoding of the paper's Remark (p. 23), in which a class of identical jobs is written once together with its cardinality.
Each milestone is a statement of the paper's proof (pp. 20–21) about the construction above, for every admissible :
The theorem places among the NP-hard problems, so (unless P = NP) the research on it has to aim at enumerative methods, pseudopolynomial algorithms or approximation, not at an exact polynomial algorithm. Together with the companion reductions of Theorem 4, it drew the boundary between easy and hard single-machine problems that the later classification of Lageweg, Lawler, Lenstra and Rinnooy Kan made systematic.
The result is proved in the paper, and Lawler's later strong NP-hardness proof supersedes it. No machine-checked proof is known to exist. A formal proof adds three things. It makes the paper's "it is easily seen" steps and the encoding argument of the Remark explicit. It produces a reusable single-machine tardiness model with processing orders. It also fixes a gap in the printed construction: the printed need not be an integer.
The equivalence is not a local exchange argument. The threshold must separate orders with from all others, and the objective is a quadratic function of the order. The orders with can still differ in by the cross terms and by how the late jobs are arranged. The construction therefore needs a slack that absorbs these terms, and a scale large enough that a nonzero always costs more than the slack. Keeping exact track of every constant, including and , is where errors creep in.
Polynomiality is a second, separate difficulty. The construction has jobs, which is exponential in the binary length of the KNAPSACK input. The goal holds only for the encoding of the Remark, and a solver must also produce an explicit polynomial-time Turing machine.
Fin n, numbered from ; a processing order is Equiv.Perm (Fin n) with π i the paper's . posCompletion p π k is the paper's for the 1-based position .CookPvsNP.PolyReducible from the published CookPvsNP_defs. Codes use the alphabet BSym and the binary numerals encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). KNAPSACK is restricted to positive integers, so that encoding's subsetSumLang is not reused.Deterministic machine scheduling was one of the first application areas of the theory of NP-completeness. After Cook (1971) and Karp (1972) showed that a large family of combinatorial problems are polynomially equivalent, Brucker, Lenstra and Rinnooy Kan set out to locate the boundary between the polynomially solvable and the NP-complete scheduling problems. Their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, Report BW 43/75, 1975; journal version in Annals of Discrete Mathematics 1, 1977) introduced the four-field notation that, in refined form, is still the standard classification of scheduling problems, and proved NP-completeness of the "easiest" hard problems by explicit reductions.
Single-machine problems with due dates sit right at that boundary. Minimizing the maximum lateness is solved by Jackson's earliest-due-date rule (1955), and minimizing the number of late jobs by Moore's algorithm (1968). Theorem 4 of the report shows that small changes to these problems — one release date, job weights, or due dates turned into deadlines under a weighted completion-time objective — make them NP-complete, by reduction from KNAPSACK. This mission formalizes four of those reductions, parts (b), (c), (e) and (f) of Theorem 4.
Timeline, as far as this mission is concerned:
A single-machine instance consists of jobs . Job needs units of processing on the machine , has a weight , a release date and a due date ; all data are nonnegative integers. A schedule assigns to each job a starting time such that the occupied intervals of distinct jobs are disjoint. Idle time is allowed; a job with occupies an empty interval. The completion time is , the lateness is (possibly negative), and is if and otherwise. The criteria are
The problem class is written in the field: by default every ; allows a nonzero release date for the last job only; fixes unit weights; admits only schedules that meet every due date. A problem is turned into a yes/no question by asking whether a schedule with value exists.
KNAPSACK (Theorem 2(b) of the report): given positive integers , is there a subset with ? Write .
A problem is reducible to , , if every instance of can be transformed in polynomial time into an instance of whose answer is the same.
as polynomial-time many-one reductions between languages of binary strings.
For positive with , and the paper's constructions:
The result. Combined with the NP-completeness of KNAPSACK, the four reductions show that the four problems are NP-hard (in the ordinary sense; they admit pseudo-polynomial algorithms). Part (c) shows that Jackson's rule cannot be extended to a single nonzero release date unless P = NP; part (f) does the same for Moore's algorithm; part (e) explains why weights are essential in the late-jobs problem; part (b) shows that deadlines turn the weighted completion-time problem, solved by Smith's ratio rule without them, into a hard one. These are entries of the complexity tables that every later scheduling classification builds on.
Formalizing it. The reductions are classical and proved on paper, in a few lines each: for (c), (e) and (f) the report gives only the construction and a figure. None of them has a machine-checked proof. A complete formalization supplies the explicit equivalence over all feasible schedules (including schedules with idle time and arbitrary processing order), the handling of the inputs the proof sets aside by "we may assume that ", and the polynomial-time computability of the constructions in a Turing-machine model.
Each equivalence has an easy direction: a subset with sum gives the schedule "jobs of , then , then the rest" (Figures 4 and 7 of the report). The other direction must rule out every feasible schedule, not only the idle-free ones in the displayed order. The report gives no argument for this direction in (c), (e) and (f), and for (b) only a computation for idle-free schedules of one shape. The equivalences are false outside in some cases (for (c), any makes every schedule on time), so the goal's reduction must treat those inputs separately.
The heavier part is polynomial-time computability: the reduction must be a function on strings, computed by a one-tape Turing machine within a polynomial number of steps, that parses a binary-coded KNAPSACK instance, computes and the threshold (for (b), a sum of products), and writes the coded scheduling instance — and maps malformed strings outside the target language.
Fin n (0-based; is the last index), with in each target language. Starting times are natural numbers: Section 3 computes them from processing orders on integer data, and since all criteria here are regular and release dates survive left shifts, real starting times give the same yes-instances. Feasibility requires disjoint occupied intervals, including empty intervals when . Idle time is allowed. Lateness is an integer.CookPvsNP.PolyReducible from the published definition CookPvsNP_defs. The alphabet and binary number codes are those of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann); its SUBSET SUM language is not reused because it admits zero sizes, while the paper's KNAPSACK is over positive integers.Parts (a), (d) and (g)–(j) of Theorem 4 are formalized in other missions of this series.
Deterministic machine scheduling asks how to process a set of jobs on a set of machines so that an overall criterion, such as the time at which the last job finishes, is as small as possible. In the early 1970s many such problems had efficient algorithms (Johnson's rule for the two-machine flow shop, Smith's ratio rule for a single machine, Lawler's rule under precedence constraints), while others resisted every attempt. The report of Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977) drew the line between the two groups systematically. It fixed the four-field notation that the scheduling literature still uses, and it proved NP-completeness of the "easiest" hard problems by explicit reductions in the sense of Karp.
The first family of reductions in the report, Theorem 3, concerns the simplest machine environment beyond a single machine: two identical machines. It shows that already there, minimizing the makespan and minimizing the total weighted completion time are as hard as PARTITION. These two reductions are simplified versions of reductions given by Bruno, Coffman and Sethi (1974), reference [3] of the report.
PARTITION. Given positive integers , decide whether there is a subset of with
Write for the total.
Two identical machines. There are jobs and two machines . Job has a processing time and a weight , and must be processed without interruption on one machine of its choice; all jobs are available at time . A schedule assigns to every job a machine and a starting time ; its completion time is . A schedule is feasible if no two jobs on the same machine are processed at the same time, i.e. the intervals on each machine are pairwise disjoint. Idle time is allowed. Two criteria are considered:
The problems and ask for a feasible schedule minimizing the respective criterion.
Reducibility. Following Section 2 of the report, each problem is replaced by its recognition version: given an instance and a threshold , is there a feasible schedule with value ? A problem is reducible to , written , if every instance of can be transformed in polynomial time into an instance of with the same answer. Instances are written as words over a finite alphabet, with every number in binary.
Both reductions use the same instance shape: jobs with .
every feasible schedule with this assignment has value at least . 3. The identity for . With ,
The result. Since PARTITION is NP-complete (Karp 1972), Theorem 3 shows that both problems are NP-hard with only two machines and a single operation per job; their recognition versions are NP-complete. Together with the single-machine and shop results in the rest of the report, it places the boundary of tractability in deterministic scheduling. The makespan problem became a standard source problem for later hardness proofs and a standard target for pseudo-polynomial algorithms and approximation schemes. The weighted completion time result contrasts with the single-machine case, which Smith's ratio rule solves in polynomial time.
Formalizing it. The theorem is classical and fully proved on paper; the report prints the constructions and, for (b), a short calculation. To our knowledge no machine-checked proof exists. The mission produces (i) a precise model of nonpreemptive schedules on two identical machines with integer start times and idle time allowed, (ii) the two yes-instance equivalences with the paper's rational thresholds, (iii) the ordering-independence statement for behind part (b), and (iv) the polynomial-time computability of the reductions in a Turing machine model. Part (iv) is the formal content of "reducible" and is missing from the paper.
For part (a) the mathematics is short. The paper treats it as evident; a formal proof must still handle schedules with idle time and the case of odd , where is not an integer.
Part (b) rests on the claim that, when , the value does not depend on the order of the jobs on a machine. For a single machine without idle time this is a symmetric double sum. A recognition-problem proof also needs the converse direction: no schedule with idle time beats the non-idle one, so every feasible schedule with assignment has value at least . The paper cites this rather than proving it.
The step the paper leaves out entirely is polynomiality. The constructions copy the input and compute or , and in a one-tape Turing machine model with an explicit polynomial time bound this needs binary arithmetic (sums, products, a floor) carried out on the tape. It also needs a decoder that rejects malformed words and lists containing a zero. This is routine in principle but long in practice.
Fin n and machines Fin 2 (machine 0 is ). Starting times are natural numbers. Section 3 of the report computes them from processing orders on nonnegative integer data, and both criteria are regular, so real starting times would give the same yes-instances. Processing times may be zero; a zero-length job occupies the empty interval. Schedules may contain idle time.CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (Cook's one-tape Turing machines, polynomial-time many-one reductions). The alphabet BSym and the binary code encNats are reused from the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). Its PARTITION language is not reused, because it allows zero sizes.BSym, which every mission of this series needs and which is reusable for other reductions on the platform.