Theoretical Computer Science

Graph Theory Linear Optimization·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms II: Every Product Multicommodity Flow Problem with k Commodities Has Ω(𝒮/log k) ≤ f ≤ 𝒮Research Paper

Why multicommodity max-flow and min-cut

For a single commodity, the Ford–Fulkerson theorem says that the maximum flow between two nodes equals the minimum capacity of a cut separating them. Many routing and partitioning problems involve many source–sink pairs at once, and for those the equality fails: the largest fraction of every demand that can be routed simultaneously can be strictly smaller than the sparsest cut. Leighton and Rao (J. ACM 1999, building on their FOCS 1988 paper) proved that the gap is at most logarithmic for broad classes of demand patterns, and turned the proof into the first $O(\log n)$ -approximation algorithms for sparsest cut, balanced separators, minimum feedback arc set, crossing number and VLSI layout problems.

This mission formalizes Section 2.3 of the paper: the extension of the uniform max-flow min-cut theorem to product multicommodity flow problems (PMFPs), where the demand between two nodes is the product of their node weights.

Timeline.

1956: Ford and Fulkerson, single-commodity max-flow = min-cut.
1963: Hu, equality for two commodities.
1988: Leighton and Rao (FOCS), $\Theta(\log n)$ gap for uniform demands; the product-demand extension, pointed out to them by Shmoys, Tardos and Sinclair, appears in the journal version (1999), Theorem 7.
1993–1995: Klein–Agrawal–Ravi–Rao, Garg–Vazirani–Yannakakis, Linial–London–Rabinovich and Aumann–Rabani extend the $O(\log k)$ gap to arbitrary demands with $k$ commodities.

Setting

A network is a finite vertex set $V$ with a symmetric capacity $C(u,v)\ge0$ on each pair, zero on the diagonal; $\{u,v\}$ is an edge when $C(u,v)>0$ . For $U\subseteq V$ , the cut capacity is $C(U,\bar U)=\sum_{u\in U,\,v\notin U}C(u,v)$ . The network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$ .

A PMFP is given by a node weighting $\pi:V\to\mathbb R_{\ge0}$ . Write $\mathcal P$ for the set of nodes with $\pi(u)\ne0$ , $p=|\mathcal P|$ , and $\pi(U)=\sum_{u\in U}\pi(u)$ . As in the paper, the weights are normalized so that $\pi(V)=p$ . Every pair $\{u,v\}$ is a commodity with demand $\pi(u)\pi(v)$ ; there are $k=\binom p2$ commodities with nonzero demand. The uniform problem is $\pi\equiv1$ .

The max-flow $f$ is the largest $\lambda$ such that $\lambda\pi(u)\pi(v)$ units of every commodity can be routed simultaneously, with the total flow on each edge (both directions) at most its capacity. The min-cut is

\mathcal S=\min_{U:\ \pi(U)>0,\ \pi(\bar U)>0}\frac{C(U,\bar U)}{\pi(U)\,\pi(\bar U)},

the quotient being the weighted ratio cost of the cut $\langle U,\bar U\rangle$ .

The dual objects are distance functions: lengths $d(e)\ge0$ on the edges, with total weight $W=\sum_eC(e)d(e)$ ; $d(u,v)$ is the shortest-path distance and $d(T,u)=\min_{t\in T}d(t,u)$ . The weighted distance constraint is $\sum_{\{u,v\}\in\mathcal P^2}\pi(u)\pi(v)d(u,v)\ge1$ .

Formalization targets

Goal: Theorem 7 (pp. 801–802)

There is an absolute constant $c>0$ such that every normalized PMFP with $p\ge2$ on a connected network satisfies

\frac{c\,\mathcal S}{\log_2\max(k,2)}\le f\le\mathcal S .

The goal leaves the constant unfixed, which is the paper's $\Omega(\cdot)$ .

Milestones, in the order the proof uses them

Weak duality (§1.2, pp. 789–790): $f\,\pi(U)\pi(\bar U)\le C(U,\bar U)$ for every cut with positive weight on both sides.
LP duality for the PMFP (p. 802 with p. 796): distance functions satisfying the weighted constraint have $W\ge f$ , and one attains $W=f$ .
Lemma 8 (p. 802): a partition whose components meeting $\mathcal P$ have radius at most $\Delta$ and whose cross capacity is at most $4W\log p/\Delta$ .
Corollary 9 (p. 802): either a set $T$ of radius $1/2p^2$ with $\pi(T)\ge2p/3$ , or a cut of weighted ratio cost $O(W\log p)$ .
Lemma 10 (p. 802): a heavy set $T$ far on average from the remaining weight yields a cut of weighted ratio cost $O(W)$ .
Lemma 11 (p. 803): a distance function satisfying the weighted constraint yields a cut of weighted ratio cost $O(W\log p)$ .

Stronger companions

$\mathcal S\le36\log_2\max(k,2)\cdot f$ , the constant of the paper's proof.
Theorem 7 without the normalization $\pi(V)=p$ , which the paper assumes "without loss of generality".

Significance

Theorem 7 bounds the multicommodity flow–cut gap by $O(\log k)$ for every product demand pattern, so an optimal dual distance function certifies a cut within $O(\log k)$ of the sparsest weighted cut. The paper itself applies it to reversible Markov chains (§3.27, p. 827). There the node weights are the stationary probabilities, and Theorem 7 shows that the inverse conductance and the resistance of a chain agree up to a $\Theta(\log p)$ factor, where $p$ is the number of states with positive stationary probability.

Theorem 7 was proved in 1988–1999 and is subsumed, up to the constant, by the general $O(\log k)$ bound for arbitrary demands (Linial–London–Rabinovich 1995; Aumann–Rabani 1998). It has no machine-checked proof, and neither has any of its milestones. A complete development would also be the first formal treatment on Prove2Me of concurrent multicommodity flow, its LP dual, and region-growing (low-diameter) decompositions, which recur across approximation algorithms and metric embeddings.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the work. Rounding an optimal dual distance function to a cut fails directly: thresholding distances from a single node gives no control on the ratio when the weight is spread out. The paper's argument needs a decomposition of the graph into components of small radius that cuts little capacity, with a loss of only $\log p$ , not $\log n$ : the regions must be grown from weighted nodes only, while the many zero-weight nodes still sit inside the graph and its capacities. It must then separately handle the case where one component carries two thirds of the weight. Formally, the LP duality step alone requires a strong-duality statement for a linear program with one constraint per path, exponentially many, which Mathlib does not provide in this form.

Formalization scope

All objects live in the namespace LeightonRao.Product in a single definitions file.

Network and graph. A network is a symmetric nonnegative capacity function on a finite type with zero diagonal. The graph has an edge where the capacity is positive.
Commodities. One commodity per ordered pair $u\ne v$ , with demand $\tfrac12\pi(u)\pi(v)$ each way (the paper's footnote 7). The total demand of a pair is then $\pi(u)\pi(v)$ , and the demand separated by $U$ is $\pi(U)\pi(\bar U)$ .
Max-flow. Flows are arc flows per commodity. The max-flow is the supremum of the feasible values $\lambda\ge0$ .
Min-cut. The min-cut ranges only over cuts with $\pi(U)>0$ and $\pi(\bar U)>0$ . On the other cuts the paper's quotient is undefined; reading it with Lean's division by zero would make $\mathcal S=0$ and the goal trivial.
Distances, radius, cross capacity. Graph distances are infima of walk lengths. The radius of a component is measured by walks inside the component. Cross capacity is the capacity between different parts of a Finpartition.
Logarithms. $\log$ is $\log_2$ (the paper's footnote 3). For $p=2$ there is one commodity and $\log k=0$ , so the goal uses $\log_2\max(k,2)$ .
Constants. The $O(\cdot)$ constants of the milestones are the ones computed in the paper's proofs: $36$ in Corollary 9 and Lemma 11, $6$ in Lemma 10.
Hypotheses added to the page, each disclosed in its statement:
- $\Delta>0$ in Lemma 8, where the page says $\Delta\ge0$ but divides by $\Delta$ ;
- $p\ge2$ in Lemma 8, which is false for $p=1$ ;
- the weighted ratio cost in Lemma 10, as its proof and its use in Lemma 11 require.
Not formalized. The polynomial-time content of "we can find" is not formalized; each such claim is an existence statement.

Contributions are welcome at every level:

proofs of the milestones;
a general strong-duality lemma for concurrent flow, reusable for the uniform, directed and short-path missions of this series;
a reusable region-growing decomposition lemma.

Selected references

T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
T. Leighton and S. Rao, An approximate max-flow min-cut theorem for uniform multicommodity flow problems with applications to approximation algorithms, FOCS 1988, 422–431. https://doi.org/10.1109/SFCS.1988.21958
N. Garg, V. V. Vazirani and M. Yannakakis, Approximate max-flow min-(multi)cut theorems and their applications, SIAM J. Comput. 25(2):235–251, 1996. https://doi.org/10.1137/S0097539793243016
N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
Y. Aumann and Y. Rabani, An O(log k) approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. 27(1):291–301, 1998. https://doi.org/10.1137/S0097539794285983
F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620

8 thms2 active usersReviewed

Complexity Theory Information Theory Probability·Captain: mikedeng1

A Pseudorandom Generator from Any One-Way Function: One-Way Functions Exist If and Only If Pseudorandom Generators ExistResearch Paper

Motivation

Cryptographic protocols use random looking strings that can be reproduced from a shorter private seed. A pseudorandom generator provides those strings if no efficient observer can tell them from uniformly sampled bits. A one-way function provides a different kind of asymmetry: anyone can evaluate it efficiently, but no efficient algorithm can usually recover a preimage of a random output. Håstad, Impagliazzo, Levin, and Luby proved that these two existence questions are equivalent. Their result identifies average-case inversion hardness as sufficient for computational pseudorandomness, without assuming a particular candidate function or algebraic problem (Håstad et al., 1999).

The equivalence is known mathematically; this mission asks for a machine-checked account of its qualitative security claim. The original article develops stronger quantitative time–success comparisons. Those comparisons are relevant to concrete cryptography, but the existence equivalence can be stated through asymptotically negligible success probabilities. This distinction is fixed throughout the formalization.

Setting

At security parameter $n$ , a function ensemble $F$ receives a string from the Boolean cube $\{0,1\}^{t_n}$ and returns one in $\{0,1\}^{\ell_n}$ . The lengths are polynomial-time parameters, and one uniform machine evaluates the family when given $1^n$ , separators, an optional unary integer advice value, and the input. The optional advice is polynomially bounded and may depend on $n$ without being computable. The goal itself uses no advice.

An adversary is a polynomial-time bit-string machine with polynomially many independent random coins. For inversion it sees $F_n(X)$ for a uniform input $X$ and may return any string $x'$ of the correct input length with $F_n(x')=F_n(X)$ . It need not recover the original $X$ . The ensemble is one-way if that success probability is negligible for every such adversary. For distinguishing, the adversary accepts only by outputting the one-bit string $[1]$ . Two laws are computationally indistinguishable if every adversary has negligible difference between its acceptance probabilities.

A generator $G$ is pseudorandom when $t_n<\ell_n$ for positive $n$ and its output law on a uniform $t_n$ -bit seed is computationally indistinguishable from the uniform law on $\ell_n$ bits. Strict stretch is essential: the identity map would otherwise satisfy the indistinguishability clause. All probabilities are finite counting fractions over Boolean cubes, so neither arbitrary measures nor a default value for an empty event space enters the definitions.

The intermediate results use Shannon entropy and order-two Rényi entropy, both in bits, and statistical distance, half the $L^1$ difference of finite laws. A universal hash family is pairwise independent in the exact sense of Definition 4.6: for distinct inputs $x,x'$ and any two prescribed outputs $a,a'$ , the chance over the uniform key that both outputs occur is exactly the reciprocal of the square of the output-space size. The public hash key is retained in the extracted output (Håstad et al., 1999, §§2–4).

Formalization targets

Main equivalence

The goal is Theorem 6.3, on printed page 1387:

(\exists F\;\mathrm{OWF}(F))\quad\Longleftrightarrow\quad (\exists G\;\mathrm{PRG}(G)).

Existence is the stable target: it does not fix a particular generator or an output-stretch constant. The reverse direction is the one the article attributes to Levin; the forward direction passes through the article's false-entropy and pseudoentropy constructions.

Intermediate targets

Lemma 4.8 bounds the statistical distance of a universal hash output with its public key by $2^{-(e+1)}$ when the source has Rényi entropy at least $m$ and the hash output has $m-2e$ bits. Theorem 4.14 converts a pseudoentropy generator into a PRG using the integer lengths and repetition count in Construction 4.13. Lemma 6.4 compares the Shannon entropies of the two Section 6 output laws:

H(\mathcal E)\ge H(\mathcal D)+10n^2,

with $k_n\ge125n^3$ . Theorem 6.2 gives the resulting mildly nonuniform false-entropy generator from a one-way function. The cited Levin direction is a separate existential milestone. These statements are the mission's milestone list, in their attack order (Håstad et al., 1999, pp. 1378–1387).

Significance

The result supplies a general route from any suitable average-case hard inversion task to a source of computational pseudorandom bits. It means an existence theorem for one primitive also settles the existence question for the other; it does not claim that an arbitrary one-bit-stretch generator is itself one-way. The paper's intermediate entropy notions record how much unpredictability remains or appears when outputs have nonuniform statistical laws.

A completed formalization would make the definitions of adversary, negligible advantage, universal hashing, entropy, and the finite output laws independently reusable. The known paper proof is not yet represented by the theorem stubs in this proposal. Formalizing the cited reverse implication, the entropy comparisons, and the links between the paper's intermediate generator notions remains solver work. No claim is made that the quantitative reduction bounds have been machine checked.

Difficulty

The one-way hypothesis only limits efficient inversion of an output; it does not directly say that the output is close to uniform. In particular, the output may carry statistical structure even when finding a preimage is hard. A direct attempt to hash the output without accounting for its varying preimage sizes does not produce the claimed pseudorandom law. The Section 6 construction therefore involves a random index, a hash prefix, independent parity masks, and a second public hash key. Their exact sample spaces matter for both the entropy gap and computational indistinguishability (Håstad et al., 1999, §§4, 6).

Formalization scope

Bit strings are Levin2003.Bits, fixed-length cubes are Levin2003.cube, and polynomial time is Mathlib's TM2 notion through the published Levin2003_owf_model. That module's own OneWay predicate requires length preservation, which Definition 3.2 of this paper does not; this mission defines its own ensemble and one-way predicate. Uniform adversaries receive no advice in the goal. Their coin budgets are polynomially bounded, and their inputs expose the security parameter in unary. Those choices rule out the vacuous encoding with unrestricted adversaries or an invisible security parameter.

The §6 laws use a finite product seed. The printed (6.8) samples index blocks as bit strings of length $\lceil\log n\rceil$ , but (6.3) defines $f'$ only for indices $0,\ldots,n-1$ and (6.5) averages uniformly over that range. The formalization uses Fin n indices. Thus Theorem 6.2 is stated for the repaired finite seed law, with a polynomial-time evaluator on its binary encoding. This exposes a gap between that seed space and Definition 3.9's uniform bit seed; bridging it is part of a complete proof. The prefix of a hash output is padded for the binary law, while the index remains present so the padding loses no information. The real-valued $m_n$ in (6.6) is rounded down to a bit length, and its integer value is the advice for Theorem 6.2. Construction 4.13 retains its printed floor and ceiling. Its pseudoentropy surplus $s_n$ may be real-valued, as in the paper; polynomial-time computability of $s_n$ is rendered as $s_n=p_n/q_n$ with natural numbers whose binary expansions are polynomial-time computable from $1^n$ .

Lemma 6.4 explicitly bounds approximate degeneracy by $n-1$ , which its printed proof uses without stating. For a one-way function that bound is needed only eventually. Accordingly computational-entropy lower bounds are formulated for all sufficiently large positive $n$ ; the paper's Definition 3.7 says all $n$ . Lemma 6.5's oracle-machine statement and its printed probability constant are left for a separate treatment. The model covers qualitative negligible success, not time–success ratios, expected-time bookkeeping, or labels such as weak-preserving. Contributions that close those quantitative gaps are welcome, as are proofs of the selected milestones and reusable finite-entropy lemmas.

Selected references

J. Håstad, R. Impagliazzo, L. A. Levin, and M. Luby, A Pseudorandom Generator from Any One-Way Function, SIAM Journal on Computing 28(4):1364–1396, 1999. DOI: 10.1137/S0097539793244708.

9 thms2 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: mikedeng1

A Theorem on Boolean Matrices: Warshall's Construction M* Equals the Boolean Sum M ∨ M² ∨ ⋯ ∨ Mᵈ of the Boolean Powers of MResearch Paper

Motivation

A finite directed graph on $d$ vertices is recorded by its adjacency matrix, a $d \times d$ array of zeros and ones. Many questions about the graph are questions about reachability: can vertex $j$ be reached from vertex $i$ by following one or more edges? In the late 1950s this question arose in the analysis of programs. Prosser (Applications of Boolean matrices to the analysis of flow diagrams, 1959) represented the flow diagram of a program by a boolean matrix and read off properties such as which blocks can follow which; Marimont (A new method of checking the consistency of precedence matrices, J. ACM 1959) used the same matrices to check precedence relations for consistency.

In both works the reachability matrix is described as a boolean sum of boolean powers of the adjacency matrix. Computed that way, it costs $d$ boolean matrix products, that is on the order of $d^3$ operations per product. Stephen Warshall's two-page note (A theorem on Boolean matrices, J. ACM 9 (1962) 11–12) proves that a much shorter procedure, $d$ passes of row updates performed in place, gives the same matrix. The same procedure was published in the same year by Floyd as Algorithm 96: Ancestor (Comm. ACM 5 (1962) 344), and its weighted version is Floyd's Algorithm 97: Shortest Path. The procedure is now taught as the Floyd–Warshall or Roy–Warshall algorithm.

Timeline. 1959: Prosser and Marimont describe reachability as a sum of boolean powers. 1959: Roy publishes the same closure construction in French (C. R. Acad. Sci. Paris 249). 1962: Warshall's note proves the in-place construction correct; Floyd's Algorithm 96 publishes it as code, and Algorithm 97 extends it to shortest paths.

Setting

Fix a natural number $d$ and let $M = (m_{ij})$ be a $d \times d$ matrix each of whose entries is $0$ or $1$ .

The boolean product of two such matrices $A$ and $B$ is the matrix $A \wedge B$ with $(A \wedge B)_{ij} = \bigvee_k (a_{ik} \wedge b_{kj})$ : the entry is $1$ when some index $k$ has $a_{ik} = b_{kj} = 1$ .
The boolean sum $A \vee B$ is the entrywise disjunction, $(A \vee B)_{ij} = a_{ij} \vee b_{ij}$ .
The boolean powers are $M^1 = M$ and $M^{p+1} = M^p \wedge M$ .
The introduction's matrix is the power sum

M' \;=\; \bigvee_{p=1}^{d} M^p .

The THEOREM defines $M'$ instead by chains: $m'_{ij} = 1$ if and only if either $m_{ij} = 1$ or there are indices $k_1, \dots, k_n$ with $m_{ik_1} = m_{k_1k_2} = \cdots = m_{k_nj} = 1$ . Footnote 2 states that the two definitions agree.
Warshall's construction $M^*$ : set $M^* = M$ ; for $i = 1, \dots, d$ in turn, for every row $j$ with $m^*_{ji} = 1$ and every column $k$ , set $m^*_{jk} = m^*_{jk} \vee m^*_{ik}$ . Entries are overwritten during a pass and later steps of the same pass read the new values.
Footnote 3 gives a recursive version: $(m_{ij})_0 = m_{ij}$ and $(m_{ij})_{n+1} = (m_{ij})_n \vee \bigl((m_{i,n+1})_n \wedge (m_{n+1,j})_n\bigr)$ , and asserts $m^*_{ij} = (m_{ij})_d$ .

In Lean the matrix is M : Fin d → Fin d → Bool. The power sum is powerSum M, the chain relation ChainRel M i j, the recursion warshallRec M n, all in the namespace WarshallBool.Closure. The construction $M^*$ is the published FloydAlgorithms.ShortestPath.algorithm96 M.

Formalization targets

Goal: the construction computes the power sum

M^* \;=\; \bigvee_{p=1}^{d} M^p \qquad \text{for every } d \text{ and every } d \times d \text{ 0-1 matrix } M .

This is the transformation the introduction asks for, combined with the THEOREM's assertion $M^* = M'$ and footnote 2. The goal has no hypothesis beyond the shape of $M$ .

Milestone 1 (Proved, referenced): the THEOREM

m^*_{ij} = 1 \iff m_{ij} = 1 \text{ or } m_{ik_1} = \cdots = m_{k_nj} = 1 \text{ for some } k_1, \dots, k_n .

It is already on the platform as FloydAlgorithms.ShortestPath.algorithm96_eq_transGen, stated with Mathlib's transitive closure Relation.TransGen, and it is not posed again.

Milestone 2: footnote 2

m_{ij} = 1 \text{ or a chain } i \to k_1 \to \cdots \to k_n \to j \text{ of 1 entries} \iff \Bigl(\bigvee_{p=1}^{d} M^p\Bigr)_{ij} = 1 .

Companion: footnote 3

M^* \;=\; \bigl((m_{ij})_d\bigr)_{i,j} .

This is not a milestone of the goal; it identifies the in-place construction with its stage-by-stage recursion.

Significance

The result. The theorem says that reachability in a directed graph on $d$ vertices, defined through matrix powers, can be computed by $d$ passes of in-place row operations, on the order of $d^2$ row updates instead of $d$ full boolean matrix products. The same scheme, with $(\min, +)$ in place of $(\vee, \wedge)$ , is the Floyd–Warshall shortest-path algorithm; with other semirings it computes regular expressions of finite automata (Kleene, McNaughton–Yamada) and path problems in general. Footnote 3's recursion is the form in which the algorithm is usually proved correct today, and its equivalence with the in-place version is what justifies running it without a second copy of the matrix.

Formalizing it. The chain form of the THEOREM is already machine-checked on Prove2Me (algorithm96_eq_transGen). What this mission adds is the statement in the paper's own terms: the introduction's power sum $\bigvee_{p=1}^d M^p$ , footnote 2's equivalence between powers and chains, which requires that chains can be shortened to length at most $d$ , and footnote 3's in-place versus recursive equivalence. None of these three is on the platform. The paper itself proves only the THEOREM; footnotes 2 and 3 are stated without proof.

Difficulty

Footnote 2 calls the equivalence "trivial", but one direction needs a pigeonhole argument: a chain $i \to k_1 \to \cdots \to k_n \to j$ of arbitrary length witnesses some power $M^{n+1}$ , and the power sum stops at $M^d$ . A chain with repeated indices has to be shortened, and the shortening must keep at least one step, since there is no reflexive part ( $m'_{ii} = 1$ only through a cycle). For a $d$ -cycle the diagonal entries appear only in $M^d$ , so the range $1..d$ is exact.

Footnote 3 compares two computations that read different data. The construction overwrites entries during a pass, and later steps of the same pass read the overwritten values; the recursion reads only the previous stage. The two agree only because of what a pass does and does not overwrite, and the published algorithm96 is three nested left folds over List.finRange, so the comparison has to be made against that concrete loop structure rather than an idealized simultaneous update.

Formalization scope

Matrices are Fin d → Fin d → Bool, with $1$ as true. Indices are $0, \dots, d-1$ instead of the page's $1, \dots, d$ ; the pivot of pass $i$ (1-based) is the 0-based index $i-1$ .
$d = 0$ is allowed; all statements are then trivially true, as on the page.
The boolean product boolProd A B i j is decide (∃ k, A i k = true ∧ B k j = true). Mathlib's matrix product on Matrix (Fin d) (Fin d) Bool is not the boolean product: Bool is a boolean ring there, its addition is exclusive or, and that product counts walks modulo 2. A formalization through * or ^ on Matrix _ _ Bool states a different, false theorem and is ruled out.
boolPow M p is the page's $M^p$ for $p \ge 1$ ; the base boolPow M 0 is the identity matrix, which is not on the page and does not enter the sum. powerSum M i j holds iff boolPow M p i j for some $p \in \{1, \dots, d\}$ . No reflexive closure is included anywhere.
ChainRel M i j is the existence of a list $[k_1, \dots, k_n]$ (possibly empty) making $i, k_1, \dots, k_n, j$ a List.IsChain of true entries.
warshallRec M n uses the 0-based pivot $n$ at stage $n+1$ and is constant after stage $d$ , which footnote 3 never uses.
$M^*$ is the published algorithm96, which fixes the inner loops over rows and columns in ascending order; Warshall leaves that order open, and it does not affect the result.
The goal must not be stated through TransGen, ChainRel or warshallRec, and powerSum is defined from boolPow, not from the closure or the algorithm.

Reusable beyond this mission: the boolean matrix product and powers, the power-sum characterization of the transitive closure of a relation on Fin d (footnote 2), and the in-place/recursive equivalence (footnote 3), which carries over to Floyd's Algorithm 97. Proofs of milestone 2 and of the companion are welcome independently of the goal.

Selected references

S. Warshall, A theorem on Boolean matrices, J. ACM 9(1) (1962) 11–12. https://doi.org/10.1145/321105.321107
R. W. Floyd, Algorithm 96: Ancestor, Comm. ACM 5(6) (1962) 344–345. https://doi.org/10.1145/367766.368166
R. W. Floyd, Algorithm 97: Shortest path, Comm. ACM 5(6) (1962) 345. https://doi.org/10.1145/367766.368168
R. T. Prosser, Applications of Boolean matrices to the analysis of flow diagrams, Proc. Eastern Joint Computer Conference (1959) 133–138. https://doi.org/10.1145/1460299.1460314
R. B. Marimont, A new method of checking the consistency of precedence matrices, J. ACM 6(2) (1959) 164–171. https://doi.org/10.1145/320964.320975
B. Roy, Transitivité et connexité, C. R. Acad. Sci. Paris 249 (1959) 216–218.

5 thms2 active usersReviewed

Completed

Formal Verification·Captain: mikedeng1

Reaching Agreement in the Presence of Faults 3: With Authenticated Messages, the S_pq Procedure Assures Interactive Consistency for m Faults for Every n ≥ mResearch Paper

Motivation

Processors in a distributed system may hold separate readings of a sensor, clock, or diagnostic result while some processors give misleading reports. The aim of interactive consistency is for every functioning processor to compute the same vector of reported values and to put each functioning processor's actual private value in its corresponding position. A shared vector can then be used for a common decision. Pease, Shostak, and Lamport formulated this problem for isolated processors communicating by two-party messages; their paper discusses clock synchronization, input stabilization, and diagnostic tests as concrete applications Pease–Shostak–Lamport 1980.

In the paper's oral-message model, faulty processors can invent reports about values they received from others. The other two missions in this series formalize the recursive majority procedure for $n\ge 3m+1$ and the matching impossibility result below that bound. Section 5 changes the communication assumption: a faulty processor may refuse to pass on a received value but cannot pass on an altered value as if it came from its original sender. Under that assumption, the authors give a procedure for every $n\ge m$ , including configurations outside the oral-message threshold Pease–Shostak–Lamport 1980, §§3–5.

Setting

Let $P$ be a finite set of $n$ processors and $V$ a type of private values. Each processor $q\in P$ has a value $\sigma(q)\in V$ . A scenario $\sigma$ records the values reported along chains of processors. A string $p_1p_2\cdots p_r$ is read from receiver to originator: $p_1$ receives a report ultimately attributed to $p_r$ . A recorded value may be NIL, meaning that no authenticated value is available. The view available to receiver $p$ is its $p$ -scenario, the restriction $w\mapsto\sigma(pw)$ ; it contains no report that begins with a different receiver.

Choose a set $N\subseteq P$ of nonfaulty processors. At most $m$ processors may be faulty, expressed as $|P|\le |N|+m$ . An authenticated scenario consistent with $N$ obeys two conditions whenever the displayed strings are in the $(m+1)$ -level scenario. If $p\in N$ and $q\in P$ , the report made by nonfaulty relay $p$ is truthful: $\sigma(qpw)=\sigma(pw)$ . For any prefix $w'$ , a chain passing through nonfaulty $p$ carries either the value at $p$ or NIL: $\sigma(w'pw)\in\{\sigma(pw),\mathrm{NIL}\}$ . The second condition allows omission by later relays while excluding a changed value falsely attributed to $p$ Pease–Shostak–Lamport 1980, p. 233.

For each receiver $p$ and originator $q$ , the procedure forms $S_{pq}$ , the set of all non-NIL values in $p$ 's view on strings $pwq$ . The intermediate string $w$ has at most $m$ distinct letters, all in $P\setminus\{p,q\}$ . Receiver $p$ records the sole value in $S_{pq}$ when this set is a singleton; otherwise it records NIL. The resulting entries, one for each $q\in P$ , form $p$ 's proposed consistency vector Pease–Shostak–Lamport 1980, p. 233.

Formalization targets

The first milestone covers a nonfaulty originator $q$ : every nonfaulty receiver $p$ sees exactly its true value. The second covers a faulty originator: the set of non-NIL values seen by one nonfaulty receiver is contained in the set seen by another. The same statement with the receivers exchanged gives equality of their sets.

The goal is the procedure's full interactive-consistency guarantee, for every choice of $N$ and every authenticated scenario satisfying the conditions above:

\begin{aligned} R_p(q)&=\sigma(q) &&(p,q\in N),\\ R_p(r)&=R_{p'}(r) &&(p,p'\in N,\ r\in P). \end{aligned}

Here $R_p(r)$ is the optional value recorded by processor $p$ for processor $r$ . Both clauses matter: agreement alone could be achieved by always recording NIL, while correct nonfaulty entries alone would leave faulty entries inconsistent.

Significance

The result identifies an exact communication assumption under which the paper's $3m+1$ oral-message bound no longer governs the procedure. Even if a faulty originator gives conflicting values, nonfaulty receivers finish with identical entries for that originator; if an originator is nonfaulty, they retain its actual value. The paper describes authenticators as a practical approximation to the assumption, but the guarantee here is a mathematical statement about scenarios satisfying its two conditions, not a probability claim about a cryptographic implementation Pease–Shostak–Lamport 1980, §5.

Formalizing this result supplies precise interfaces for authenticated scenario consistency, local views, the set $S_{pq}$ , and the recording rule. The paper proves the result on pp. 233–234; this mission asks for a machine-checked proof of those statements in Lean. The scenario and local-view definitions can support later formalizations of message-passing protocols with truthful or omissible relays. Contributions that establish the two source milestones and the final guarantee, or develop reusable list and finite-set facts needed by them, are within scope.

Difficulty

The case of a faulty originator is the central difficulty. Its private value has no required relationship to what different nonfaulty receivers hear, so simply asserting that every receiver obtains the same direct report is unjustified. A faulty relay may also omit a report, which makes equality of raw scenario entries too strong. The target must compare sets of non-NIL values obtained along admissible relay chains. At the longest allowed chain, the length bound prevents adding another relay, and the number of faulty processors is needed to establish that an admissible nonfaulty relay occurs in the chain Pease–Shostak–Lamport 1980, p. 234.

Formalization scope

Lean represents processors by a finite set P : Finset α, values by a type V, strings by List α, and NIL by none : Option V. A scenario is a total function from strings to optional values. Only strings over $P$ of length at most $m+2$ are constrained by authenticated consistency, matching the $(m+1)$ -level scenario that the procedure reads. A single-letter string has a non-NIL private value for every processor in $P$ . Conditions (i) and (ii) constrain nonfaulty relays only; condition (ii) allows either the original value or NIL for every prefix over $P$ , including an empty prefix.

The procedure is applied only to $p$ 's view $w\mapsto\sigma(pw)$ , so it has no access to the full scenario or to $N$ . Its intermediate strings are repetition-free, exclude both $p$ and $q$ , and have length at most $m$ . The set $S_{pq}$ contains values in $V$ , not NIL; an empty set and a set with multiple values both cause a NIL record. The formal theorem retains the printed $n\ge m$ condition, although it is not needed in the proof of the stated set relationships. It also covers $p=q$ , $m=0$ , and empty or singleton processor sets when their quantified conditions apply. These conventions rule out an always-NIL decision rule and the trivial rule that reads $\sigma(q)$ from outside the receiver's view.

The cryptographic maps $A_p$ , their message encodings, and the paper's assertion that practical authenticators can meet the assumption with arbitrarily high probability are outside scope. The formal result assumes the two exact authenticated-scenario conditions. A complete development needs finite-set cardinality and list facts, especially about distinct relay strings and bounded concatenation; these facts can be reused for other authenticated relay models.

Selected references

M. Pease, R. Shostak, and L. Lamport, Reaching Agreement in the Presence of Faults, Journal of the ACM 27(2), 1980, 228–234. DOI: 10.1145/322186.322188.

5 thms2 active usersReviewed

Completed

Formal Verification·Captain: mikedeng1

Reaching Agreement in the Presence of Faults 2: If |V| ≥ 2 and 3 ≤ n ≤ 3m, No Family {F_p} Assures Interactive Consistency for m Faults, However Many Rounds Are UsedResearch Paper

Motivation

A fault-tolerant system built from several processors must let its working processors act on the same data, even though some processors may have failed in ways nobody can predict: a failed processor may stop relaying information, relay something it invented, or tell different processors different things. Pease, Shostak and Lamport (J. ACM 27 (1980) 228–234) isolated the core question in the setting of the SIFT aircraft-control computer: each of $n$ processors holds a private value, at most $m$ processors are faulty, and processors communicate only by two-party messages. Can the nonfaulty processors each compute a vector of values, one entry per processor, such that all nonfaulty processors compute the same vector and the entry of each nonfaulty processor is its true private value? This requirement is called interactive consistency.

The paper answers with a sharp threshold. Interactive consistency can be achieved when $n\ge 3m+1$ (Section 3), and it cannot be achieved when $n\le 3m$ , however many rounds of message exchange are allowed (Section 4). With unforgeable signatures it can be achieved for every $n\ge m$ (Section 5). The impossibility half is the origin of the " $3m+1$ " bound that appears throughout Byzantine fault tolerance, popularised two years later as the Byzantine Generals Problem (Lamport, Shostak, Pease, ACM TOPLAS 4 (1982)). This mission is the impossibility theorem.

Timeline:

1980: Pease, Shostak and Lamport prove the threshold $n\ge 3m+1$ for interactive consistency with oral messages, including the impossibility for $n\le 3m$ stated in terms of scenarios.
1982: Lamport, Shostak and Pease restate the problem as the Byzantine Generals Problem, with the same bound.
1985–1986: Fischer, Lynch and Merritt give a short "hexagon" proof of the same bound for several agreement problems (Distributed Computing 1 (1986)).

Setting

Let $P$ be a finite set of $n$ processors and $V$ a set of values. Write $P^*$ for the set of strings over $P$ (the empty string included) and $P^+$ for the nonempty strings. A string $p_1p_2\cdots p_r$ is read as a chain of reports: $p_1$ was told by $p_2$ that $\dots$ $p_{r-1}$ was told by $p_r$ that $p_r$ 's private value is the recorded value.

A scenario is a map $\sigma: P^+\to V$ . The value $\sigma(p)$ is processor $p$ 's private value, and $\sigma(p_1\cdots p_r)$ is the value $p_1$ received for the chain $p_2\cdots p_r$ . For $p\in P$ , the $p$ -scenario $\sigma_p$ is the restriction of $\sigma$ to the strings beginning with $p$ : everything $p$ ever learns.

For a set $N\subseteq P$ of nonfaulty processors, $\sigma$ is consistent with $N$ if

\sigma(pqw)=\sigma(qw)\qquad\text{for all }q\in N,\ p\in P,\ w\in P^*,

that is, every nonfaulty processor reports truthfully what it knows or hears. Faulty processors are unconstrained.

A decision family assigns to each $p\in P$ a map $F_p$ that takes a $p$ -scenario and a processor $q$ and returns a value $F_p(\sigma_p,q)\in V$ : the entry $p$ computes for $q$ . The family assures interactive consistency for $m$ faults if for every $N\subseteq P$ with $|N|\ge n-m$ and every scenario $\sigma$ consistent with $N$ ,

$F_p(\sigma_p,q)=\sigma(q)$ for all $p,q\in N$ ;
$F_p(\sigma_p,r)=F_q(\sigma_q,r)$ for all $p,q\in N$ , $r\in P$ .

In the Lean development these are InteractiveConsistency.Impossibility.ConsistentWith P N σ and AssuresIC P m F, with restrict σ p the $p$ -scenario.

Formalization targets

Goal: the THEOREM of Section 4

If $|V|\ge 2$ and

3\le n\le 3m,

then no family $\{F_p\mid p\in P\}$ assures interactive consistency for $m$ faults. Since scenarios are defined on strings of every length, no bound on the number of rounds is assumed.

Milestones, in the order the proof of the paper uses them

If $3\le n\le 3m$ , then $P$ is the disjoint union of three nonempty sets $A$ , $B$ , $C$ , each with at most $m$ members (p. 232).
For such a partition and values $v,v'$ , the scenarios $\alpha,\beta,\sigma$ that the page defines by recursion on the length of strings are consistent with $A\cup C$ , $B\cup C$ and $A\cup B$ respectively (p. 233).
For the same scenarios, $\alpha(aw)=\sigma(aw)$ and $\beta(bw)=\sigma(bw)$ for all $a\in A$ , $b\in B$ , $w\in P^*$ (p. 233).

Significance

The theorem shows that the algorithm of Section 3 is optimal in its fault tolerance: with oral messages, $n\ge 3m+1$ processors are not only sufficient but necessary. Every later lower bound for Byzantine agreement, Byzantine broadcast and approximate agreement with unauthenticated messages rests on this bound or a variant of its argument, and it is the reason replicated state machines tolerating $m$ Byzantine faults use $3m+1$ replicas. It also explains why Section 5 needs authentication: the argument depends on faulty processors being able to relay fabricated values.

The result has been proved since 1980; what is open here is its formalization. Nothing on Prove2Me models message-passing agreement, and this mission states the theorem in the paper's own model: scenarios on unbounded strings and decision functions of a single $p$ -scenario. The mission produces a reusable vocabulary (scenarios, consistency, interactive consistency) and the explicit three-scenario construction.

Difficulty

The obvious attempt is to argue round by round about what a processor can know after $k$ rounds; with unboundedly many rounds this never terminates in a contradiction. The paper's argument instead needs three entire scenarios, each a legitimate behaviour for a different set of faulty processors, that two processors cannot tell apart from their own views. Writing these scenarios down so that consistency holds on every string while the indistinguishability survives on every string is the delicate part: the faulty set of each scenario must relay exactly the values that keep the other scenario's view intact, and one of the defining equations ( $\beta(paw)=\alpha(aw)$ ) looks like a misprint but is what the argument requires. The counting step is elementary but carries the hypothesis $n\ge 3$ that the printed theorem leaves implicit.

Formalization scope

Processors are a Finset P in a type with decidable equality; strings are lists read left to right ( $p_1$ is the head of the list); a scenario is a total function List α → V whose values on the empty list and on lists with a letter outside $P$ carry no meaning: every condition quantifies only over strings whose letters lie in $P$ . Decision functions have type α → (List α → V) → α → V and are applied only to the $p$ -scenario fun w => σ (p :: w), never to $\sigma$ ; giving $F_p$ the whole scenario would make the problem trivial (output $\sigma(q)$ ). Consistency with $N$ constrains only relays by members of $N$ , and includes the empty $w$ . The quorum $|N|\ge n-m$ is written $|P|\le |N|+m$ , which avoids truncated subtraction on $\mathbb N$ . $|V|\ge 2$ is the existence of two distinct values.

Explicit readings of the page:

The printed hypothesis " $n\ge 3m$ " is a misprint for $n\le 3m$ (the proof opens "Since $n\le 3m$ ", and the section title is "Proof of Impossibility for $n<3m+1$ "); with $n\ge 3m$ the statement is false.
The hypothesis $n\ge 3$ is implicit in the proof's "three nonempty sets". It is necessary: for $n\le 2$ the family $F_p(\sigma_p,q)=\sigma(pq)$ assures interactive consistency.
In the construction, each letter $a$ , $b$ , $c$ ranges independently over $A$ , $B$ , $C$ (so " $\alpha(cc)$ " covers $\alpha(c'c)$ ); the value $\sigma(c'cw)$ , which the page leaves unspecified, is fixed to $\sigma(cw)$ .
The construction is stated as a definition, and the two "easy" claims about it (consistency, indistinguishability) are separate milestones.

A complete development needs only finite sets and lists from Mathlib. The vocabulary of p. 232 is shared with the other two missions of this series, Reaching Agreement in the Presence of Faults 1 (the algorithm for $n\ge 3m+1$ ) and 3 (authenticated messages, $n\ge m$ ), each of which defines it in its own namespace. Proofs of the milestones and of the goal are welcome, as is a proof of the goal by a different route.

Selected references

M. Pease, R. Shostak, L. Lamport, Reaching agreement in the presence of faults, Journal of the ACM 27(2) (1980) 228–234. https://doi.org/10.1145/322186.322188
L. Lamport, R. Shostak, M. Pease, The Byzantine Generals Problem, ACM Transactions on Programming Languages and Systems 4(3) (1982) 382–401. https://doi.org/10.1145/357172.357176
M. J. Fischer, N. A. Lynch, M. Merritt, Easy impossibility proofs for distributed consensus problems, Distributed Computing 1 (1986) 26–39. https://doi.org/10.1007/BF01843568

6 thms2 active usersReviewed

Completed

Formal Verification·Captain: mikedeng1

Reaching Agreement in the Presence of Faults 1: With n ≥ 3m + 1 Processors, the Recursive Majority Procedure on (m + 1)-Level Scenarios Assures Interactive Consistency for m FaultsResearch Paper

Motivation

A fault-tolerant system often replicates a computation on several processors and needs the nonfaulty ones to act on the same data, even though some processors may fail in arbitrary ways: send wrong values, send different values to different recipients, or lie about what they were told. Pease, Shostak and Lamport posed the question in 1980, motivated by the SIFT fault-tolerant aircraft-control computer under development at SRI (Wensley et al. 1978), where it arises in clock synchronization among other places: $n$ processors, at most $m$ of them faulty, communicate by two-party messages whose sender is always identifiable, and each holds a private value. Can the nonfaulty processors all compute the same vector of values, one entry per processor, whose entry for every nonfaulty processor is that processor's true value? The paper (J. ACM 27 (1980) 228–234) calls this interactive consistency and settles it: possible if and only if $n \ge 3m+1$ when messages can be forged in relay, and possible for every $n \ge m$ when they cannot. The same problem, under the name Byzantine generals, became the standard model of arbitrary ("Byzantine") failures in distributed computing (Lamport, Shostak & Pease 1982); the $3m+1$ bound underlies the quorum sizes of later replication protocols.

This mission covers the positive half of the paper's characterization: Section 3's recursive procedure, which achieves interactive consistency with $n\ge 3m+1$ processors in $m+1$ rounds of message exchange.

Setting

Let $P$ be a finite set of $n = |P|$ processors and $V$ a set of values. A string over a set $S$ is a finite sequence $p_1p_2\cdots p_r$ of elements of $S$ , repetitions allowed. For $k\ge 1$ a $k$ -level scenario is a map $\sigma$ from the nonempty strings over $P$ of length at most $k+1$ to $V$ . The value $\sigma(p)$ is $p$ 's private value $V_p$ ; for $r\ge 2$ , $\sigma(p_1p_2\cdots p_r)$ is the value $p_2$ tells $p_1$ that $p_3$ told $p_2$ … that $p_r$ told $p_{r-1}$ is $p_r$ 's private value. A $k$ -level scenario records the outcome of $k$ rounds of message exchange.

Faults are modeled by a set $N\subseteq P$ of nonfaulty processors, unknown to the processors. Nonfaulty processors relay truthfully, so $\sigma$ is consistent with $N$ when

\sigma(pqw) = \sigma(qw)\qquad (q\in N,\ p\in P,\ w \text{ a string over } P,\ |pqw|\le k+1).

Faulty processors are otherwise unconstrained. A processor $p$ sees only its view $\sigma_p$ , the restriction of $\sigma$ to strings beginning with $p$ .

The procedure (p. 230). Processor $p$ computes the entry for processor $q$ as follows, with $n$ and $m$ the current processor count and fault bound:

If some $Q\subseteq P$ with $|Q|>(n+m)/2$ and some $v$ satisfy $\sigma_p(pwq)=v$ for every string $w$ over $Q$ of length $\le m$ , record $v$ .
Otherwise apply the procedure for $m-1$ , $n-1$ to the processor set $P-\{q\}$ and the view $\hat\sigma_p(pw)=\sigma_p(pwq)$ , obtaining a vector of $n-1$ entries. If at least $\lfloor (n+m)/2\rfloor$ of them agree, record the common value; otherwise record NIL.

In Lean this is InteractiveConsistency.OralAlgorithm.record m P τ q with τ = fun w => σ (p :: w), values in Option V with none for NIL.

Formalization targets

Goal: the procedure assures interactive consistency

For $n\ge 3m+1$ , for every $N\subseteq P$ with $|N|\ge n-m$ and every $(m+1)$ -level scenario $\sigma$ consistent with $N$ ,

\mathrm{record}(m,P,\sigma_p,q)=\sigma(q)\quad(p,q\in N),\qquad \mathrm{record}(m,P,\sigma_p,r)=\mathrm{record}(m,P,\sigma_{p'},r)\quad(p,p'\in N,\ r\in P).

This is procedure_assures_ic. It is the paper's claim about this procedure, not an existence statement.

Milestones, in the order the paper's proof uses them

Nonfaulty $q$ (p. 231): for $p,q\in N$ , step (1) succeeds and $p$ records $V_q$ .
Two step-(1) quorums agree (p. 231): if $p,p'\in N$ find quorums $Q_1,Q_2$ with values $v,v'$ , then $v=v'$ .
The subscenario (p. 230): for faulty $q$ , $\hat\sigma(w)=\sigma(wq)$ is an $m$ -level scenario on $P-\{q\}$ consistent with $N$ , and $|N|\ge (n-1)-(m-1)$ .
The $\hat Q$ claim (p. 231): if $Q,v$ satisfy step (1) for $p'$ and $q$ , then $\hat Q=Q-\{q\}$ has at least $\lfloor(n+m)/2\rfloor$ members and $\hat Q, v$ satisfy step (1) of the recursive call for every $q'\in\hat Q$ .

Significance

The theorem is the upper bound in the tight characterization $n\ge 3m+1$ of when interactive consistency is achievable with unauthenticated messages; the matching impossibility (the paper's Section 4 THEOREM) shows that no procedure, with any number of rounds, does better. The procedure is the ancestor of the "oral messages" algorithm $\mathrm{OM}(m)$ of the Byzantine generals paper, and its quorum arithmetic ( $|Q|>(n+m)/2$ , intersections of two quorums containing a nonfaulty member) recurs throughout Byzantine fault-tolerant replication.

The result is proved in the paper, in a half-page induction. What this mission adds is a machine-checked proof against an explicit model of scenarios, views and consistency with a bounded number of rounds. Machine-checked proofs exist for the related $\mathrm{OM}(m)$ algorithm of the later Byzantine generals paper in other proof systems; this procedure, with its quorum-based step (1), has to our knowledge not been formalized in Lean, and nothing on message-passing agreement exists on this platform.

Difficulty

Each step of the paper's proof is short, but the bookkeeping is where an argument breaks. The recursion changes three things at once: the processor set loses $q$ , the fault bound drops by one, and the scenario becomes $\hat\sigma(w)=\sigma(wq)$ of one level less. The induction hypothesis must therefore be stated for every finite processor set and every scenario, and applied to a subscenario whose consistency is inherited only for strings of the right length. The mixed case, where one nonfaulty processor exits at step (1) and another recurses, is the delicate one: the two processors' computations take different branches, and since $q$ is faulty nothing forces either value to be $q$ 's private value. The thresholds are exact: $|Q|>(n+m)/2$ in step (1) and $\lfloor(n+m)/2\rfloor$ agreeing entries in step (2), both in the current $n$ and $m$ ; off-by-one changes in either break the case analysis. Finally, step (2)'s majority value must be shown unique, so that two processors with the same vector record the same value.

Formalization scope

Processors form a Finset α with decidable equality; strings are List α, read left to right (the receiver first, the originator last), so $\sigma_p(pwq)$ is σ (p :: (w ++ [q])). A scenario is a total function List α → V; consistency with $N$ (ConsistentUpTo P N (m + 1) σ) constrains it only on strings over $P$ of length at most $m+2$ , the domain of an $(m+1)$ -level scenario and all the procedure reads. The procedure receives only the view fun w => σ (p :: w), never $\sigma$ or $N$ . The fault hypothesis $|N|\ge n-m$ is P.card ≤ N.card + m; $m=0$ is included.

Explicit readings of the paper's prose: "size $>(n+m)/2$ " is P.card + m < 2 * Q.card; $\lfloor(n+m)/2\rfloor$ is natural-number division; "strings over $Q$ of length $\le m$ " includes the empty string and allows repetitions; the step-(2) vector is indexed by P.erase q and includes $p$ 's own entry; the recorded value in step (1) is $\sigma_p(pq)$ (the empty string forces it); when several values reach the step-(2) threshold one is chosen deterministically from the vector (under the goal's hypotheses at most one does); for $m=0$ a failing step (1) records NIL (never reached under the hypotheses). Two printed slips are corrected in the Lean: "records $V_q$ and $q$ " (for "for $q$ ") and " $\sigma_{p'}(p'wq')$ " (for $\hat\sigma_{p'}$ ).

Trivializing formalizations are ruled out: the procedure never sees $\sigma$ itself (with it, recording $\sigma(q)$ would be trivial), consistency constrains only relays by nonfaulty processors, and $N$ ranges over every subset of size at least $n-m$ .

The development needs only finite sets and lists; no library beyond Mathlib is required. The quorum-intersection lemmas and the subscenario construction are reusable for other oral-message protocols. Contributions welcome: proofs of the four milestones, the goal by induction on $m$ , and a computable version of the procedure for concrete instances. This is mission 1 of a series of three on this paper; mission 2 formalizes the impossibility THEOREM for $n\le 3m$ (Section 4), and mission 3 the authenticated-message procedure for every $n\ge m$ (Section 5).

Selected references

M. Pease, R. Shostak, L. Lamport, Reaching agreement in the presence of faults, Journal of the ACM 27(2), 1980, 228–234. https://doi.org/10.1145/322186.322188
L. Lamport, R. Shostak, M. Pease, The Byzantine generals problem, ACM Transactions on Programming Languages and Systems 4(3), 1982, 382–401. https://doi.org/10.1145/357172.357176
J. H. Wensley et al., SIFT: Design and analysis of a fault-tolerant computer for aircraft control, Proceedings of the IEEE 66(10), 1978, 1240–1255. https://doi.org/10.1109/PROC.1978.11114

7 thms2 active usersReviewed

Completed

Combinatorics Number Theory Probability·Captain: mikedeng1

A New Class of Random Number Generators 1: For Prime m = bʳ + bˢ − 1, Every Nontrivial Add-with-Carry Sequence Is Periodic After r Steps, with Period the Order of b mod mResearch Paper

Why add-with-carry generators

Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep $r$ machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as $2^{640}$ when the base $b$ is near $2^{32}$ (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base- $b$ digits of a fraction $k/m$ written backwards, so the period of the generator is the period of a repeating base- $b$ expansion, i.e. the multiplicative order of $b$ modulo $m$ .

Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus $m$ (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.

Setting

Fix a base $b \ge 2$ and two lags $r$ and $s$ with $0 < s < r$ . A state (or seed vector) is

x = (x_1, x_2, \dots, x_r, c),

where each $x_i \in \{0, 1, \dots, b-1\}$ is a base- $b$ digit and $c \in \{0, 1\}$ is the carry bit. The digit $x_1$ is the oldest one. The add-with-carry map $f$ (p. 465) is

f(x_1, \dots, x_r, c) = \begin{cases} (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c,\ 0) & \text{if } x_{r+1-s} + x_1 + c < b,\\ (x_2, \dots, x_r,\ x_{r+1-s} + x_1 + c - b,\ 1) & \text{if } x_{r+1-s} + x_1 + c \ge b, \end{cases}

and the generated sequence of a seed $x$ is $x, f(x), f^2(x), \dots$ . Reading off the last digit of each state gives a digit stream $x_1, \dots, x_r, x_{r+1}, x_{r+2}, \dots$ obeying $x_n = x_{n-r} + x_{n-s} + c \bmod b$ , with the carry updated at each step. The two trivial seeds are $(0, \dots, 0, 0)$ and $(b-1, \dots, b-1, 1)$ . The modulus of the generator is

m = b^r + b^s - 1 .

For $0 \le k < m$ and $j \ge 1$ , the $j$ -th base- $b$ digit of $k/m$ after the point is $d_j(k/m) = \lfloor b \cdot (b^{j-1} k \bmod m) / m \rfloor$ . The order $\operatorname{ord}_m(b)$ is the least $p \ge 1$ with $b^p \equiv 1 \pmod m$ , and $b$ is a primitive root of a prime $m$ when $\operatorname{ord}_m(b) = m - 1$ .

Formalization targets

Goal: the period is the order of $b$

Let $m = b^r + b^s - 1$ be prime, and let $x$ be any seed other than the two trivial seeds. Then $f^r(x)$ is a periodic point of $f$ and

\min\{p \ge 1 : f^{p}(f^{r}(x)) = f^{r}(x)\} = \operatorname{ord}_m(b).

This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base $b$ for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular $b$ , $r$ , $s$ and does not assume that $b$ is a primitive root. When it is, the period is $b^r + b^s - 2$ , the value announced in §2.

Milestones

§4.1 (p. 467): for $\gcd(k, m) = \gcd(b, m) = 1$ , $p > 0$ is a period of the base- $b$ expansion of $k/m$ iff $\operatorname{ord}_m(b) \mid p$ .
§4.1 (p. 467): if $b$ is a primitive root of the prime $m$ , every proper fraction $k/m$ has least period $m - 1$ .
p. 472: $f(x) = x$ iff $x$ is a trivial seed.
p. 472: $f^r(x)$ is periodic for every seed.
§4.2 (p. 468): for every seed other than $(b-1, \dots, b-1, 1)$ and every $C$ , there is $0 \le k < m$ , positive iff the seed is nonzero, with

x_n = d_{C+1-n}(k/m) \qquad (r + 1 \le n \le C).

p. 472, Method 3: $x$ is periodic iff $c = 0$ and $x_r \cdots x_{s+1} \ge x_{r-s} \cdots x_1$ , or $c = 1$ and $x_r \cdots x_{s+1} \le x_{r-s} \cdots x_1$ (digit strings read as base- $b$ integers).
§2 (p. 465): the instance $b = 10$ , $r = 2$ , $s = 1$ , period $108$ .
§7 (p. 477): the instance $b = 6$ , $r = 21$ , $s = 2$ , period $6^{21} + 6^2 - 2$ .

Significance

The result. The goal reduces the period of the generator, a property of a dynamical system on $2b^r$ states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses $b, r, s$ : search for primes $m = b^r + b^s - 1$ and check the order of $b$ . Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus $m$ . Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.

Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base- $b$ expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.

Difficulty

The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: $f$ is not linear over $\mathbb{Z}/b$ , and the state $(x_1, \dots, x_r, c)$ does not live in a group in any evident way. The link to the order of $b$ modulo $m$ goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed $(b-1, \dots, b-1, 1)$ , whose digits are those of $m/m = 1$ , has to be excluded.

A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by $r$ (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.

Formalization scope

Representation. All declarations are in namespace CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of $0 < s$ and $s < r$ . A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so $c \le 1$ holds by typing. Lean index $i$ is the paper's $x_{i+1}$ : x 0 is $x_1$ (the digit the step drops), and the partner digit $x_{r+1-s}$ is index $r - s$ . step is defined directly from the two-case formula of p. 465, not through $k/m$ . The digit stream out is one-based: the seed digits for $n \le r$ , then the last digit of $f^{\,n-r}(x)$ . digit b m k j is the exact integer formula above, used for $j \ge 1$ only.
Period. "The period" is Mathlib's Function.minimalPeriod. It is $0$ at non-periodic points, so the goal's equation with the positive $\operatorname{ord}_m(b)$ also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period $L$ " is stated as " $p > 0$ is a period iff $L \mid p$ ".
Quantifier readings. "With appropriately chosen base $b$ , lags $r$ and $s$ and seed vector $x$ " (p. 465) is read as: $m$ prime and $x$ not a trivial seed, following p. 468 ("Making $m$ a prime ensures this") and p. 472. "After a few iterations" is "after at most $r$ ", the paper's own bound (p. 472), so the goal is stated at $f^r(x)$ . In milestone 5 the fraction $k$ depends on the length $C$ of the finite string, as in the paper's "arbitrarily long finite string". In milestone 8, "for any set of 21 seed digits" is stated at $f^{21}(x)$ for the same reason.
Corrected misprints. p. 465 prints the second trivial seed as "(9, 9, 9)"; the last entry is the carry, so milestone 7 excludes $(9, 9, 1)$ . p. 473, example (a), prints the Method 3 inequalities reversed; milestone 6 follows p. 472, which exhaustive checks on small parameters confirm. p. 478 repeats the die period with "− 1" for "− 2"; milestone 8 quotes p. 477.
Ruled-out trivializations. The goal is not "some period divides $m - 1$ " and not "every orbit is eventually periodic". Both hold for any self-map of a finite set or are vacuous. The trivial seeds are named states, not excluded by an assumption such as $f(x) \neq x$ .
Infrastructure and contributions. Needed: periods of base- $b$ expansions of rationals (milestones 1–2, reusable beyond this mission) and finite-dynamics facts about minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.

Selected references

G. Marsaglia and A. Zaman, A new class of random number generators, Ann. Appl. Probab. 1(3) (1991), 462–480. https://doi.org/10.1214/aoap/1177005878
S. Tezuka, P. L'Ecuyer and R. Couture, On the lattice structure of the add-with-carry and subtract-with-borrow random number generators, ACM Trans. Model. Comput. Simul. 3(4) (1993), 315–331. https://doi.org/10.1145/159737.159749
R. Couture and P. L'Ecuyer, Distribution properties of multiply-with-carry random number generators, Math. Comp. 66 (1997), 591–607. https://doi.org/10.1090/S0025-5718-97-00827-2
M. Lüscher, A portable high-quality random number generator for lattice field theory simulations, Comput. Phys. Commun. 79 (1994), 100–110. https://doi.org/10.1016/0010-4655(94)90232-1

17 thms2 active usersReviewed

Completed

Machine Learning Operations Research Probability·Captain: mikedeng1

The Weighted Majority Algorithm 6: Under the Weak Independence Condition, the Randomized Master WMR Has E(m) ≤ E(ln(w_init/w_fin))/(1−β)Research Paper

Motivation

Prediction with expert advice asks a learner to predict a binary label in each of a sequence of trials, having seen the predictions of a pool of $n$ prediction algorithms (the experts), and to make not many more mistakes than the best of them, with no probabilistic assumption on how the instances and labels are generated. Littlestone and Warmuth's Weighted Majority Algorithm (Littlestone, Warmuth 1994) maintains a weight for each pool member, predicts by a weighted vote, and shrinks the weights of members that err. Its mistake bounds are the origin of the multiplicative-weights method used throughout online learning, game theory and optimization (Arora, Hazan, Kale 2012).

A deterministic master with binary predictions can be forced to err in every trial in which the weight is split evenly, which costs it a factor of about two against the best expert. Section 6 of the paper introduces a randomized master, WMR, which predicts $1$ with probability equal to the weighted average prediction of the pool. Theorem 6.1 bounds its expected number of mistakes under a precisely stated condition on how its randomization interacts with the choice of instances and labels.

Timeline:

1989: Littlestone and Warmuth's technical report and FOCS paper introduce the Weighted Majority Algorithm and its randomized variant.
1991: Maass independently analyses the case $\beta = 0$ with binary pool predictions and a lazy update ([Maa91], cited in the paper).
1994: the journal version states the weak independence condition and proves Theorem 6.1 (p. 240).
1997: Freund and Schapire's Hedge algorithm recasts the randomized master as a distribution over experts in a decision-theoretic setting (Freund, Schapire 1997).

Setting

A pool of $n$ algorithms is run for $t$ trials on a probability space $(\Omega, \mathcal F, P)$ . In trial $j$ the pool member $i$ predicts $x_i^{(j)} \in [0,1]$ , the label is $\rho^{(j)} \in \{0,1\}$ , and the master predicts $\lambda^{(j)} \in \{0,1\}$ . All of these are random variables; deterministic sequences are a special case. Write $x^{(j)} = (x_1^{(j)}, \dots, x_n^{(j)})$ .

Each member carries a weight. The initial weights $w_i^{(1)}$ are positive, and the update step (5.1) multiplies the weight of member $i$ in trial $j$ by a factor $F$ that depends on $\beta$ , $x_i^{(j)}$ and $\rho^{(j)}$ :

w_i^{(j+1)} = F\,w_i^{(j)}, \qquad \beta^{|x_i^{(j)}-\rho^{(j)}|} \le F \le 1-(1-\beta)\,|x_i^{(j)}-\rho^{(j)}|,

where $0 \le \beta < 1$ and $0^0 = 1$ . WMR updates in every trial. Let $s^{(j)} = \sum_i w_i^{(j)}$ , so $s^{(1)} = w_{\mathrm{init}}$ and $s^{(t+1)} = w_{\mathrm{fin}}$ , and let

\gamma^{(j)} = \frac{\sum_{i=1}^n w_i^{(j)} x_i^{(j)}}{s^{(j)}}

be the weighted average prediction. WMR predicts $1$ with probability $\gamma^{(j)}$ . Its number of mistakes is $m = \sum_{j=1}^t |\lambda^{(j)} - \rho^{(j)}|$ .

The weak independence condition (p. 238) requires, for $j = 1, \dots, t$ ,

\mathbf E\big(\lambda^{(j)} \,\big|\, (x^{(1)},\rho^{(1)}), \dots, (x^{(j)},\rho^{(j)})\big) = \gamma^{(j)} \quad \text{almost surely}.

The conditioning includes the current predictions of the pool and the current label. It allows instances and labels to depend on the master's past predictions, and it holds, for instance, when WMR draws one uniform number $r \in [0,1]$ and predicts $1$ whenever $\gamma^{(j)} \ge r$ , provided the instances and labels are generated independently of $r$ .

Formalization targets

Goal: Theorem 6.1

Under the weak independence condition, and with $w_{\mathrm{fin}} > 0$ almost surely,

\mathbf E(m) \le \frac{\mathbf E\big(\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})\big)}{1-\beta}.

The statement fixes neither the pool, nor the update factors within (5.1), nor the distribution of instances and labels.

Milestone: expected mistakes equal expected loss of the weighted average

The step of the proof on p. 240: under the weak independence condition, $\mathbf E(|\lambda^{(j)}-\rho^{(j)}| \mid \mathcal F_j) = |\gamma^{(j)}-\rho^{(j)}|$ almost surely, and hence

\mathbf E(m) = \mathbf E\Big(\sum_{j=1}^t |\gamma^{(j)}-\rho^{(j)}|\Big).

Significance

Theorem 6.1 gives the randomized master the same bound that Theorem 5.2 gives the deterministic master WMC, whose predictions are allowed to lie in $[0,1]$ . With equal initial weights, $\ln(w_{\mathrm{init}}/w_{\mathrm{fin}}) \le \ln n + m_i \ln(1/\beta)$ for every pool member $i$ with total loss $m_i$ , and the bound yields Corollary 6.1 (p. 241): $\mathbf E(m) \le (\ln n + \mathbf E(m_i)\ln(1/\beta))/(1-\beta)$ . For $\beta$ close to $1$ this is better by nearly a factor of two than the bound for the deterministic binary master WMG. The weak independence condition is also what makes the bound valid against labels that adapt to the master's past predictions, which is the setting of later regret analyses.

The result is proved in the paper; this mission produces a machine-checked version. The platform has proofs of the randomized weighted majority bound in the form of Hazan's Lemma 1.4 and of Mohri et al.'s Theorem 8.4, but both state an expectation over the algorithm's internal distribution with deterministic data, unit weights and one fixed update rule. Neither covers random instances and labels, the conditional-expectation condition, or the whole class of updates (5.1).

Difficulty

The pathwise part of the argument is the loss bound for the weighted average (Lemma 5.3, posed in the companion mission on WMC). The new difficulty is probabilistic. The predictions, labels and weights are random and may depend on each other across trials, so the mistake indicator $|\lambda^{(j)}-\rho^{(j)}|$ cannot be replaced by $|\gamma^{(j)}-\rho^{(j)}|$ pointwise. The replacement holds only after conditioning on the $\sigma$ -algebra $\mathcal F_j$ , and requires that $\rho^{(j)}$ is $\mathcal F_j$ -measurable and binary, so that the indicator is affine in $\lambda^{(j)}$ . A reading that conditions on less (dropping the current label) or uses unconditional expectations does not support this step when the label depends on earlier randomness.

A second difficulty is that $\mathbf E(\ln(w_{\mathrm{init}}/w_{\mathrm{fin}}))$ may be infinite: the weights can become arbitrarily small with positive probability.

Formalization scope

The pool is Fin n; trials are indexed from $0$ to $t-1$ , so totalWeight … 0 is $w_{\mathrm{init}}$ and totalWeight … t is $w_{\mathrm{fin}}$ . The probability space is a measure P with IsProbabilityMeasure P. Predictions, labels and master predictions are real-valued measurable random variables; pool predictions lie in $[0,1]$ and labels and master predictions in $\{0,1\}$ on every sample path. Initial weights are deterministic and positive. The update factor of member $i$ in trial $j$ is a measurable function $F_{j,i}(x, r)$ of the member's prediction and the label, satisfying (5.1) on every sample path; the weights are computed from it, so they are random variables determined by the predictions and labels. $\mathcal F_j$ is the supremum of the $\sigma$ -algebras generated by the pairs $(x^{(k)}, \rho^{(k)})$ , $k \le j$ , and the weak independence condition is stated with Mathlib's conditional expectation P[λ j | 𝓕 j].

Expectations in the goal are lower Lebesgue integrals in $[0,\infty]$ , so the right-hand side may be $+\infty$ and no integrability of the logarithm is assumed. The hypothesis $w_{\mathrm{fin}} > 0$ almost surely excludes the case where the paper's bound is infinite and Lean's $\ln 0 = 0$ would make the literal statement false. A formalization that replaces the conditional expectation by the unconditional one, takes the logarithm's Bochner integral (which is $0$ when the logarithm is not integrable), or restricts to deterministic instances and labels does not state Theorem 6.1.

A complete development needs the pathwise loss bound of Lemma 5.3 for this weight model, the pull-out property of conditional expectations for bounded measurable factors, and the exchange of expectation and finite sums. The weight model and the filtration are reusable for Theorem 6.3 and for the lazy variant of the Appendix. Proofs of the milestone and of the goal are welcome, as are formalizations of Corollary 6.1.

Selected references

N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
Y. Freund, R. E. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, Journal of Computer and System Sciences 55(1), 119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8, 121–164, 2012. https://doi.org/10.4086/toc.2012.v008a006
N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

3 thms2 active usersReviewed

Completed

Machine Learning Operations Research·Captain: mikedeng1

The Weighted Majority Algorithm 3: On a Countably Infinite Pool, WMI2 Makes at Most inf_i (log(Ŵ(1)/W(i)) + m_i log(1/β) + log 2)/log(1/u) MistakesResearch Paper

Motivation

In prediction with expert advice, a master algorithm predicts a binary label in each of a sequence of trials, after seeing the predictions of a pool of other algorithms (the "experts"), and is charged one mistake whenever its prediction differs from the label. No probabilistic assumption is made on the sequence: the goal is a bound on the master's mistakes, valid for every sequence, in terms of the mistakes of the best pool member. The Weighted Majority Algorithm of Littlestone and Warmuth (Inform. and Comput. 108, 1994) achieves this for a finite pool of $n$ members with $O(\log n + m_i)$ mistakes, where $m_i$ is the number of mistakes of member $i$ .

Many natural pools are infinite: all programs in an enumeration, all hypotheses of a countable class, all values of a discretised parameter. Section 4 of the paper asks whether a master can compete with every member of a countably infinite pool $A_1, A_2, \dots$ , making at most $c(\log i + m_i)$ mistakes for every $i$ , while keeping only finitely many weights at any time. Running the Weighted Majority Algorithm on infinitely many weights would give such a bound, but cannot be implemented.

Timeline. Barzdin and Freivalds (1972, 1974) studied prediction of a sequence by an enumerable family of functions and gave an essentially optimal bound for the case of a pool containing a member consistent with the whole sequence ( $\beta = 0$ below). Littlestone and Warmuth's earlier versions of the paper (1989) introduced an algorithm WMI for infinite pools; the journal version (1994) replaced it by $\mathrm{WMI}_2$ , which matches the Barzdin–Freivalds bound when $\beta = 0$ and a consistent member exists, and extends it to pools in which every member may err.

Setting

Fix a parameter $\beta$ with $0 \le \beta < 1$ and put $u = (1+\beta)/2$ . Fix two real functions $W$ and $\hat W$ on the positive integers with

W(i) > 0, \qquad \sum_{i} W(i) < \infty, \qquad \hat W(i) \ge \sum_{j \ge i} W(j), \qquad \lim_{i \to \infty} \hat W(i) = 0 .

$W(i)$ is the initial weight of the pool member $A_i$ , and $\hat W(i)$ bounds the weight of the tail $A_i, A_{i+1}, \dots$ .

A sequence of $T$ trials gives, for each trial $t$ , the prediction $x_t(i) \in \{0,1\}$ of every pool member and a label $\rho_t \in \{0,1\}$ . Member $A_i$ makes at most $m_i$ mistakes: $x_t(i) \ne \rho_t$ for at most $m_i$ trials $t$ .

The master $\mathrm{WMI}_2$ keeps an active pool $A_1, \dots, A_l$ and a weight for each active member. With $m$ the number of its own mistakes so far, let

\theta(m) = \frac{u^{m+1}\,\hat W(1)}{(1-\beta)(m+1)(m+2)} .

Initially, and after each trial in which it errs, $\mathrm{WMI}_2$ raises $l$ (starting from $l = 0$ ) to the least value with $\hat W(l+1) \le \theta(m)$ ; a newly activated $A_i$ gets weight $W(i)$ . In a trial it computes the active weight $q_0$ predicting $0$ and $q_1$ predicting $1$ ; it predicts $0$ if $q_0 > q_1 + \theta(m)$ , predicts $1$ if $q_1 > q_0 + \theta(m)$ , and may predict either otherwise. After a mistake, every active member that disagreed with the label has its weight multiplied by $\beta$ . The weights $\omega_i$ of the analysis are the current weight of an active member and $W(i)$ for an inactive one.

Formalization targets

The goal is Theorem 4.1, part 3 (p. 227). Let $m$ be the total number of mistakes of $\mathrm{WMI}_2$ on the sequence.

Goal: the mistake bound of $\mathrm{WMI}_2$

If $0 < \beta < 1$ , then

m \le \inf_{i \ge 1} \frac{\log\bigl(\hat W(1)/W(i)\bigr) + m_i \log(1/\beta) + \log 2}{\log(1/u)} ,

and if $\beta = 0$ and $m_i = 0$ for some $i$ , then $m \le 1 + \log_2\bigl(\hat W(1)/W(i)\bigr)$ .

Milestone: the size of the active pool (Theorem 4.1, part 1)

At the beginning of any trial, $l$ is the minimum $l$ with $\hat W(l+1) \le \theta(m)$ , where $m$ counts the mistakes made in prior trials.

Milestone: the weight invariant (Theorem 4.1, part 2)

After any initial sequence of trials in which $m$ mistakes have been made,

\sum_{i=1}^{\infty} \omega_i \le \Bigl(2 - \frac{1}{m+1}\Bigr) u^{m}\, \hat W(1) .

Significance

The result. The bound holds simultaneously for every pool member, so the master competes with the best member of an infinite pool, paying $\log(\hat W(1)/W(i))$ for the position of that member in the enumeration. With $W(i) = 1/(i(i+1))$ and $\hat W(i) = 1/i$ (the paper's Corollary 4.1) this is $O(\log i + m_i)$ mistakes, with an active pool that grows exponentially in the number of mistakes but is finite at every time. Different choices of $W$ trade the mistake bound against the growth of the active pool. The same analysis shows how the predictions can be computed from finite-precision approximations of the weights, which is the reason for the slack band in the prediction rule. Its $\beta = 0$ case recovers the Barzdin–Freivalds bound.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist, and there is no formalization of the Weighted Majority Algorithm on infinite pools on Prove2Me. The work is to formalize the paper's proof: the size statement for the active pool, the inductive invariant for the total weight, and the final logarithmic bound. The definition of a run of $\mathrm{WMI}_2$ , with free predictions in the slack band and lazily activated weights, is reusable for other lazy-activation algorithms on countable pools, and the paper's Corollaries 4.1–4.3 are direct instances once the goal is proved.

Difficulty

The ordinary Weighted Majority analysis tracks the total weight of the whole pool, which shrinks by the factor $u$ after each mistake. For $\mathrm{WMI}_2$ that argument does not apply as is: the master only sees the active weights, and the inactive tail, whose weight is unknown to the algorithm and charged at its initial value, may vote with the label. The obvious bound on the tail is too weak if applied with a fixed slack; it must shrink with the number of mistakes at the right rate so that the accumulated overhead stays below a constant factor. The slack band in the prediction rule interacts with this: when the master errs inside the band, the active majority may not have been wrong by much, and the shrinkage factor must be recovered from the band's width. The factor $2 - 1/(m+1)$ is where these effects are balanced.

Formalization scope

The pool is indexed by ℕ+ and trials by Fin T; false encodes the prediction $0$ , true the prediction $1$ . IsWMI2Run is a relation between the input sequence and the master's predictions, the weights $w_t(i)$ and the active-pool sizes $l_t$ at every trial boundary $t \in \{0, \dots, T\}$ ; a prediction inside the slack band is unconstrained, so the theorems hold for every run. Only active weights are constrained; the analysis uses omega, which counts inactive members at $W(i)$ . The bound $m_i$ is any upper bound on the mistakes of $A_i$ . The tail hypothesis is stated with a tsum together with Summable W, and the milestone on the total weight asserts summability of $\omega$ in its conclusion, so it cannot hold through the value $0$ that Lean assigns to a divergent series. The infimum in the goal is stated as a bound for every $i$ , which is equivalent. Logarithms in the ratio are natural logarithms (the base cancels); the $\beta = 0$ bound uses Real.logb 2. The paper requires $W$ and $\hat W$ to be computable; this only makes the algorithm implementable, and the formal statements hold for arbitrary real functions with the stated analytic properties.

A statement for an algorithm whose runs do not exist would be vacuous; runs of $\mathrm{WMI}_2$ exist for every sequence under the hypotheses (this has been checked locally in Lean), because $\hat W \to 0$ and $\theta(m) > 0$ keep the active pool finite.

Needed infrastructure: finite sums over the active pool, tsum manipulations for sequences that agree with $W$ outside a finite set, and real logarithm inequalities. Contributions welcome: proofs of the two milestones and the goal, and the Corollaries 4.1–4.3 as follow-up statements.

Selected references

N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
J. M. Barzdin, R. V. Freivalds, On the prediction of general recursive functions, Soviet Mathematics Doklady 13, 1224–1228, 1972.
J. M. Barzdin, R. V. Freivalds, Prognozirovanie i predel'nyi sintez effektivno perechislimykh klassov funktsii [Prediction and limit synthesis of effectively enumerable classes of functions], in Theory of Algorithms and Programs (J. M. Barzdin, ed.), Vol. 1, 101–111, Latvian State University, 1974 (in Russian).
N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proceedings of the 30th Annual Symposium on Foundations of Computer Science, 256–261, IEEE, 1989 (cited in the journal paper as [LW89a]).

4 thms2 active usersReviewed

Completed

Combinatorics·Captain: xuanji

Deterministic APSP in O(n^2.99791) time on a Word RAMResearch Paper

Motivation

All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an $n$ -vertex weighted directed graph. Floyd–Warshall solves it in $O(n^3)$ time, and for decades no algorithm beat $n^{3-\delta}$ for any constant $\delta>0$ on graphs with polynomially bounded integer weights. The APSP conjecture of fine-grained complexity asserted that none exists. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) refuted it with a deterministic $O(n^{2.99942})$ algorithm. That bound is the campaign's first entry, and it is formally proved on the platform.

This entry records the deterministic exponent $2.99791$ , obtained by tightening the accounting in the same algorithm.

Setting

The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo $2^W$ , indirect load and store, a sign branch, and accept or reject, on words of width $W \ge b(\log_2 n + 1)$ . Inputs have integer weights of absolute value at most $n^\kappa$ for a fixed $\kappa$ , and there are no negative cycles. The machine has no source of randomness, so randomized (Las Vegas) algorithms do not count.

Formalization target

The goal is the campaign template with the value $2.99791$ :

\texttt{TrulySubcubicAPSP.APSP.SolvedInTime}\ 2.99791,

which says there is a deterministic word-RAM program that solves APSP in $O(n^{2.99791})$ steps.

How the bound arises

The core of the published algorithm is a data structure for thin min-plus-type products with inner dimension $D = N^\varepsilon$ . It has preprocessing $\tilde O(N^2/D^{\Gamma})$ and queries $\tilde O(D^{q})$ , with parameters $c = L/m$ (recursion ratio) and $\theta = t/m$ (switch threshold). Four changes improve the saving $3 - \omega_{\mathrm{APSP}}$ from $0.00058$ to about $0.0021$ :

All-edges Exact Triangle (paper, footnote 10). APSP reduces to all-edges Exact Triangle, and then to min-plus product, by determining $A\star B$ one bit at a time from $\lfloor A/2\rfloor\star\lfloor B/2\rfloor$ with two all-edges calls per bit, followed by repeated squaring. This keeps the whole Exact Triangle saving, where the decision-version route keeps only a third of it.
Exact binomial tail. With $\beta_d = \binom{L}{m-d}9^{L-m+d}$ , Stirling's formula gives a box-preprocessing tail $D^{-\Gamma(c,\theta)+o(1)}$ , where $\Gamma(c,\theta) = \bigl(cH(1/c) - cH((1-\theta)/c) - \theta\ln 9\bigr)/\ln 4$ . This replaces the paper's geometric estimate $\gamma = \theta\ln((c-1)/9)/\ln 4$ .
Pruned encodings. Encoding branches whose prefix holds more than $m$ copies of the distinguished branch $P_0$ are discarded. This lowers the encoding exponent to $A_{\mathrm{pruned}}(c) = \bigl(\tfrac12 cH(1/c) + (c-1)\ln 3\bigr)/\ln 4$ , so the thinness condition becomes $\varepsilon < 1/(A_{\mathrm{pruned}}+\Gamma)$ .
True middle dimension in the deterministic hashing reduction. Take prime size $n^u$ and block size $n^v$ with $u+v=\varepsilon$ , and balance preprocessing, queries and false-positive scanning. The resulting saving is

\delta_{\det} = \varepsilon\min\Bigl\{\frac{\Gamma}{2},\ \frac{1-2q}{3}\Bigr\},\qquad q(\theta) = \frac{H(\theta)+\theta\ln 9}{\ln 4}.

The explicit parameters $c = 21.915$ , $\theta = 0.116107$ and $\varepsilon = 0.055197$ satisfy the thinness condition ( $\varepsilon_{\max} = 0.0551984\ldots$ ) and give $\delta_{\det} = 0.00209524\ldots$ . Since $3 - 0.00209524 < 2.99791$ , the slack absorbs all polylogarithmic factors.

Significance

The randomized version of the same argument reaches about $2.99601$ by repeating random-prime hashing. That bound is out of reach in this deterministic model. Closing the gap between deterministic and randomized collision handling is a natural next target for the campaign.

Selected references

J. Alman and V. Vassilevska Williams, Truly subcubic APSP (2026). https://arxiv.org/abs/2610.06783
T. Kopelowitz, S. Pettie and E. Porat, Higher lower bounds from the 3SUM conjecture, SODA 2016.
Refined exponent accounting (unpublished AI-assisted calculation, October 2026). This is the source of $2.99791$ and has not been peer reviewed.

5 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+1·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 1: Binary Search over Rounded LP Vertices Finds a Schedule within Twice the Optimal MakespanResearch Paper

Motivation

Scheduling unrelated parallel machines to minimize the makespan, written $R\,\|\,C_{\max}$ , is one of the basic NP-hard problems of scheduling theory. A set of jobs must each be run on one of several machines, and the time a job takes depends arbitrarily on the machine; the goal is to finish all jobs as early as possible. Before the work formalized here, the best polynomial algorithm known guaranteed only a schedule within $2\sqrt m$ times the optimum (Davis and Jaffe, 1981), a factor that grows with the number of machines $m$ .

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714, 1987; Math. Programming 46, 1990) gave a polynomial algorithm with guarantee $2$ , independent of $m$ . Their tool is a rounding theorem: a vertex of a natural linear-programming relaxation can be rounded to an integral schedule that exceeds each machine's budget by at most one job. The rounding theorem and the binary-search framework around it became standard material in approximation algorithms.

Setting

There are $n$ jobs and $m\ge 1$ machines. If job $j$ is scheduled on machine $i$ , it takes $p_{ij}$ time units, a positive integer. A schedule $\sigma$ assigns every job $j$ to one machine $\sigma(j)$ . The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$ , the makespan of $\sigma$ is the largest load, and $\mathrm{OPT}$ is the minimum makespan over all schedules.

For deadlines $d_1,\dots,d_m$ and a threshold $t$ , let $J_i(t)=\{j: p_{ij}\le t\}$ and $M_j(t)=\{i : p_{ij}\le t\}$ . The linear program (LP) has variables $x_{ij}\ge 0$ for $j\in J_i(t)$ and constraints

\sum_{i\in M_j(t)}x_{ij}=1\quad(j=1,\dots,n),\qquad \sum_{j\in J_i(t)}p_{ij}x_{ij}\le d_i\quad(i=1,\dots,m).

The integer program (IP) replaces $d_i$ by $d_i+t$ and requires $x_{ij}\in\{0,1\}$ . A vertex of (LP) is an extreme point of its feasible polytope. The support graph of a point $\tilde x$ is the bipartite graph on machines and jobs with an edge $(i,j)$ whenever $\tilde x_{ij}>0$ .

A $\rho$ -relaxed decision procedure answers, for a deadline $d$ , either 'no' or a schedule, such that (1) every schedule it returns has makespan at most $\rho d$ , and (2) if it answers 'no', no schedule has makespan at most $d$ . The binary search of Lemma 1 starts from the greedy schedule (each job on a machine where it runs fastest), whose makespan $t$ is an upper bound $u$ , with lower bound $l=\lceil t/m\rceil$ , queries the procedure at $d=\lfloor(u+l)/2\rfloor$ , moves $u$ to $d$ on a schedule and $l$ to $d+1$ on 'no', and outputs the best schedule found once $l=u$ .

The LP rounding procedure answers, on deadline $d$ , by solving (LP) with $d_1=\dots=d_m=t=d$ : 'no' if it is infeasible, and otherwise a 0-1 solution of (IP) obtained by rounding a vertex $\tilde x$ chosen by the LP solver, supported on $\tilde x$ .

Formalization targets

Goal: Theorem 2

For every LP solver (every rule choosing a vertex of (LP) when it is feasible), an LP rounding procedure $D$ exists, and for every such $D$ the output $\sigma_D$ of the binary search satisfies

\operatorname{makespan}(\sigma_D)\le 2\cdot\mathrm{OPT}.

Milestones

The support graph of every vertex of (LP) is a pseudoforest: every set $S$ of machines and $T$ of jobs spans at most $|S|+|T|$ edges (§2, p. 4).
In a machine–job pseudoforest, every set of jobs of degree at least $2$ can be matched injectively into the machines (§2, pp. 4–5).
A schedule supported on a feasible $\tilde x$ with at most one fractional job per machine has loads at most $d_i+t$ (§2, p. 5).
Theorem 1 (Rounding Theorem): every vertex $\tilde x$ of (LP) has a schedule $\sigma$ supported on $\tilde x$ with

\sum_{j:\sigma(j)=i}p_{ij}\le d_i+t\qquad(i=1,\dots,m).

Lemma 1: for every $\rho$ -relaxed decision procedure, the binary search outputs a schedule of makespan at most $\rho\cdot\mathrm{OPT}$ .
A schedule with makespan at most $d$ gives a feasible point of (LP) with $d_i=t=d$ (§3, p. 5).
The LP rounding procedure is $2$ -relaxed (§3, pp. 5–6).

Significance

Theorem 2 gives a constant-factor approximation for $R\,\|\,C_{\max}$ that does not depend on $m$ . The same rounding theorem drives the paper's second algorithm, a $(1+\epsilon)$ -approximation for a fixed number of machines using polynomial space, and the paper's lower bound shows that no polynomial algorithm achieves a factor below $3/2$ unless $\mathrm{P}=\mathrm{NP}$ . The Rounding Theorem, in its later form for generalized assignment by Shmoys and Tardos (1993), is a standard tool for LP-based scheduling and assignment.

The result is proved; it has, to our knowledge, no machine-checked proof. The platform contains Matoušek and Gärtner's textbook version (MatousekLP.Scheduling.lst_two_approximation, Theorem 8.3.4 of Understanding and Using Linear Programming), which uses a different relaxation: one bound minimized parametrically over $T$ , optimal solutions with linearly independent columns, and no per-machine deadlines. This mission formalizes the report's own route: deadlines $d_i$ , arbitrary vertices, binary search over a relaxed decision procedure. A formal proof would also yield reusable statements about extreme points of transportation-type polytopes and matchings in pseudoforests.

Difficulty

The obvious rounding, putting each job on a machine where $\tilde x_{ij}$ is largest, can overload a machine by many jobs at once: nothing in feasibility alone prevents many jobs from each placing a small fraction on the same machine. The bound $d_i+t$ requires that each machine receive at most one job that the vertex treats fractionally, and this fails for general feasible points; it holds only because $\tilde x$ is a vertex. The step that carries the weight is therefore a statement about the combinatorial structure of the support of an extreme point, which must be derived from the linear independence of the tight constraints, followed by a matching argument on the resulting graph. Neither step is available in Mathlib in the form needed.

On the algorithmic side, the binary search must be shown to return a schedule within $\rho\cdot\mathrm{OPT}$ although the decision procedure is only approximately correct; the invariants (the lower bound stays below $\mathrm{OPT}$ , the stored schedule stays within $\rho$ times the upper bound) have to be tracked through a recursion.

Formalization scope

Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive in Lemma 1 and Theorem 2 (the paper's model, p. 2). Loads, makespans and optimal schedules are the published MatousekLP.Scheduling.Schedule definitions applied to the real matrix $(p_{ij})$ ; $\mathrm{OPT}$ is the makespan of a schedule σopt with IsOptimalSchedule.
(LP) is modelled on full $m\times n$ real matrices with the entries $p_{ij}>t$ fixed to $0$ ; this polytope is affinely isomorphic to the paper's, so vertices (Mathlib's Set.extremePoints) correspond exactly. Theorem 1 and its steps are stated for real deadlines and real $t\ge 0$ , more general than the paper's integers; the paper's proof does not use integrality, and mission 2 of this series needs non-integral $t$ .
Algorithmic wording not formalized. Theorem 2 states "a 2-approximation algorithm ... that runs in time bounded by a polynomial in the input size"; Lemma 1 speaks of polynomial procedures; Theorem 1 adds "this rounding can be done in polynomial time". Running time, the ellipsoid method and vertex finding are not formalized. What is formalized is the guarantee the proofs establish: the binary search, written as a Lean function, returns a schedule within $\rho\cdot\mathrm{OPT}$ (Lemma 1, for every $\rho$ -relaxed procedure) and within $2\cdot\mathrm{OPT}$ for every LP rounding procedure and every choice of vertex (Theorem 2).
Explicit constants: the factor $2$ of Theorem 2 and of the $2$ -relaxed procedure, which comes from $d_i+t$ with $d_i=t=d$ ; the overshoot $t$ of Theorem 1; the initial bounds $u=$ greedy makespan and $l=\lceil u/m\rceil$ (the paper's $t/m$ , rounded up because $\mathrm{OPT}$ is an integer); the query point $\lfloor(u+l)/2\rfloor$ .
The LP solver's choice is quantified over by a vertex selector, returning a vertex when (LP) is feasible and nothing otherwise; one always exists, since the polytope is compact.
Trivializing formalization ruled out. "There is a schedule with makespan at most $2\cdot\mathrm{OPT}$ " is trivially witnessed by an optimal schedule; the goal instead bounds the output of the binary search, whose every 'almost' answer must be a rounding of the solver's vertex, supported on it and feasible for (IP).
Needed infrastructure: extreme points of polytopes given by linear constraints and their tight-constraint rank characterization; bipartite pseudoforests and Hall-type matchings; well-founded recursion for the search. Proofs of any milestone, and reusable lemmas on extreme points of assignment polytopes, are welcome.

Selected references

J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (the source of this mission's statements and numbering); also Proc. 28th IEEE Symposium on Foundations of Computer Science (1987) 217–224
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271, https://doi.org/10.1007/BF01585745
E. Davis, J. M. Jaffe, Algorithms for scheduling tasks on unrelated processors, Journal of the ACM 28 (1981) 721–736, https://doi.org/10.1145/322276.322284
D. B. Shmoys, É. Tardos, An approximation algorithm for the generalized assignment problem, Mathematical Programming 62 (1993) 461–474, https://doi.org/10.1007/BF01585178
J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3, https://doi.org/10.1007/978-3-540-30717-4

11 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 6: Concatenating Optimal Schedules of Processor Pairs Gives Finish Time within ⌈m/2⌉ Times the OptimumResearch Paper

Motivation

A flow shop is the simplest model of a production line: every job passes through the same sequence of machines in the same order. Minimizing the time at which the last job leaves the last machine (the finish time, or makespan) is easy for two machines, where Johnson's rule gives an optimal schedule in time $O(n\log n)$ (Johnson 1954), and NP-hard from three machines on (Garey, Johnson, Sethi 1976; Gonzalez, Sahni 1978, §1, for preemptive schedules). For three or more machines the practical question is therefore how far a fast heuristic can be from the optimum in the worst case.

Gonzalez and Sahni (1978, §2) first show that any busy schedule, one that never leaves a processor idle while a task is available for it, has finish time at most $m$ times the optimum (their Lemma 10), and that the natural "longest job first" order does no better. They then give a heuristic, H, that uses Johnson's two-machine algorithm as a subroutine and has the better worst-case ratio $\lceil m/2\rceil$ (Lemma 11). This mission formalizes that bound.

Setting

A flow shop has $m$ processors $P_1,\dots,P_m$ and $n$ jobs. Job $i$ consists of $m$ tasks; task $j$ runs on processor $P_j$ and needs processing time $t_{j,i}\ge 0$ (zero is allowed). A non-preemptive schedule gives every task a start time $s_{j,i}$ , and the task occupies $P_j$ during $[s_{j,i},s_{j,i}+t_{j,i})$ . It is feasible when all start times are nonnegative, when task $j+1$ of a job starts only after task $j$ of that job has completed ( $s_{j,i}+t_{j,i}\le s_{j+1,i}$ ), and when no processor runs two tasks of positive length at the same time. Its finish time $\mathrm{FT}(s)$ is the latest completion time $s_{j,i}+t_{j,i}$ (and $0$ if there is no task). An optimal finish time (OFT) schedule $S^*$ is a feasible schedule of least finish time.

Heuristic H (p. 48) divides the processors into $\lceil m/2\rceil$ groups: group $g$ consists of $P_{2g-1}$ and $P_{2g}$ , and when $m$ is odd the last group is $P_m$ alone. The flow shop $F_g$ on group $g$ has the same jobs, with task times $t_{2g-1,i},t_{2g,i}$ only. For each group an OFT schedule $R(g)$ of $F_g$ is computed (by Johnson's algorithm), with finish time $f(R(g))$ . The schedule $S$ generated by H runs these schedules one after another: every task of group $g$ starts at its time in $R(g)$ plus the offset $\sum_{h<g}f(R(h))$ .

Formalization targets

Goal: Lemma 11 (p. 49)

For every flow shop with $m$ processors and $n$ jobs, every choice of OFT schedules $R(g)$ of the group flow shops, the schedule $S$ generated by H, and every feasible non-preemptive schedule $\tau$ of the flow shop (in particular an OFT schedule $S^*$ ),

\mathrm{FT}(S)\le\Big\lceil\frac m2\Big\rceil\,\mathrm{FT}(\tau).

The paper writes this as $\mathrm{FT}(S)/\mathrm{FT}(S^*)\le\lceil m/2\rceil$ .

Milestones

Every group flow shop $F_g$ has an OFT schedule (p. 48; the paper obtains it with Johnson's algorithm).
The concatenation of feasible group schedules is a feasible schedule of the $m$ -processor flow shop (p. 48).
$\mathrm{FT}(S^*)\ge\max_g f(R(g))$ (proof of Lemma 11, p. 49).
$\mathrm{FT}(S)\le\sum_g f(R(g))\le\lceil m/2\rceil\max_g f(R(g))$ (proof of Lemma 11, p. 49).

Significance

The result gives a polynomial-time heuristic, running in time $O(mn\log n)$ , whose finish time is within a factor $\lceil m/2\rceil$ of the optimum on every instance, half the factor $m$ that every busy schedule already achieves. The paper's Example 4 (p. 49) shows that for $m=3$ the factor $2=\lceil 3/2\rceil$ is approached, so the analysis cannot be improved in general.

Formalizing it produces a reusable, machine-checked model of the $m$ -processor flow shop with non-preemptive schedules, its restriction to blocks of consecutive processors, and the concatenation of schedules of disjoint blocks. Lemma 11 has a short paper proof; to our knowledge it has no machine-checked proof. The model's careful treatment of zero task times, of odd $m$ , and of the restriction of a schedule to a processor group is itself part of the value: these are the points at which an informal argument is silent.

Difficulty

The arithmetic of the bound is short; the content lies in two structural facts about a precise model: that the concatenated object is a feasible schedule of the whole flow shop, including across the boundary between consecutive groups and for a final group of a single processor, and that the optimum of the whole flow shop is at least the optimum of each group flow shop, whose first processor has no predecessor. Informal arguments are silent on exactly these points. A naive formalization that leaves the offsets free, or that does not require the $R(g)$ to be optimal, makes the statement false; one that lets $S$ be any schedule with the right restrictions makes it witnessed by $S^*$ itself.

The existence of OFT schedules for the group flow shops (milestone 1) is a separate matter: the paper takes it from Johnson's algorithm, and proving it requires an optimality argument for two-machine flow shops (or a compactness argument over finitely many processing orders).

Formalization scope

Representation. Processors are Fin m and jobs Fin n, both 0-based; times are real numbers. A flow shop is a matrix t : Fin m → Fin n → ℝ with t ≥ 0. A schedule is a matrix of start times. Group $g$ (0-based, g : Fin ((m + 1) / 2)) contains the processors $2g$ and $2g+1$ that exist, min 2 (m - 2g) of them.
Finish time. A fold of max with baseline $0$ over all tasks; it is $0$ for $m=0$ or $n=0$ . The maximum of the group finish times is also a fold of max with baseline $0$ . No supremum over an unbounded or empty set is taken.
Zero task times. A zero-length task occupies no processor time (it is exempt from the non-overlap condition) but still respects the job's task order and counts in the finish time when it is placed late; optimal schedules are unaffected.
The optimum. "OFT schedule $S^*$ " is replaced by a universally quantified feasible schedule $\tau$ , which is stronger and needs no existence assumption for $S^*$ . Optimality of $R(g)$ is the predicate "feasible, and finish time at most that of every feasible schedule of the same group flow shop".
Constants. $\lceil m/2\rceil$ is (m + 1) / 2 in $\mathbb N$ , cast to $\mathbb R$ ; the two agree for every $m\ge 0$ . The ratio is multiplied out, so a zero optimum does not divide by zero.
Not formalized. Johnson's algorithm and the running times $O(n\log n)$ and $O(mn\log n)$ . The goal quantifies over every family of optimal group schedules, which includes the one Johnson's algorithm computes; the paper's proof uses only optimality. The preemptive comparison on p. 50 and the tightness examples are outside the mission.
Trivialization ruled out. The schedule $S$ is a function of the $R(g)$ with the fixed offsets $\sum_{h<g}f(R(h))$ , and each $R(g)$ must be optimal for its group flow shop; neither the offsets nor $S$ are free.
Infrastructure. Elementary facts about Finset.fold max and sums over Fin; nothing beyond Mathlib. Contributions proving milestone 1 by formalizing Johnson's rule for this model are welcome and reusable.

Selected references

T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117

7 thms2 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 5: Sequencing Jobs by Shortest Total Processing Time Gives Mean Flow Time within m Times the OptimumResearch Paper

Motivation

Flow shops and job shops are the basic models of multi-stage production: every job passes through several machines, and each machine handles one task at a time. Gonzalez and Sahni (Operations Research 26(1), 1978) showed that minimizing the finish time of such shops is NP-complete even with preemption, and then asked how well simple heuristics do. One of the two objectives they study is the mean flow time, the average completion time of the jobs, which measures how long a job spends in the shop on average.

Their Lemma 9 analyses the most natural rule for that objective, shortest processing time first (SPT): process the jobs in order of nondecreasing total work. For a single machine SPT is optimal (Smith 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 76, which the paper cites). Lemma 9 shows that with $m$ processors the same rule loses at most a factor $m$ , and the paper's Example 2 shows that the factor $m$ is attained in the limit.

Setting

A job shop has $m\ge1$ processors $P_1,\dots,P_m$ and $n$ jobs. Job $i$ is a finite sequence of tasks; each task names the processor that must process it and a processing time $p\ge0$ . The tasks of a job are processed in their order: a task may start only after the job's previous task has completed. A flow shop is the special case in which every job has $m$ tasks and its $k$ -th task runs on $P_k$ .

A non-preemptive schedule gives every task a start time $s\ge0$ ; the task then occupies its processor during $[s,s+p)$ , and two distinct tasks on one processor never overlap. The finish time $f_i(S)$ of job $i$ in schedule $S$ is the time at which all tasks of job $i$ have been completed, and the mean flow time is

\mathrm{MFT}(S)=\frac1n\sum_{i=1}^n f_i(S).

An OMFT schedule $S^*$ is a feasible schedule of least mean flow time.

Let $L_i$ be the sum of the task times of job $i$ . An SPT order is a listing $\sigma(0),\dots,\sigma(n-1)$ of the jobs with $L_{\sigma(0)}\le\dots\le L_{\sigma(n-1)}$ , ties broken arbitrarily. The SPT schedule processes the jobs in that order: each job in turn, each positive-time task starting at the later of the completion of the job's previous task and the latest completion of a task already placed on its processor. A zero-time task completes when its preceding task completes and leaves the processor available.

Formalization targets

Goal: Lemma 9

For every job shop, every SPT order $\sigma$ with SPT schedule $S$ , and every feasible non-preemptive schedule $\tau$ ,

\mathrm{MFT}(S)\le m\cdot\mathrm{MFT}(\tau),

so that $\mathrm{MFT}(S)/\mathrm{MFT}(S^*)\le m$ for an OMFT schedule $S^*$ . A separate item states the same bound for flow shops.

Milestones

The milestones follow the paper's proof of Lemma 9 on p. 47:

the SPT schedule is a feasible schedule;
the job in position $k$ of the SPT schedule finishes by $\sum_{j\le k}L_{\sigma(j)}$ ;
in any feasible schedule, if $i_1,\dots,i_n$ is the order in which the jobs finish, then $f_{i_k}\ge\sum_{j\le k}L_{i_j}/m$ ;
a prefix sum of any listing of the $L_i$ is at least the corresponding prefix sum of the sorted listing;
$\mathrm{MFT}(S^*)\ge\frac1n\sum_{k=1}^n\sum_{j=1}^k L_j/m$ .

Significance

Lemma 9 is one of the earliest performance guarantees for a shop-scheduling heuristic under a sum objective. It shows that a rule computable by one sort, $O(n\log n)$ plus a linear pass, is within a factor equal to the number of machines, independently of the number of jobs. This is better than the factor $n$ that Lemma 8 of the same paper gives for an arbitrary busy schedule, whenever $m<n$ . Example 2 of the paper shows that the factor cannot be improved for SPT. Lower bounds of the work-per-machine type used here recur in later approximation results for total completion time in shops and on parallel machines.

The result has been proved since 1978. As far as a search of the Prove2Me catalogue shows, it has not been machine-checked. This mission adds a machine-checked statement of the SPT schedule as an algorithm, not as an arbitrary schedule with a property. It also adds the guarantee for job shops with arbitrary task sequences, of which flow shops are a special case.

Difficulty

The arithmetic of the proof is short. The work is in two places. The SPT schedule is a concrete construction, a fold over jobs and tasks that updates processor availability, so the bound on its finish times has to be carried through an invariant of that construction. The lower bound on every feasible schedule needs a packing argument: tasks on one processor that complete by a given time have total length at most that time. That argument is not available in Mathlib in a form that applies here. The tempting shortcut of comparing the two schedules job by job fails: the optimal schedule need not finish jobs in SPT order, so the comparison must go through sums of sorted prefixes.

Formalization scope

Instance and feasibility. The job data come from the published JobShopLTAS.Core.Instance (jobs Fin n, processors Fin m, tasks Fin (μ j), real processing times $\ge0$ ). The local IsPaperFeasibleSchedule requires nonnegative starts, in-job order, and no overlap of positive-time tasks on the same processor. Zero-time tasks occupy no processor interval. The paper assumes $m\ge1$ , and the scheduling theorems carry that hypothesis.
Finish time and MFT. $f_i$ is the maximum completion time over the tasks of job $i$ , with baseline $0$ ; MFT divides by $n$ , and for $n=0$ both sides are $0$ .
The SPT schedule is the list schedule constructed by the heuristic, for every SPT order, so ties are broken in every possible way. Zero-time tasks do not advance processor availability. It is not "any feasible schedule whose jobs finish in SPT order", a reading under which an optimal schedule would qualify and the goal would be trivial.
The optimum. The paper's "Let $S^*$ be an OMFT schedule" is stated as "for every feasible non-preemptive schedule $\tau$ ". This is equivalent and does not assume that an optimum exists.
Ratios multiplied out. $\mathrm{MFT}(S)/\mathrm{MFT}(S^*)\le m$ is stated as $\mathrm{MFT}(S)\le m\cdot\mathrm{MFT}(\tau)$ , and the proof's bounds divided by $m$ are multiplied by $m$ . No division by a possibly zero quantity occurs.
Constants. The only constant is the factor $m$ , the number of processors.
Not formalized. The running time of SPT, the comparison with Lemma 8 and its remark "it is assumed that $m<n$ " (not a hypothesis of Lemma 9), and the tightness Example 2.
Milestones 2 and 4 are stated for every listing $\sigma$ and every pair of listings; they are combinatorial facts about list schedules and sorted sums that are reusable beyond this mission. Proofs of any milestone, and a reusable packing lemma for non-overlapping intervals, are welcome.

Selected references

T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106
K. Jansen, R. Solis-Oba, M. Sviridenko, Makespan Minimization in Job Shops: A Linear Time Approximation Scheme, SIAM J. Discrete Math. 16(2), 288–300, 2003 (source of the job-shop definition reused here). https://doi.org/10.1137/S0895480199363908

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 4: The 3-Partition Job Shop on Two Machines Has a Schedule of Finish Time 2tB, Preemptive or Not, Iff a 3-Partition ExistsResearch Paper

Motivation

In a job shop, each job has an ordered list of tasks, and each task must use a specified machine. A production planner may be able to interrupt a task and resume it later, yet still be unable to find a short schedule efficiently. Gonzalez and Sahni studied how the ability to preempt changes the difficulty of minimizing the time at which all jobs are complete. Their 1978 paper establishes complexity results for flow shops and job shops and then examines approximation schedules when exact optimization is difficult (Gonzalez and Sahni, 1978).

This mission concerns the paper's two-machine construction from 3-PARTITION. It is the reduction used for their claim that finding an optimal preemptive or non-preemptive finish-time schedule remains NP-complete when input size is measured by the sum of task lengths. The formal target isolates the decision equivalence proved for the constructed instance. It gives solvers a precise schedule statement to establish without conflating the scheduling theorem with the separate complexity-class argument.

Setting

A 3-PARTITION input $C$ comprises an integer $t\ge0$ , a positive integer target $B$ , and $s=3t$ positive integer sizes $a_1,\ldots,a_s$ . A valid input satisfies

\sum_{i=1}^{s}a_i=tB,\qquad B/4<a_i<B/2\quad(1\le i\le s).

It has a 3-partition when the $s$ indices can be assigned to $t$ disjoint groups, each containing exactly three indices and having total size $B$ . The strict bounds rule out groups of other cardinalities at that sum and are part of the source problem, not a convenience added for formalization. When $t=0$ , the input has no sizes or groups and the empty grouping is a solution.

The paper builds a job shop $JS(C)$ with machines $P_1,P_2$ and $s+1$ jobs. For $1\le i\le s$ , job $i$ has a task of length $a_i$ on $P_1$ , followed by a task of length $a_i$ on $P_2$ . The last job, $s+1$ , has $2t$ tasks, each of length $B$ . Its tasks alternate between the machines, starting on $P_2$ . This last order matters: reversing it would produce a different construction. The source gives the decision threshold $\tau=2tB$ (Lemma 7, p. 44).

A non-preemptive schedule gives each task one continuous processing interval. A preemptive schedule may divide an operation into finitely many positive-length intervals. In either case, jobs obey their task order, distinct pieces on the same machine do not overlap, and processing starts at or after time zero. Write $FT(S)$ for the time at which all tasks of schedule $S$ have finished. The paper allows the same job to revisit a machine, as the final job does here.

Formalization targets

Lemma 7: the constructed instance

For every valid $C$ , the main goal states both the paper's preemptive equivalence and the non-preemptive form established by its two directions:

\begin{aligned} \exists S\text{ preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition},\\ \exists S\text{ non-preemptive for }JS(C): FT(S)\le2tB &\iff C\text{ has a 3-partition}. \end{aligned}

The milestones follow the source's proof text: the schedule supplied by a solution in Lemma 7(a), the timing forced on the final job, the exclusion of short preemptive schedules in Lemma 7(b), and the preemptive equivalence stated in the proof. The final-job milestone describes the occupied time slots of the paper's Figure 4, independently of how many adjacent pieces a formal schedule uses.

Significance

The equivalence transfers the distinction between solvable and unsolvable 3-PARTITION inputs to an exact finish-time threshold in a job shop with only two machines. It also establishes the non-preemptive decision equivalence for this construction, because a solution yields a non-preemptive schedule while an unsolvable input rules out even the more permissive preemptive schedules. These facts supply the scheduling part of the paper's strong NP-completeness claim; membership in NP is handled separately by Lemma 6 (pp. 44–45).

The result is proved in the source paper. The work proposed here is a machine-checked development of its explicit reduction equivalence and the finite-piece scheduling model needed to state it. The milestone theorems expose statements that can be reused when formalizing other preemptive scheduling reductions. The shared job-shop instance and 3-PARTITION input are already published definitions; the particular reduction instance and preemptive schedule predicate are new local definitions.

Difficulty

Preemption makes a task's processing time distributable across intervals. Merely checking that each machine has enough total capacity does not characterize feasible schedules: every job's operations must still occur in order, and pieces of different jobs must avoid one another on each machine. The converse direction must constrain every preemptive schedule that meets the threshold, not only a schedule having the visual pattern in Figure 4. A schedule can also represent one uninterrupted interval as several adjacent pieces, so piece count alone cannot express the source's timing claim.

Formalization scope

Machines are Fin 2, with $P_1$ numbered $0$ and $P_2$ numbered $1$ . Jobs are Fin (3t+1); the final job is index $3t$ . Its zero-based operation $i$ uses machine $1$ for even $i$ and machine $0$ for odd $i$ . The definition uses the published JobShopLTAS.Core.Instance for ordered operations, machines, real processing times, and non-preemptive feasibility. It uses the published ResourceScheduling.Chain.ThreePartition for $t,B,a_i$ , validity, and solutions. Those objects have the same conventions as the paper here. The local preemptive model uses finitely many positive-length pieces per task, whose durations sum exactly to that task's processing time. The threshold is the explicit real cast of $2tB$ ; no real infimum or division by a possibly zero optimum appears.

The goal is specific to the instance the paper constructs from each valid input. A free job-shop instance, a freely chosen schedule, or an extra hypothesis that the input has a solution would erase the reduction's content. Validity carries $B>0$ , total $tB$ , and both strict bounds on each $a_i$ . The case $t=0$ remains in scope: the constructed job has no tasks and its finish-time threshold is zero. All existing tasks have positive length whenever the input is valid, so the published non-preemptive predicate's treatment of zero-length tasks does not affect this mission.

The paper states “3-Partition $\alpha$ preemptive JOFT with $m=2$ ” and connects it to NP-completeness for preemptive and non-preemptive scheduling when complexity is measured by the sum of task lengths. The Lean theorem states the proof's two decision equivalences with constant $2tB$ and machine count $2$ . It does not formalize $\alpha$ as a polynomial-time many-one reduction, the unary task-length measure, NP-completeness, or Lemma 6's NP-membership argument. Contributions that establish the reduction statements, the schedule construction, or general finite-piece scheduling facts are within scope.

Selected references

Teofilo Gonzalez and Sartaj Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 1978, pp. 36–52. DOI: 10.1287/opre.26.1.36.

9 thms2 active usersReviewed

Combinatorics Operations Research·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 2: The 3-Partition Flow Shop on Three Machines Has a Preemptive Schedule of Finish Time 2tB Iff a 3-Partition ExistsResearch Paper

Motivation

A flow shop is the simplest multi-stage production model: every job passes through the same machines in the same order, and the question is how to sequence the work so that everything is finished as early as possible. Gonzalez and Sahni's 1978 paper in Operations Research settled the computational complexity of the preemptive version of this problem, in which a task may be interrupted and resumed later on the same machine. For two machines the optimal finish time is computed by Johnson's rule, and preemption does not help. The paper shows that with three machines the preemptive problem is already NP-complete, and its second result, Theorem 2, strengthens this to NP-completeness in the strong sense: the problem stays hard even when the task times are written in unary.

Strong NP-completeness matters because it rules out a pseudo-polynomial algorithm, one whose running time is polynomial in the sum of the task lengths. The preemptive three-machine flow shop ( $F3\mid pmtn\mid C_{\max}$ in later notation) is a standard entry in complexity classifications of scheduling problems, and Theorem 2 is the reference for its status. The paper notes that Garey and Johnson obtained a proof independently.

Timeline. Johnson (1954) solved the two-machine flow shop. Garey, Johnson and Sethi (1976) proved the non-preemptive three-machine flow shop NP-complete in the strong sense. Gonzalez and Sahni (1978) treated the preemptive case: Theorem 1 (ordinary NP-completeness via Partition) and Theorem 2 (strong NP-completeness via 3-Partition), the subject of this mission.

Setting

A flow shop has $m\ge 1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ runs on $P_j$ and takes time $t_{j,i}\ge 0$ ; zero times are allowed. For each job, task $j\ge 2$ can begin only after task $j-1$ has been completed, and schedules start at time $0$ .

A preemptive schedule is given, as in the paper's footnote on p. 40, by finitely many pieces $(s,f)$ per task: the task is processed on its processor during $[s,f)$ . Pieces have $0\le s<f$ , pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$ , and a piece of task $j'$ starts only after every piece of every earlier task $j<j'$ of the same job has ended. A task has no preemption when it is processed in at most one piece; a non-preemptive schedule has no preemption anywhere. The completion time of job $i$ is $f_i(S)$ , the end of its last piece, and the finish time is $FT(S)=\max_i f_i(S)$ .

3-Partition. An instance $C=(a_1,\dots,a_s,B)$ , $s=3t$ , consists of a positive integer $B$ and nonnegative integers $a_i$ with $\sum_i a_i=tB$ and $B/4<a_i<B/2$ . It has a 3-partition if $\{1,\dots,s\}$ splits into $t$ disjoint sets $L_1,\dots,L_t$ , each of three elements with $\sum_{j\in L_k}a_j=B$ .

The instance FS. From $C$ the proof of Lemma 4 builds a three-processor flow shop with $s+t+2$ jobs:

jobs $1,\dots,s$ : times $(a_i,\,0,\,a_i)$ on $(P_1,P_2,P_3)$ ;
job $s+1$ : $(0,\,2B,\,B)$ ;
jobs $s+i+1$ , $1\le i\le t-2$ : $(B,\,2B,\,B)$ ;
job $s+t$ : $(B,\,2B,\,0)$ ;
job $s+t+1$ : $(0,\,0,\,B)$ ;
job $s+t+2$ : $(B,\,0,\,0)$ .

Each processor carries total work exactly $2tB$ , and the threshold is $\tau=2tB$ .

Formalization targets

Goal: Theorem 2, as Lemma 4's equivalence

For every 3-Partition instance $C$ with $t\ge 2$ ,

\exists\,S \text{ preemptive schedule of } FS:\ FT(S)\le 2tB \quad\Longleftrightarrow\quad C \text{ has a 3-partition},

and every task time of $FS$ satisfies $t_{j,i}\le 2B$ . The second clause records that the instance's numbers are bounded by those of $C$ , the reduction's contribution to "the problem size being measured as the sum of the length of the tasks".

Milestones

Lemma 3 (p. 40). For a flow shop with $m\ge 1$ processors, every preemptive schedule $S$ can be replaced by a schedule $S'$ with no preemptions on $P_1$ and on $P_m$ and $FT(S')=FT(S)$ .
Lemma 4(a) (p. 41). If $C$ has a 3-partition, $FS$ has a non-preemptive schedule with $FT\le 2tB$ .
First step of Lemma 4(b) (pp. 41–42). In every preemptive schedule of $FS$ with $FT\le 2tB$ , the jobs among $1,\dots,s$ whose $P_1$ task is completed by time $2B$ have $\sum t_{1,i}=B$ .
Lemma 4(b) (pp. 41–42). If $C$ has no 3-partition, every preemptive schedule of $FS$ has $FT>2tB$ .

Significance

The result. Theorem 2 places the preemptive three-machine flow shop among the strongly NP-hard scheduling problems, so no algorithm polynomial in the number of jobs and the total processing time exists unless P = NP. It also shows that allowing preemption, which makes several single-stage problems (such as $P\mid pmtn\mid C_{\max}$ ) easy, does not help for three-stage flow shops. Lemma 3, that preemptions on the first and last machines can be removed without changing the finish time, holds for any number of machines and is a reusable structural fact about flow-shop schedules.

Formalizing it. The result is proved on paper, and its proof of the "only if" direction is an informal busy-processor argument repeated window by window. As far as is known, no part of it has a machine-checked proof. A formal development has to make the interval accounting rigorous: why each processor is busy throughout $[0,2tB]$ , why exactly $B$ units of element jobs end on $P_1$ by $2B$ , and how the argument restarts on $[2B,2tB]$ . Lemma 3 needs an exchange argument on piece representations. Both are new for the platform.

Difficulty

The direction "3-partition $\Rightarrow$ schedule" is a direct construction. The hard direction is the converse. Preemption lets any task be split across many intervals, so the usual non-preemptive arguments, which reason about the order in which whole tasks run, do not apply directly. The paper's argument that the window $[0,2B]$ must contain exactly three element jobs of total $B$ on $P_1$ depends on every processor being continuously busy, and turning "otherwise there is idle time" into a precise statement requires a careful account of which jobs are available to each processor at each moment. The induction on windows is then not a literal restriction of the schedule to a smaller instance, because pieces may cross the boundary at $2B$ .

Formalization scope

Times are real numbers; the 3-Partition data are natural numbers cast to $\mathbb R$ . Processors are Fin m with $P_1=$ 0; in $FS$ , $P_1,P_2,P_3$ are 0, 1, 2.
The 3-Partition instance is the published ResourceScheduling.Chain.ThreePartition (0-based indices, t parts, b $=B$ , Valid, HasSolution), whose definition is the paper's p. 37 problem.
Preemptive schedules are finite sets of pieces per task; precedence is required between every pair of tasks $j<j'$ of a job, so a zero task occupies no time and does not break the job's order. Finish time is a maximum over jobs with baseline $0$ , never an unattained supremum.
"No preemptions on $P_j$ " means at most one piece per task on $P_j$ .
Not formalized: "NP-complete", the reduction symbol $\propto$ , "the problem size being measured as the sum of the length of the tasks", and Lemma 2 (membership in NP). The goal states the equivalence Lemma 4 proves for the constructed instance, plus the bound $t_{j,i}\le 2B$ on its task times.
Added hypothesis: $t\ge 2$ . For $t<2$ the paper's job indices $s+1$ and $s+t$ coincide with conflicting times, so the construction is undefined there.
The first step of Lemma 4(b) is read as: the sum of $t_{1,i}$ over element jobs whose $P_1$ task has completed by time $2B$ equals $B$ .
A trivializing formalization is ruled out: the schedules quantified over are all preemptive schedules of the specific instance $FS(C)$ , the threshold $2tB$ is explicit, and the validity conditions $B/4<a_i<B/2$ are kept, so the schedule side cannot match the weaker "partition into $t$ groups of sum $B$ ".

Contributions welcome: the interval-accounting lemmas (busy processors, work available before a time), Lemma 3's exchange argument, and the schedule of Figure 2.

Selected references

T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1):36–52, 1978. https://doi.org/10.1287/opre.26.1.36
M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2):117–129, 1976. https://doi.org/10.1287/moor.1.2.117
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1):61–68, 1954. https://doi.org/10.1002/nav.3800010110
M. R. Garey, D. S. Johnson, "Strong" NP-Completeness Results: Motivation, Examples, and Implications, Journal of the ACM 25(3):499–508, 1978. https://doi.org/10.1145/322077.322090

8 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Flowshop and Jobshop Schedules: Complexity and Approximation 1: The Partition Flow Shop on Three Machines Has a Schedule of Finish Time 2T, Preemptive or Not, Iff a Partition ExistsResearch Paper

Motivation

Shop scheduling asks how to process a set of jobs, each a sequence of tasks on prescribed machines, so that all work is completed as early as possible. The flow shop, in which every job visits the machines in the same order, is the most studied of these models in operations research. For two machines, Johnson's rule (1954) computes a schedule of minimum finish time in $O(n\log n)$ time, and for two machines allowing interruptions (preemption) does not help. Garey, Johnson and Sethi (Math. Oper. Res. 1976) and Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum report BW 43/75, 1975; Ann. Discrete Math. 1977) showed that the non-preemptive problem becomes NP-complete with three machines.

Gonzalez and Sahni (Operations Research, 1978) extended this picture to preemptive schedules. Their Theorem 1 shows that minimizing the finish time of a three-machine flow shop is NP-complete with or without preemption, even when every job has at most two tasks of nonzero length. When every job has only one task the problem is trivial, so this is the simplest NP-complete case of the flow-shop finish-time problem. The result explains why no exact polynomial algorithm is expected and motivates the approximation results in the second half of the same paper.

Timeline:

1954: Johnson, two-machine flow shop, optimal non-preemptive rule.
1975: Brucker, Lenstra, Rinnooy Kan: non-preemptive three-machine flow shop NP-complete, including the case of two nonzero tasks per job (the paper's Corollary 1, which it says "is also obtained in [1]").
1976: Garey, Johnson, Sethi: non-preemptive three-machine flow shop NP-complete even when the problem size is the sum of the task lengths.
1978: Gonzalez, Sahni: the preemptive three-machine flow shop is NP-complete, by a reduction from PARTITION that also covers the non-preemptive case with two nonzero tasks per job.

Setting

A flow shop has $m\ge1$ processors $P_1,\dots,P_m$ and a finite set of jobs. Task $j$ of job $i$ must be processed on $P_j$ for $t_{j,i}\ge 0$ time units, and it can start only after task $j-1$ of the same job is completed. Task times may be zero. The schedule starts at time $0$ .

A preemptive schedule gives every task a finite set of pieces $(s,f)$ with $0\le s<f$ : the task is processed on its processor during $[s,f)$ . Pieces on the same processor do not overlap, the pieces of a task have total length $t_{j,i}$ , and every piece of a task starts after every piece of the earlier tasks of the same job has ended. A non-preemptive schedule processes every task in at most one piece. For a schedule $S$ , $f_i(S)$ is the time at which job $i$ is completed and the finish time is $\mathrm{FT}(S)=\max_i f_i(S)$ .

PARTITION. A multiset $S=\{a_1,\dots,a_n\}$ of nonnegative integers has a partition if some set $u$ of indices satisfies $\sum_{i\in u}a_i=\tfrac12\sum_{i=1}^n a_i$ .

The instance FS. With $T=\sum_i a_i$ , the flow shop $\mathrm{FS}$ has $m=3$ processors and $n+2$ jobs:

t_{\cdot,i}=(a_i,0,a_i)\ (1\le i\le n),\qquad t_{\cdot,n+1}=(T/2,\,T,\,0),\qquad t_{\cdot,n+2}=(0,\,T,\,T/2),

and the threshold is $\tau=2T$ . Every job has at most two nonzero tasks.

Formalization targets

Goal: Theorem 1 (p. 38)

For every $n$ and every $a_1,\dots,a_n\in\mathbb N$ :

\mathrm{FS}\ \text{has at most two nonzero tasks per job},

\big(\exists\,S'\ \text{preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition},

\big(\exists\,S'\ \text{non-preemptive},\ \mathrm{FT}(S')\le 2T\big)\iff S\ \text{has a partition}.

Milestones

Lemma 1(a) (p. 39): a partition of $S$ yields a non-preemptive schedule of FS with $\mathrm{FT}=2T$ (Figure 1).
Observations (i)–(ii) (p. 39): in any preemptive schedule with $\mathrm{FT}\le 2T$ , task $t_{1,n+1}$ ends by $T$ and task $t_{3,n+2}$ starts no earlier than $T$ .
Lemma 1(b) (p. 39): if $S$ has no partition, every preemptive schedule of FS has $\mathrm{FT}>2T$ .
Lemma 1 (p. 38): the preemptive equivalence.
Corollary 1 (p. 39): the non-preemptive equivalence.

Significance

The result. The equivalence shows that a polynomial-time algorithm deciding whether a three-machine flow shop (with two nonzero tasks per job) has a schedule of finish time at most $\tau$ , preemptive or not, would decide PARTITION in polynomial time. With membership in NP (the paper's Lemma 2) it gives NP-completeness of both versions. It also marks the boundary with the polynomial cases: $m=2$ (Johnson's rule), and jobs with a single task.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no machine-checked proof of this reduction exists, and the platform has no formal model of preemptive shop schedules. The mission produces one: a piece-based preemptive schedule with zero task times, which subsumes the non-preemptive case, together with the first formal NP-hardness reduction for preemptive flow shops on the platform.

Difficulty

Direction (a) asks for one explicit schedule. Direction (b) must rule out every preemptive schedule of FS, and preemption is exactly what makes this delicate: a task may be split into any finite number of pieces placed anywhere on its processor, so the naive intuition that a failed partition leaves "unusable gaps" is no longer evident, since pieces of different jobs can be interleaved to fill gaps. A correct argument must therefore be an accounting of processor time over the pieces, valid for any number and position of pieces, and it must treat zero-length tasks, which occupy no processor time but still delay the next task of their job. Finally, the non-preemptive equivalence is not a formal consequence of the preemptive one alone: it uses that (a) produces a non-preemptive schedule and that (b) holds for all preemptive schedules, which include the non-preemptive ones.

Formalization scope

Processors are Fin 3 ( $P_1,P_2,P_3$ = 0, 1, 2), jobs of FS are Fin n ⊕ Fin 2 (Sum.inr 0 is job $n+1$ , Sum.inr 1 is job $n+2$ ). Task times are real numbers; the PARTITION data are a : Fin n → ℕ, and "has a partition" is $2\sum_{i\in u}a_i=\sum_i a_i$ in $\mathbb N$ .
A schedule is a Finset of pieces $(s,f)$ per task with the four conditions of the Setting. Non-preemptive means at most one piece per task. Zero tasks have no pieces and occupy no processor time. $f_i(S)$ and $\mathrm{FT}(S)$ are maxima with baseline $0$ .
Explicit constants: $T=\sum_i a_i$ , the times $T/2$ and $T$ of jobs $n+1,n+2$ , and the threshold $\tau=2T$ , as on p. 39. Lemma 1(a) states finish time exactly $2T$ , as the paper does.
Not formalized: "NP-complete", the reducibility relation " $\alpha$ ", membership in NP (Lemma 2, p. 40) and the polynomial computability of FS from $S$ . The paper states Theorem 1, Lemma 1 and Corollary 1 as complexity claims. Their proofs establish the equivalences above for the constructed instance, and those equivalences are what is formalized.
No trivializing reading is admitted: the statements concern the specific instance FS built from $a$ , not an arbitrary flow shop, and the schedule model rules out overlapping pieces and out-of-order tasks while still allowing zero tasks. A sorry-free check confirms that Figure 1 is a valid non-preemptive schedule of FS for $S=\{1,1\}$ .
Reusable beyond this mission: the flow-shop model with preemptive pieces, and PARTITION. Proofs of the milestones and a proof of the goal from them are welcome.

Selected references

T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
M. R. Garey, D. S. Johnson, R. Sethi, The Complexity of Flowshop and Jobshop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum report BW 43/75, 1975; Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Bounds on Multiprocessing Timing Anomalies 1: Changing the List, Relaxing the Order, Shortening the Tasks and Using n′ Processors Multiplies the Finishing Time by at Most 1 + (n − 1)/n′Research Paper

Motivation

Scheduling work on several identical processors creates a plausible expectation: completing tasks sooner, removing constraints, or adding a processor should not delay the overall finish. A fixed priority-list rule defeats that expectation. When a task becomes ready earlier, it can occupy a processor that would otherwise have run another task; that decision changes later availability. Graham gives explicit schedules in which changing only the list raises the finishing time from 12 to 14, removing two precedence constraints raises it to 16, shortening every task raises it to 13, or adding one processor raises it to 15. These examples establish that the effect is a property of the scheduling rule, rather than of a change in the total set of tasks. See Graham, §2, pp. 417–419.

This mission concerns the upper limit of that effect. An operations researcher comparing a list schedule before and after a change in available processors or task data needs a bound that survives all four changes at once. The result is also a compact benchmark for formalizing algorithms whose behavior depends on changing availability: the model must describe when tasks become ready, when processors are idle, and which ready task a processor takes next. Graham's Theorem 1, proved in the 1969 paper, supplies the bound.

Setting

There are $r$ tasks $T_1,\ldots,T_r$ and $n$ identical processors. Each task $T_j$ has a positive processing time $\mu(T_j)$ . A strict precedence order $\prec$ specifies tasks that must be completed first: $T_i\prec T_j$ means $T_j$ cannot start before $T_i$ ends. A priority list $L$ orders all tasks once each. It may place a successor before a predecessor, because the processor skips any task that is not ready. These conventions are those of Graham's system in §2, p. 416.

A schedule gives each task a processor and a start time $S_j\ge0$ . Once started, the task occupies that processor continuously on $[S_j,S_j+\mu(T_j))$ . Two tasks on one processor cannot overlap, while tasks may meet at an endpoint. Precedence means $S_i+\mu(T_i)\le S_j$ whenever $T_i\prec T_j$ . The finishing time $\omega$ is the largest completion time $S_j+\mu(T_j)$ . The paper's list rule starts the first currently ready task in $L$ whenever a processor can take a task. A ready task that has not started cannot coexist with an idle processor. If one task starts while another ready task waits, the started task is earlier in $L$ .

The same task set is run a second time, with processing times $\mu'$ , order $\prec'$ , list $L'$ , processor count $n'$ , and finishing time $\omega'$ . The data satisfy $\mu'(T_j)\le\mu(T_j)$ for every $j$ and $\prec'\subseteq\prec$ . Thus the second run may have shorter tasks and fewer precedence relations; both lists may differ arbitrarily. Both runs obey the same list-scheduling rule Graham, §3, p. 419.

Formalization targets

General anomaly bound

For $r,n,n'\ge1$ , positive processing times in both runs, and the two list schedules just described, the target is Graham's Theorem 1:

\frac{\omega'}{\omega}\le 1+\frac{n-1}{n'}.

The numerator and denominator refer to the actual runs, with potentially different lists and processor counts. The conclusion does not require the new schedule to finish earlier. Its factor permits the anomalies shown in §2 while preventing an arbitrarily large increase for fixed $n,n'$ . The supporting targets follow the proof's numbered displays: a precedence chain covering idle times in the second run (1), an idle-time estimate for that chain (2), a comparison of its length with the first run (3)–(4), and the work-volume bound used in (5) Graham, pp. 419–420.

Significance

The theorem places a quantitative limit on the damage caused by a list rule after simultaneous changes in task durations, precedence, ordering, and capacity. When $n'=n$ , the factor is $2-1/n$ ; when the first run has one processor, it is $1$ . The statement applies to every finite task set and every pair of lists, so it can be reused when a scheduling method produces a list without additional structural guarantees. Graham states that the bound is best possible, citing earlier examples; this mission formalizes the inequality in this paper and does not claim to formalize those external examples Graham, p. 420.

The result is proved in the source paper. The work here is to give its objects precise Lean definitions and to supply machine-checked proofs of the bound and its supporting claims. A formal development needs to account for continuous real start times, processor assignments, half-open execution intervals, and the behavior of the list rule when several tasks or processors become available together. The resulting model of a nonpreemptive list schedule and the basic volume and chain estimates can serve later formalizations of parallel scheduling. The present proposal contains statements and definitions; its theorem bodies are open proof obligations.

Difficulty

Total work alone does not control the anomaly: processors can be idle while precedence keeps available work from starting, and changing precedence can alter which tasks occupy the processors later. A direct comparison of corresponding task completion times between the two runs also fails in Graham's §2 examples. The central difficulty is expressing the second run's idle periods through work on a single precedence chain and then relating that chain to the first run's finishing time. In Lean, the chain and the time intervals must be represented without silently changing endpoint conventions or treating a ready but unstarted task as running.

Formalization scope

Tasks are Fin r and processors are Fin n, with zero-based Lean indices corresponding to Graham's one-based subscripts. Processing times and start times are real. A priority list is a bijection between positions and tasks, so it contains every task exactly once and need not respect precedence. The order is strict. Feasible schedules are nonpreemptive and use half-open running intervals. The finishing time is a finite maximum of completion times; for no tasks it is defined as zero, while the ratio theorem assumes $r>0$ so its denominator is positive. Both processor counts are positive. The strict positivity of both time functions is inherited from the paper's $\mu:T\to(0,\infty)$ convention.

The model captures Graham's rule by no unforced idleness and list priority. It does not encode the smaller-index tie rule for identical processors, since the tie affects only processor labels and not start times or $\omega$ . The covering-chain milestone represents Graham's set $B$ as times before $\omega'$ when not all processors are busy; all-idle times before the finish cannot occur under the list rule. The idle-time milestone writes the total duration of empty tasks as $n'\omega'-\sum_j\mu'(T_j)$ using display (5). Natural-number subtraction is not used in the constants: $n-1$ and $n'-1$ are real differences. The companion existence statement and a concrete two-task sanity check rule out a vacuous list-schedule predicate. Contributions can address that existence theorem, the chain construction, interval accounting, the volume bound, and the final ratio.

Selected references

R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

7 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Bounds on Multiprocessing Timing Anomalies 2: Scheduling the k Longest Independent Tasks Optimally First Gives ω(k)/ω₀ ≤ 1 + (1 − 1/n)/(1 + ⌊k/n⌋)Research Paper

Motivation

Parallel processing poses a basic allocation question: given tasks of known lengths and several identical processors, how much time is lost when tasks are assigned by a simple list rule instead of an optimal allocation? The finishing time is the moment the last processor completes its work. For independent tasks, a list rule starts each next task on a processor that becomes free first. Such a rule is easy to execute, but the resulting allocation can be worse than the best partition of tasks among processors. Graham's 1969 paper studies precise worst-case ratios for this model. Its Theorem 3 asks what guarantee follows when the first $k$ tasks of the list are chosen among the longest and scheduled optimally before the remaining tasks are appended.

The paper also notes two endpoints of this family. With $k=0$ , the rule is ordinary list scheduling and has ratio at most $2-1/n$ . With $k=n$ , the $n$ longest tasks can start one per processor, giving ratio at most $3/2-1/(2n)$ . Theorem 3 expresses these as instances of one bound, including the integer jump at each multiple of $n$ Graham, pp. 427–428.

Setting

There are $r>0$ independent tasks, indexed by $jin\{0,\ldots,r-1\}$ , and $n>0$ identical processors, indexed by $p\in\{0,\ldots,n-1\}$ . Task $j$ takes a strictly positive time $\mu_j$ . A priority list $L$ contains every task exactly once. Its first $k$ tasks are $k$ of the longest tasks; equal lengths may be ordered either way. As a processor becomes available, it takes the next task in the list. Once started, a task runs without interruption. With no precedence constraints, every unstarted task is ready, so a processor runs its assigned tasks consecutively from time zero.

An assignment $\sigma$ records the processor that executes each task. The load $\ell_p(\sigma)$ of processor $p$ is the sum of its assigned task lengths. The finishing time is the largest load, $\omega(k)=\max_p\ell_p(\sigma)$ . For a list assignment, each task is assigned to a processor whose load from earlier list tasks is smallest at that step. If two processors are tied, either can be selected without changing the finishing time. For any assignment $\tau$ , let $\omega_k(\tau)$ be the largest load contributed by only the first $k$ list tasks. The algorithm requires its own first $k$ assignments to minimize $\omega_k(\tau)$ over all assignments $\tau$ ; the remaining tasks may occur in any list order.

Write $\omega_0$ for the smallest finishing time achievable for all $r$ tasks. The paper introduces it as the minimum over possible lists and later describes the same problem as minimizing the largest part sum over partitions of the task lengths Graham, pp. 421, 428. The formalization uses the partition or assignment form of $\omega_0$ .

Formalization targets

Theorem 3

For $0\le k\le r$ , when the first $k$ longest tasks have an optimal prefix schedule, Graham's bound is

\frac{\omega(k)}{\omega_0} \le 1+\frac{1-1/n}{1+\lfloor k/n\rfloor}.

Here $\lfloor k/n\rfloor$ is the greatest integer at most $k/n$ . The theorem also says the bound is best possible when $k$ is divisible by $n$ Graham, Theorem 3, p. 427. The equality examples are a separate companion statement in this mission.

Source milestones

The milestones state the finite-volume lower bound on $\omega_0$ , the case in which completing all tasks takes no longer than completing the first $k$ , and the paper's numbered inequalities (14), (15), and (16). They use $\alpha^*$ for the greatest task length after the first $k$ positions. These are individual mathematical claims from the proof on p. 427, with their original wording and formulas recorded alongside the formal statements.

Significance

The theorem gives a quantitative tradeoff between work spent optimizing a prefix and the worst-case finishing time of the full list. Its denominator is $1+\lfloor k/n\rfloor$ , so the guarantee improves when the optimized prefix contains another full processor's worth of long tasks. The example at multiples of $n$ shows that the stated coefficient cannot be uniformly reduced for the algorithm as specified Graham, p. 427.

The result is proved in the paper. This mission's remaining work is a machine-checked proof of its exact statement and the source's intermediate inequalities. The published identical-machine makespan definition is reused, while the list-assignment rule, optimal prefix, and longest-remaining-task quantity are made explicit here. Those definitions can also support later work on list scheduling without precedence constraints. No machine-checked proof of Theorem 3 is claimed by this proposal.

Difficulty

An optimal schedule for the first $k$ long tasks does not make the entire list optimal: short tasks appended later can affect which processor finishes last. A bound based only on average total work ignores this final imbalance; a bound based only on the largest remaining task ignores how many long tasks every assignment must place together. The proof must relate both constraints to one finishing time while preserving the floor $\lfloor k/n\rfloor$ . Replacing that floor with the real quotient changes the claim, and allowing an arbitrary prefix arrangement loses the algorithm's required optimality.

Formalization scope

Tasks and processors are finite indexed sets Fin r and Fin n; their zero-based indices correspond to the paper's one-based $T_j$ and $P_i$ . Task lengths are positive real numbers, and both $r$ and $n$ are positive. The list is a permutation, not merely a sequence that might omit or repeat a task. The condition $k\le r$ is explicit because choosing $k$ tasks from $r$ requires it; the paper treats $r>k$ inside the proof and the case $k=r$ is covered by the theorem. There is no precedence relation in this mission.

The list rule is a predicate on assignments: each next task goes to a processor with least current load. It omits the paper's smaller-index tie convention, since tied identical processors can be interchanged without changing the finishing time. The first $k$ positions must contain $k$ longest tasks, and their assignment must minimize the prefix finishing time among all assignments of those tasks. Those conditions are part of the goal; the inequalities (14)–(16) are conclusions to establish, not assumptions of the goal. A separate existence statement and a checked concrete instance ensure the list predicate is satisfiable.

All maxima and minima range over finite nonempty processor or assignment sets. The optimum is a minimum over assignments, equivalent to the paper's minimum over lists in the independent-task model. The quantity $\alpha^*$ is the largest duration outside the prefix when $k<r$ , and is defined as zero when none remains; statements using it require $k<r$ . Division is by $n>0$ and by $\omega_0>0$ . Lean's natural-number quotient represents $\lfloor k/n\rfloor$ ; real subtraction is used for coefficients such as $n-1$ . Contributions toward the finite load identities, the optimum-over-lists equivalence, and proofs of the listed bounds are within scope.

Selected references

R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

8 thms2 active usersReviewed

Completed

Combinatorics·Captain: marwahaha

Truly Subquadratic 3SUM on a Word RAMResearch Paper

3SUM asks whether three distinct positions in a list of integers contain values summing to zero. It is a central problem in fine-grained complexity.

This mission formalizes a deterministic $O(n^{1.9992})$ algorithm for 3SUM on $n$ polynomially bounded integers, on a word RAM with $O(\log n)$ -bit words. Alman and Vassilevska Williams's 2026 breakthrough gives a truly subquadratic bound, refuting the integer 3SUM hypothesis in this model.

The mission uses the accompanying Lean specification and shares the Exact Triangle milestone with Truly Subcubic APSP on a Word RAM.

References

Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026, Theorem 22.
Anthropic, formal-math / 3sum-apsp: accompanying Lean formalization, Theorem_22_3SUM.

51 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Fibonacci Heaps and Their Uses in Improved Network Optimization Algorithms: O(log n) Amortized Time for Delete Min and Delete, O(1) for Every Other F-Heap OperationResearch Paper

Why priority queues with cheap decrease key matter

Many network optimization algorithms spend most of their time in a heap (priority queue): a set of items with real keys that supports inserting an item, finding and deleting an item of minimum key, melding two heaps, decreasing the key of an item, and deleting an arbitrary item. Dijkstra's shortest-path algorithm performs at most one delete min per vertex and may perform a decrease key for each edge, so on a graph with $n$ vertices and $m$ edges its running time is governed by how cheap decrease key is. Binomial queues support the heap operations in $O(\log n)$ worst-case time.

Fredman and Tarjan (J. ACM 34 (1987)) introduced Fibonacci heaps (F-heaps), in which delete min and delete take $O(\log n)$ amortized time and every other operation, decrease key included, takes $O(1)$ amortized time. This brings Dijkstra's algorithm to $O(n \log n + m)$ and improves the best bounds then known for all-pairs shortest paths, weighted bipartite matching (the assignment problem) and minimum spanning trees. F-heaps descend from the binomial queues of Vuillemin (1978) and use the potential technique of amortized analysis of Sleator and Tarjan. This mission formalizes the paper's §2 analysis, culminating in THEOREM 1 on p. 604.

Setting

An F-heap is a list of heap-ordered rooted trees: every child's key is at least its parent's key. Each node holds an item, the item's real key and a mark bit; the children of a node are kept in the order in which they were linked to it, earliest first. The rank $r(x)$ of a node is its number of children. A collection is a list of heaps, named by position; a run starts with no heaps.

Linking two trees with roots $x$ and $y$ makes $y$ the last child of $x$ if the key of $x$ is smaller, and otherwise makes $x$ the last child of $y$ ; the root that becomes a child is unmarked. The operations act as follows:

make heap adds an empty heap; find min acts on a nonempty heap and returns a root of minimum key; insert adds a one-node tree for a new item; meld concatenates two root lists.
delete min removes a root $x$ of minimum key, adds the children of $x$ to the roots, then repeats the linking step, "find any two trees whose roots have the same rank, and link them", in any order, until all root ranks are distinct.
decrease key $(\Delta, i, h)$ , $\Delta \ge 0$ , lowers the key of $i$ and, if the node $x$ of $i$ is not a root, cuts $x$ from its parent, making its subtree a new tree. delete $(i, h)$ cuts $x$ the same way, destroys it and adds its children to the roots; a minimum root is deleted as in delete min.
After every cut of a child of $p$ , if $p$ is not a root it is marked if unmarked and cut from its own parent if marked: a cascading cut, which may repeat upwards.

The actual time of an operation is one unit, plus one per linking step, plus one per cut, plus for delete min the scan of the rank array (the largest rank involved). The potential $\Phi$ of a collection is the number of trees plus twice the number of marked nonroot nodes, and the amortized time of an operation is its actual time plus the increase of $\Phi$ .

Formalization targets

Goal: THEOREM 1 (p. 604)

There is an absolute constant $C > 0$ such that for every sequence of $T$ operations started from no heaps, with $n_t$ the number of items in the heap that operation $t$ acts on, just before it acts,

\sum_{t<T} \mathrm{cost}_t \;\le\; \sum_{t<T} b_t, \qquad b_t = \begin{cases} C(\log_2 n_t + 1) & \text{delete min or delete},\\ C & \text{otherwise.}\end{cases}

The paper's wording is "the total time is at most the total amortized time, where the amortized time is $O(\log n)$ for each delete min or delete operation and $O(1)$ for each of the other operations"; the goal pins the $O(\cdot)$ to one constant and does not name the potential.

Milestones

LEMMA 1: the $i$ th child of a node, in linking order, has rank at least $i - 2$ .
$F_{k+2} \ge \varphi^k$ , with $F_k$ the Fibonacci numbers and $\varphi = (1+\sqrt5)/2$ .
COROLLARY 1: a node of rank $k$ has at least $F_{k+2} \ge \varphi^k$ descendants, itself included.
A node of rank $k$ in an $n$ -item heap has $\varphi^k \le n$ , hence $k \le \log n / \log\varphi$ .
make heap, find min and meld leave $\Phi$ unchanged; insert raises it by one.
delete min raises $\Phi$ by at most $\log n / \log \varphi$ minus the number of linking steps.
decrease key raises $\Phi$ by at most three minus the number of cascading cuts.
From no heaps, the total amortized time bounds the total actual time.

Significance

THEOREM 1 is the data-structure fact behind the paper's algorithmic results: Dijkstra's algorithm in $O(n\log n + m)$ , all-pairs shortest paths and the assignment problem in $O(n^2 \log n + nm)$ , and minimum spanning trees in $O(m\,\beta(m,n))$ .

The result has been proved since 1987. What the mission adds is a machine-checked version of the paper's own analysis on an operational model with arbitrary linking order, unmarking on link, marking or cascading on every cut, and the paper's unit costs. The proposal states the theorem and its supporting claims; their proofs remain to be formalized.

Difficulty

The obvious argument, that every tree is a binomial tree and so every rank is at most $\log_2 n$ , fails as soon as cuts are allowed: decrease key and delete remove subtrees arbitrarily, and the trees of an F-heap need not be binomial. The rank bound has to come from an invariant of the whole history (LEMMA 1), which only holds because a node loses at most one child before it is cut itself; without cascading cuts a node of rank $k$ can be left with only $k+1$ descendants, and no logarithmic rank bound holds. A second difficulty is that the actual cost of one decrease key is unbounded, since a single operation may trigger arbitrarily many cascading cuts; a per-operation worst-case argument cannot give THEOREM 1, and the bound holds only for whole sequences started from no heaps.

Formalization scope

All declarations sit in the namespace FibHeap.Amort. Trees are a nested inductive FTree with item ℕ, key ℝ, a mark bit and a list of children in linking order; a heap is List FTree (its roots) and a collection is List Heap. Operations are a step relation Step s op s' d whose data d records linking steps, cuts, cascading cuts and the scan, so that cost d = 1 + links + cuts + scan is determined by what the operation did. The linking loop allows every order of linking; a link tie makes the first root a child of the second, while delete min may choose any minimum-key root. Runs start from no heaps; reachable collections consist of heap-ordered trees with each item in at most one heap. LEMMA 1, COROLLARY 1 and the delete-min bound are stated for reachable collections only, as the paper's "a node in an F-heap" intends. The paper's standing assumption that an item is in only one heap at a time is enforced by the precondition of insert and is not a hypothesis. The minimum pointer and returned items are not stored in the step relation; find min is a state-preserving step charged one unit. A heap destroyed by meld remains as an empty heap at its index.

Logarithms in the goal are base 2 (footnote 1, p. 600), with a $+1$ so that one-item heaps have positive budget. The paper's constant " $\le 1.4404 \log n$ " on p. 604 is a rounding slip ( $1/\log_2 \varphi = 1.44042\ldots$ ); milestones use the exact $\log_\varphi n$ .

The goal is not trivialized: the cost counts every linking step and every cut as fixed by the step relation, $C$ is quantified before the run, and a companion theorem (step_exists) shows that every valid operation can be performed, so runs containing delete min, decrease key and cascading cuts exist. A further supporting statement gives an explicit form of the delete potential bound. A complete development needs facts about the nested inductive (sizes, subtree lists, marked counts under list edits), an invariant for LEMMA 1 recording when each child was linked, and the Fibonacci inequality; contributions of any of these as separate lemmas are welcome.

Selected references

M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, J. ACM 34(3):596–615, 1987. https://doi.org/10.1145/28869.28874
J. Vuillemin, A data structure for manipulating priority queues, Comm. ACM 21(4):309–315, 1978. https://doi.org/10.1145/359460.359478
R. E. Tarjan, Amortized computational complexity, SIAM J. Algebraic Discrete Methods 6(2):306–318, 1985. https://doi.org/10.1137/0606031
E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1:269–271, 1959. https://doi.org/10.1007/BF01386390

10 thms2 active usersReviewed

Completed

Combinatorics·Captain: wurtle

Truly Subcubic APSP on a Word RAMResearch Paper

All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph. It is a fundamental problem in graph algorithms and a fundamental problem in fine-grained complexity.

This mission formalizes a deterministic $O(n^{2.99942})$ algorithm for APSP on directed $n$ -vertex graphs with polynomially bounded integer edge weights and no negative cycles, on a word RAM with $O(\log n)$ -bit words. This is a truly subcubic bound and refutes the integer-weight APSP hypothesis in this model.

References:

Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026, Theorem 22.
Anthropic, formal-math / 3sum-apsp: accompanying Lean formalization, Theorem_22_APSP.

51 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 3: On the 3-Dimensional Matching Instances, a Schedule within ρ < 3/2 of Optimal Has Makespan ≤ 2 Iff a Matching ExistsResearch Paper

Motivation

Minimum makespan scheduling on unrelated parallel machines, written $R\,||\,C_{\max}$ , is one of the basic models of scheduling theory: $n$ jobs must each be run on one of $m$ machines, and the time a job takes depends arbitrarily on the machine. Lenstra, Shmoys and Tardos (CWI Report OS-R8714, 1987; journal version Math. Programming 46, 1990) gave a polynomial 2-approximation algorithm for this problem and, in the same paper, a matching limit from below: no polynomial algorithm can guarantee a factor smaller than $3/2$ unless $P = NP$ (their Corollary 2).

The two bounds have stood for more than three decades. Closing the gap between $3/2$ and $2$ for $R\,||\,C_{\max}$ is listed among the central open problems of approximation algorithms (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, open problem on unrelated machines; Schuurman and Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 1999). The lower bound of $3/2$ is the subject of this mission.

Timeline:

1979: Graham, Lawler, Lenstra and Rinnooy Kan introduce the classification $R\,||\,C_{\max}$ .
1987/1990: Lenstra, Shmoys and Tardos prove NP-completeness of deciding makespan at most 3 (Theorem 4, giving the bound $4/3$ ) and at most 2 (Theorem 5, giving $3/2$ ), both by reduction from 3-dimensional matching.
Since then: the $3/2$ hardness bound has not been improved for general $R\,||\,C_{\max}$ ; progress has concentrated on special cases such as the restricted-assignment problem.

Setting

3-dimensional matching. There are three disjoint sets $A = \{a_1,\dots,a_n\}$ , $B = \{b_1,\dots,b_n\}$ , $C = \{c_1,\dots,c_n\}$ and a family $F = \{T_1,\dots,T_m\}$ of triples, each with one element of $A$ , one of $B$ and one of $C$ . A matching is a subfamily $F'$ with $|F'| = n$ whose union is $A \cup B \cup C$ . In Lean an instance is a map $T : \mathrm{Fin}\,m \to \mathrm{Fin}\,n \times \mathrm{Fin}\,n \times \mathrm{Fin}\,n$ , and HasMatching T says that a matching exists.

The scheduling model. Machines are $\mathrm{Fin}\,m$ , jobs are $\mathrm{Fin}\,N$ , and $p_{ij}$ is the positive integer processing time of job $j$ on machine $i$ . A schedule $\sigma$ assigns each job to one machine; the load of machine $i$ is $\sum_{j:\sigma(j)=i} p_{ij}$ and the makespan $C_{\max}(\sigma)$ is the largest load. These are the published definitions MatousekLP.Scheduling.load and makespan.

The instance of Theorem 5. The triples containing $a_j$ are the triples of type $j$ ; let $t_j$ be their number. From $T$ the paper builds a scheduling instance with $m$ machines, machine $i$ corresponding to $T_i$ , and with

$2n$ element jobs, one for each $b_k$ and each $c_l$ ;
$t_j - 1$ dummy jobs of type $j$ , for each $j$ .

If $T_i = (a_j, b_k, c_l)$ , machine $i$ processes the element jobs of $b_k$ and $c_l$ in time $1$ , each dummy job of type $j$ in time $2$ , and every other job in time $3$ . In Lean the processing-time matrix is P T.

A $\rho$ -approximate schedule of an instance is a schedule $\sigma$ with $C_{\max}(\sigma) \le \rho\, C_{\max}(\tau)$ for every schedule $\tau$ of the same instance.

Formalization targets

Goal: Corollary 2 (p. 8)

For every instance $T$ , every $\rho < 3/2$ , and every $\rho$ -approximate schedule $\sigma$ of the instance of Theorem 5 built from $T$ ,

C_{\max}(\sigma) \le 2 \iff T \text{ has a matching}.

This is the mathematical content of "for every $\rho < 3/2$ there is no polynomial $\rho$ -approximation algorithm unless $P = NP$ ": a $\rho$ -approximate answer on the reduced instance decides 3-dimensional matching.

Theorem 5 (p. 7)

For every instance $T$ ,

\exists\,\sigma:\ C_{\max}(\sigma) \le 2 \iff T \text{ has a matching}.

Milestones from the proof of Theorem 5 (pp. 7–8)

If every $t_j \ge 1$ , then $\sum_j (t_j - 1) + n = m$ : there are $m - n$ dummy jobs.
A matching yields a schedule with makespan at most $2$ .
A schedule with makespan at most $2$ yields a matching.

Significance

The result. Theorem 5 shows that $R\,||\,C_{\max}$ is NP-hard already when every processing time lies in $\{1,2,3\}$ and the target makespan is $2$ . Corollary 2 turns this into the best known inapproximability bound for the problem, $3/2$ , which sits opposite the paper's own factor-2 algorithm. The same reduction pattern (machines as triples, dummy jobs that pin machines down) is reused in many later hardness proofs for scheduling and assignment problems.

Formalizing it. The result is proved on paper; no machine-checked version is known to exist. A formal proof requires the full combinatorial argument behind the reduction, including the counting of machines per type and the case where some element of $A$ lies in no triple, which the paper does not discuss. Together with mission 1 of this series (the factor-2 algorithm), it fixes both ends of the $[3/2, 2]$ gap in one formal library.

Difficulty

The construction is short, but the converse direction carries the weight: from an arbitrary schedule with makespan at most $2$ one must recover a matching, although nothing in the schedule singles out the triples that form it. The obvious first idea, to read the matching off the machines that receive unit-time jobs, fails as it stands: a machine may receive one unit-time job or none, and the argument must exclude this for every schedule, including the degenerate instances in which some $a_j$ lies in no triple or triples repeat. For Corollary 2, the passage from the real-valued approximation guarantee to the threshold $2$ depends on the strict inequality $\rho < 3/2$ ; at $\rho = 3/2$ the statement is no longer implied by Theorem 5.

Formalization scope

Machines are Fin m; 3DM elements are Fin n; a 3DM instance is T : Fin m → Fin n × Fin n × Fin n, so a triple may repeat. A matching is a set of $n$ triple indices covering every $a_j$ , $b_k$ , $c_l$ (the covering form of the paper's definition, which forces disjointness).
The jobs of the reduced instance are the sum type $\mathrm{Fin}\,n \oplus \mathrm{Fin}\,n \oplus \Sigma_j\,\mathrm{Fin}(t_j - 1)$ . They are enumerated by a fixed bijection with $\mathrm{Fin}\,N$ so that the published MatousekLP.Scheduling.makespan applies. All statements quantify over every schedule, so the choice of bijection is irrelevant.
$t_j - 1$ is natural-number subtraction. When some $t_j = 0$ (a case the paper leaves aside), type $j$ has no dummy job; the reduced instance then has neither a matching nor a schedule of makespan at most $2$ , so Theorem 5 and Corollary 2 hold as stated, with no hypothesis $t_j \ge 1$ . Only the dummy-count milestone assumes $t_j \ge 1$ .
Processing times are natural numbers cast to $\mathbb R$ ; makespans are real.
Not formalized: "polynomial" (running time of an algorithm and of the reduction), membership in NP, "NP-complete" and "unless $P = NP$ ". Theorem 5 is stated as the reduction's equivalence; Corollary 2 is stated as the fact that any $\rho$ -approximate schedule of the reduced instance, $\rho < 3/2$ , decides 3-dimensional matching. The reduction is evidently polynomial, but this is not stated.
The approximation hypothesis compares $\sigma$ with every schedule $\tau$ of the same reduced instance; a goal in which $\sigma$ is an arbitrary schedule, or is bounded against an unrelated quantity, would be a different statement. The strict inequality $\rho < 3/2$ is essential and kept.
Contributions welcome: proofs of the three milestones, of Theorem 5 from them, and of Corollary 2; reusable lemmas about integer-valued makespans and about sum-type job sets.

Selected references

J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (FOCS 1987); the version cited for every theorem number in this mission.
J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979 (3-dimensional matching, problem [SP1]).
P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, Journal of Scheduling 2 (1999) 203–213. https://doi.org/10.1002/(SICI)1099-1425(199909/10)2:5<203::AID-JOS26>3.0.CO;2-5
D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

8 thms2 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 4: With Times in {p, q} and gcd(p, q) = 1, a q-Dimensional Matching Exists Iff a Schedule Has Makespan ≤ pqResearch Paper

Motivation

Minimum makespan scheduling on unrelated parallel machines asks for an assignment of $n$ jobs to $m$ machines, where job $j$ takes $p_{ij}$ time units on machine $i$ , so that the largest machine load is as small as possible. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) it is $R\,\|\,C_{\max}$ . It models load balancing across heterogeneous processors, workers or production lines, and it is a standard test case for linear-programming rounding.

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714; Mathematical Programming 46, 1990) gave a polynomial 2-approximation algorithm for $R\,\|\,C_{\max}$ and showed that no polynomial algorithm achieves a ratio below $3/2$ unless P = NP. They also asked which restrictions on the processing times keep the problem hard. Their Section 5 answers this when only two distinct processing times occur:

all $p_{ij}=1$ : trivial;
all $p_{ij}\in\{1,\infty\}$ : bipartite cardinality matching;
all $p_{ij}\in\{1,2\}$ : polynomial by matching techniques (Theorem 6);
all $p_{ij}\in\{p,q\}$ with $p<q$ , $2p\ne q$ : NP-hard (Theorem 7).

Theorem 7 is the paper's last result and closes this classification. Its proof generalizes the reduction of Theorem 4, which handles the case $\{1,3\}$ , from 3-dimensional matching to $q$ -dimensional matching.

Setting

Machines are indexed by $i\in\{1,\dots,m\}$ and jobs by $j$ . A schedule $\sigma$ assigns every job to exactly one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$ , and the makespan $C_{\max}(\sigma)$ is the largest load.

$q$ -dimensional matching. An instance is a ground set $U$ of $qn$ elements and a family $S_1,\dots,S_m$ of $q$ -element subsets of $U$ . A matching is a subfamily $F'\subseteq\{1,\dots,m\}$ with $|F'|=n$ and $\bigcup_{i\in F'}S_i=U$ ; its members are then pairwise disjoint.

The instance of Theorem 7. Fix natural numbers $0<p<q$ that are relatively prime. Build a scheduling instance with $m$ machines, machine $i$ corresponding to $S_i$ , and two kinds of jobs:

$qn$ element jobs, one per $u\in U$ , with $p_{iu}=p$ if $u\in S_i$ and $p_{iu}=q$ otherwise;
$p(m-n)$ dummy jobs, each taking $q$ time units on every machine.

Every processing time lies in $\{p,q\}$ .

The instance of Theorem 4. For disjoint sets $A=\{a_1,\dots,a_n\}$ , $B$ , $C$ of the same size and triples $T_i=(a_j,b_k,c_l)$ , $i=1,\dots,m$ , there are $3n$ element jobs, one per element of $A\cup B\cup C$ , and $m-n$ dummy jobs. Machine $i$ processes the element jobs of $a_j$ , $b_k$ , $c_l$ in one time unit and every other job in three time units. A 3-dimensional matching is a subfamily of $n$ triples covering $A\cup B\cup C$ .

Formalization targets

Goal: Theorem 7 (p. 8; proof pp. 8–9)

For relatively prime $0<p<q$ and a family of $q$ -subsets $S_1,\dots,S_m$ of a $qn$ -element set, the instance above has all processing times in $\{p,q\}$ , and

\exists\,\sigma:\ C_{\max}(\sigma)\le pq \quad\Longleftrightarrow\quad \exists\,F'\subseteq\{1,\dots,m\}:\ |F'|=n,\ \bigcup_{i\in F'}S_i=U .

Milestones

Theorem 4 (p. 7): on the 3-dimensional matching instance with times in $\{1,3\}$ , a schedule with makespan at most $3$ exists iff a matching exists.
Matching gives a schedule (pp. 8–9): if $S$ has a matching, some schedule has $C_{\max}\le pq$ .
No idle time, two kinds of machine (p. 9): in every schedule with $C_{\max}\le pq$ , three things hold. Every load equals $pq$ . Every element job runs at length $p$ , on a machine whose tuple contains it. Each machine processes either exactly $q$ element jobs and no dummy job, or exactly $p$ dummy jobs and no element job.

Significance

The result. Theorems 6 and 7 together say exactly which two-valued restrictions of $R\,\|\,C_{\max}$ are tractable. Up to scaling, the polynomial case is $\{1,2\}$ , and every other pair $\{p,q\}$ with $p<q$ is NP-hard. Theorem 4 is the base case. It also yields Corollary 1 of the paper: no polynomial $\rho$ -approximation with $\rho<4/3$ exists unless P = NP. Reductions of this "no idle time" kind are a standard template for hardness of restricted-assignment and two-value scheduling, a line still active in the study of the restricted assignment problem and of the "graph balancing" special case.

Formalizing it. The result is proved, in two short paragraphs. The proof leaves to the reader the construction of the schedule from a matching and the "easy number theoretic argument" behind the converse, and both become explicit here. The development also produces reusable pieces: a $q$ -dimensional matching definition over an arbitrary family of $q$ -sets, and two reduction instances built on the published load and makespan of MatousekLP.Scheduling.Schedule. To our knowledge no machine-checked proof of these reductions exists.

Difficulty

The forward direction is a direct construction. The converse is where care is needed. A schedule with makespan at most $pq$ may a priori place an element job on a machine whose tuple does not contain it, at length $q$ , and may mix element and dummy jobs on one machine. Looking at one machine at a time does not exclude either: a single machine can carry such a mixed load below $pq$ . What excludes them is a property of the whole schedule together with the arithmetic of $p$ and $q$ . The hypotheses are sharp for this step: for $p>q$ element jobs are cheaper on foreign machines, and for $\gcd(p,q)>1$ a load $ap+bq=pq$ with $a,b>0$ becomes possible.

Formalization scope

Model. Machines are Fin m. Schedules are maps from jobs to machines. Load and makespan are those of the published MatousekLP.Scheduling.Schedule, with natural-number processing times cast to $\mathbb R$ . The jobs are enumerated as Fin (q * n + p * (m - n)) (Theorem 7) and Fin (3 * n + (m - n)) (Theorem 4), element jobs first, through finSumFinEquiv.
Ground set and family. The ground set is Fin (q * n) and the family is indexed by machines, so repeated tuples are allowed. The $q$ -partite structure of $q$ -dimensional matching is not imposed: the reduction does not use it, and statements over all families of $q$ -sets contain the $q$ -partite case. Theorem 4 keeps the tripartite structure, with triples of indices in Fin n × Fin n × Fin n.
Threshold. The thresholds are exactly $pq$ and $3$ , with "makespan at most".
Complexity wording not formalized. "NP-hard" (Theorem 7) and "NP-complete" (Theorem 4) are not formalized: membership in NP, polynomial size of the reductions, and the hardness of the matching problems are not stated. What is stated is the equivalence each reduction establishes.
Hypotheses. Theorem 7's goal assumes $0<p<q$ , $\gcd(p,q)=1$ and $|S_i|=q$ . The paper's general case $\gcd(p,q)=g>1$ is its stated "without loss of generality": divide all times by $g$ , which divides every makespan by $g$ . It is not part of the formal statement. The paper's hypothesis $2p\ne q$ is dropped because the reduction does not use it. With coprime $p<q$ it excludes only $(p,q)=(1,2)$ , where the equivalence still holds but the source problem is bipartite matching. The formal goal is therefore stronger than the paper's.
Edge cases. For $m<n$ , natural-number subtraction gives no dummy jobs; both sides of each equivalence are false when $n\ge1$ . This stands in for the paper's "trivial 'no' instance". For $n=0$ the empty family is a matching and the dummy jobs fill the machines exactly.
No trivialization. The goal is an equivalence about a constructed instance whose processing times are given by explicit definitions. Neither side is assumed, the schedule is quantified over all maps from jobs to machines, and the instance is not a free parameter pinned by hypotheses.
Welcome contributions. Besides the milestones: counting lemmas relating a machine's load to the numbers of jobs of each length on it, and lemmas on the makespan of MatousekLP.Scheduling.Schedule (it bounds every load; it is attained when $m\ge1$ ), which are reusable across scheduling reductions.

Selected references

J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Amsterdam, 1987 (the version formalized here); journal version in Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979 (3-dimensional matching, problem SP1).
R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3 (the schedule, load and makespan definitions reused here). https://doi.org/10.1007/978-3-540-30717-4

7 thms2 active usersReviewed

Combinatorics Operations Research Probability·Captain: mikedeng1

An Optimal Algorithm for On-line Bipartite Matching 2: No Randomized On-line Algorithm Guarantees an Expected Matching Larger Than n(1 − 1/e) + o(n)Research Paper

Motivation

An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of $1-1/e$ for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).

The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.

Setting

There are $n$ boys, represented by rows, and $n$ girls, represented by columns. A bipartite graph $G\subseteq[n]\times[n]$ records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of $G$ . This assumption supplies an offline benchmark of $n$ matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.

Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order $n,n-1,\ldots,1$ . A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance $p(A)$ is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).

The paper's hard family begins with the complete upper-triangular graph $T_n$ , where row $i$ is adjacent to column $j$ exactly when $i\le j$ . Its columns arrive from largest to smallest. Relabeling the rows by a permutation $\pi$ gives an instance $T_\pi$ that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write $V_{T_n}(n,\varnothing)$ for RANDOM's expected number of matches on $T_n$ , beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).

Formalization targets

Main theorem

For every $\varepsilon>0$ , there is one threshold $N$ such that, for every $n\ge N$ and every randomized online algorithm $A$ on $n$ rows and columns, a graph $G$ with a perfect matching satisfies

\mathbb E_A[|M(G)|]\le (1-e^{-1}+\varepsilon)n.

The threshold is uniform over algorithms. The graph may depend on $A$ . This is the quantified upper-bound reading of Theorem 2's $p(A)\le n(1-1/e)+o(n)$ (Karp, Vazirani, and Vazirani, 1990, Theorem 2).

Milestone statements

Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted $T_n$ with RANDOM's expected size on $T_n$ . Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit

\lim_{n\to\infty}\frac{V_{T_n}(n,\varnothing)}{n}=1-e^{-1}.

Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).

Significance

Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from $n$ is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.

Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.

Difficulty

For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the $o(n)$ claim in Lemma 16.

Formalization scope

Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order $n,\ldots,1$ is represented by zero-based order $n-1,\ldots,0$ ; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.

RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For $n=0$ , the matching and RANDOM value are zero; the main theorem is eventual in $n$ and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's $o(n)$ in Theorem 2 is stated as $\forall\varepsilon>0,\exists N,\forall n\ge N$ with $N$ before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.

Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.

Selected references

Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, pp. 352–358, 1990. DOI: 10.1145/100216.100262.

9 thms2 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments III: The Three Revenue-Ordered Approximation Bounds Are TightResearch Paper

Motivation

A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.

Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.

Timeline:

Talluri and van Ryzin (2004) showed that revenue-ordered assortments are optimal under the multinomial logit model.
Rusmevichientong, Shmoys, Tong and Topaloglu (2014) showed the problem NP-hard under a mixture of two logit models, and proved that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit.
Aouad, Farias, Levi and Segev (2018) proved an $\Omega(1/\ln(r_k/r_1))$ guarantee under random utility models, and that the assortment problem there is NP-hard to approximate within $\Omega(1/n^{1-\epsilon})$ and $\Omega(1/\log^{1-\epsilon}(r_k/r_1))$ .
Berbeglia and Joret (2016–2020, Algorithmica) proved the guarantees $1/k$ , $1/\sum_{i}(r_i-r_{i-1})/r_i\ge1/(1+\ln(r_k/r_1))$ and a purchase-probability bound under any regular model, and an instance on which all three, in their sum forms, are attained in the limit.

Setting

The products form a finite set $\mathcal C$ . A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$ , the probability $\mathcal P(x,S)$ that a customer buys $x$ . The no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ . The model is regular if

$\mathcal P(x,S)\ge0$ for $x\in\mathcal C\cup\{0\}$ ;
$\mathcal P(x,S)=0$ for $x\notin S$ ;
$\sum_{x\in S}\mathcal P(x,S)\le1$ ;
$\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$ .

Each product has a revenue $r(x)>0$ . Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$ , and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$ .

Let $r_1<\dots<r_k$ be the distinct revenues, with $r_0:=0$ , and $S_i=\{x: r(x)\ge r_i\}$ . The heuristic earns

\mathrm{RO}=\max_{i\in[k]}\mathrm{rev}(S_i).

For an optimal $S^*$ let $N_i=\sum_{x\in S^*,\,r(x)\ge r_i}\mathcal P(x,S^*)$ , $N_{k+1}=0$ , and $\ell$ the largest index with $N_\ell>0$ . Section 3 of the paper proves

(A) $\mathrm{OPT}\le k\cdot\mathrm{RO}$ (Theorem 3.1);
(B) $\mathrm{OPT}\le D_r\cdot\mathrm{RO}$ , with $D_r=\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\le 1+\ln(r_k/r_1)$ (Theorem 3.2);
(C) $\mathrm{OPT}\le D_N(S^*)\cdot\mathrm{RO}$ , with $D_N(S^*)=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le 1+\ln(N_1/N_\ell)$ (Theorem 3.3).

Formalization targets

Goal: Theorem 3.4

For every $k\ge1$ and every $\delta>0$ there are a finite nonempty product set, a regular $\mathcal P$ , revenues $r>0$ with exactly $k$ distinct values, and an optimal $S^*$ with $N_1>0$ , such that

k\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_r\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_N(S^*)\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT}.

So none of the bounds (A), (B), (C) stays true when multiplied by $1+\delta$ , for any number $k$ of distinct revenues.

The tight instance (milestones)

The paper's witness has products $(i,j)$ with $i\in[k]$ and $j\in[i]$ . Product $(i,j)$ has revenue $\varepsilon^{-j}$ , and $\mathcal P((i,j),S)=\varepsilon^i$ when $(i,j)\in S$ and $(i,1),\dots,(i,j-1)\notin S$ , and $0$ otherwise, for $0<\varepsilon\le\tfrac12$ . The milestones follow the proof on pp. 10–11:

the axiom (iii) bound;
(7);
(8);
(9);
regularity;
the distinct revenues $r_i=\varepsilon^{-i}$ ;
$\mathrm{RO}=\mathrm{rev}(\mathcal C)<1/(1-\varepsilon)$ ;
$\mathrm{OPT}=k$ , attained by $\{(i,i)\}$ ;
the limits $\mathrm{OPT}/\mathrm{RO}\to k$ and $D_r\to k$ ;
$N_i=\varepsilon^i+\dots+\varepsilon^k$ and $D_N\to k$ as $\varepsilon\to0^+$ .

Significance

With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters $k$ , $D_r$ and $D_N$ , revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.

On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.

Difficulty

The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:

the regularity of the instance at the no-purchase option, (9), which needs the row decomposition (8);
the claim that $\{(i,i)\}$ is optimal among all $2^{k(k+1)/2}$ offer sets, asserted without proof;
the claim that the full set is the best threshold set;
the evaluation of $D_N(S^*)$ , which needs $\ell=k$ .

The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly $k$ revenues on which all three bounds are nearly attained, for every $k$ .

Formalization scope

Products are an arbitrary finite type C. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. Offer sets are Finset C.
IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at $x=0$ is essential: without it the guarantees fail.
$\mathrm{OPT}$ is Finset.sup' over all subsets, including $\emptyset$ . $\mathrm{RO}$ is Finset.sup' over the $k$ threshold sets only, and needs Nonempty C.
The distinct revenues are the sorted image of r, indexed by Fin k from $0$ : the Lean index $i$ is the paper's $i+1$ , and $r_0=0$ is a separate case. $\ell$ lives in WithBot (Fin k).
Bounds are multiplicative ( $\mathrm{OPT}\le D\cdot\mathrm{RO}$ ); there is no ratio $\mathrm{RO}/\mathrm{OPT}$ in the goal. Limits are along 𝓝[>] 0.
The tight instance keeps the paper's 1-based pairs $(i,j)$ as a subtype of Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.

Ruled out:

a fixed $k$ , since "for every $k$ " is the content;
tightness of the logarithmic forms $1/(1+\ln(r_k/r_1))$ and $1/(1+\ln\nu)$ , which this instance does not show (there $1+\ln(r_k/r_1)\to\infty$ while $\mathrm{OPT}/\mathrm{RO}\to k$ ), so only the sum forms are claimed tight;
an instance whose regularity is assumed;
a heuristic maximizing over all subsets.

Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of $\{(i,i)\}$ , and general lemmas on sorted distinct values of a finite function.

Selected references

G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; published in Algorithmica, 2020. https://arxiv.org/abs/1606.01371
K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191
A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724

15 thms2 active usersReviewed

Theoretical Computer Science

Missions

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms II: Every Product Multicommodity Flow Problem with k Commodities Has Ω(𝒮/log k) ≤ f ≤ 𝒮Research Paper

Why multicommodity max-flow and min-cut

Setting

Formalization targets

Goal: Theorem 7 (pp. 801–802)

Milestones, in the order the proof uses them

Stronger companions

Significance

Difficulty

Formalization scope

Selected references

A Pseudorandom Generator from Any One-Way Function: One-Way Functions Exist If and Only If Pseudorandom Generators ExistResearch Paper

Motivation

Setting

Formalization targets

Main equivalence

Intermediate targets

Significance

Difficulty

Formalization scope

Selected references

A Theorem on Boolean Matrices: Warshall's Construction M* Equals the Boolean Sum M ∨ M² ∨ ⋯ ∨ Mᵈ of the Boolean Powers of MResearch Paper

Motivation

Setting

Formalization targets

Goal: the construction computes the power sum

Milestone 1 (Proved, referenced): the THEOREM

Milestone 2: footnote 2

Companion: footnote 3

Significance

Difficulty

Formalization scope

Selected references

Reaching Agreement in the Presence of Faults 3: With Authenticated Messages, the S_pq Procedure Assures Interactive Consistency for m Faults for Every n ≥ mResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Reaching Agreement in the Presence of Faults 2: If |V| ≥ 2 and 3 ≤ n ≤ 3m, No Family {F_p} Assures Interactive Consistency for m Faults, However Many Rounds Are UsedResearch Paper

Motivation

Setting

Formalization targets

Goal: the THEOREM of Section 4

Milestones, in the order the proof of the paper uses them

Significance

Difficulty

Formalization scope

Selected references

Reaching Agreement in the Presence of Faults 1: With n ≥ 3m + 1 Processors, the Recursive Majority Procedure on (m + 1)-Level Scenarios Assures Interactive Consistency for m FaultsResearch Paper

Motivation

Setting

Formalization targets

Goal: the procedure assures interactive consistency

Milestones, in the order the paper's proof uses them

Significance

Difficulty

Formalization scope

Selected references

A New Class of Random Number Generators 1: For Prime m = bʳ + bˢ − 1, Every Nontrivial Add-with-Carry Sequence Is Periodic After r Steps, with Period the Order of b mod mResearch Paper

Why add-with-carry generators

Setting

Formalization targets

Goal: the period is the order of bbb

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Weighted Majority Algorithm 6: Under the Weak Independence Condition, the Randomized Master WMR Has E(m) ≤ E(ln(w_init/w_fin))/(1−β)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1

Milestone: expected mistakes equal expected loss of the weighted average

Significance

Goal: the period is the order of $b$

Goal: the mistake bound of $\mathrm{WMI}_2$