Theoretical Computer Science

Completed

Captain: marwahaha

Schönhage–Pan–Winograd Bound: omega < 2.522Research Paper

Motivation

The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, $N\times N$ matrices can be multiplied using $O(N^{c+\varepsilon})$ arithmetic operations for every $\varepsilon>0$ . Improvements to $\omega$ are a central benchmark in algebraic complexity because matrix multiplication is also a basic subroutine in linear algebra, graph algorithms, and symbolic computation.

The existing Prove2Me mission formalizes Schönhage's bound $\omega<2.55$ from a concrete two-summand tensor degeneration. The present mission advances the same formal development to the next clean historical construction. Pan and Winograd found a simultaneous approximate algorithm for three matrix products; Romani recorded its tensor form and the parameter choice $n=11$ , $k=5$ , which gives $\omega\le 2.5218127\ldots$ . Schönhage's 1981 paper reports the equivalent bound $3\log 52/\log 110$ in the arbitrary-field setting. The exact formal target here is the slightly weaker rational inequality $\omega<1261/500=2.522$ .

Setting

For a field $K$ , the matrix-multiplication tensor $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix:

\langle a,b,c\rangle_K =\sum_{i<a}\sum_{j<b}\sum_{\ell<c} e_{ij}\otimes e_{j\ell}\otimes e_{\ell i}.

A direct sum places several such tensors in disjoint coordinate blocks. A tensor $T$ has border rank at most $r$ when it is a polynomial degeneration of the diagonal tensor $I_r=\sum_{s<r}e_s\otimes e_s\otimes e_s$ . In the Lean development this relation is Degenerates T (TensorObj.diagObj K 3 r). The argument order matters: the first tensor is the target and the diagonal tensor is the source.

The platform already defines ordinary tensor rank, asymptotic tensor rank, the tensor-rank exponent matMulExp K, the equivalent Strassen-preorder exponent matMulExp_strassen K, and Schönhage's asymptotic sum inequality. This mission reuses those declarations. No alternative definition of $\omega$ is introduced.

Formalization targets

The goal has exactly the same quantified proposition as the existing $2.55$ mission, with only the rational endpoint changed:

\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{1261}{500}.

The source construction to be formalized is

\underline R\!\left( \langle1,5,22\rangle_K\oplus \langle11,2,5\rangle_K\oplus \langle10,11,1\rangle_K \right)\le156.

Each summand has volume $110$ :

1\cdot5\cdot22=11\cdot2\cdot5=10\cdot11\cdot1=110.

The milestone chain records the degeneration, its asymptotic-rank consequence, the exact numerical implication

3\cdot110^{\omega^{\mathrm{Str}}_K/3}\le156 \quad\Longrightarrow\quad \omega^{\mathrm{Str}}_K<\frac{1261}{500},

and the resulting Strassen-form exponent bound. The public goal then transfers the bound to matMulExp K through the already established equality of the two exponent definitions.

Significance

Mathematically, this construction improves the concrete exponent certified by the existing mission from $2.55$ to $2.522$ without changing the surrounding theory. It isolates the first genuinely new ingredient after the accepted Schönhage example: a larger simultaneous tensor degeneration rather than a sharper numerical estimate for the old witness.

For formalization, the mission tests whether the current polynomial-degeneration API can express a historically important trilinear aggregation at realistic scale. Once the explicit witness is available, the remaining declarations form a reusable template for later bounds: a source tensor degeneration, an asymptotic-rank bound, a specialization of the asymptotic sum inequality, and a final exponent transfer. This creates a trustworthy stepping stone toward the Coppersmith--Winograd tensor and later laser-method analyses.

The $2.522$ theorem is known mathematically; the open work is its machine-checked Lean formalization. The exact numerical endpoint and every downstream bridge from the degeneration have already been checked locally. The explicit Pan--Winograd degeneration remains the substantive open milestone.

Difficulty

The central difficulty is not the logarithmic comparison. It is constructing and verifying the polynomial family whose leading nonzero coefficient is exactly the tagged direct sum of the three matrix-multiplication tensors and whose earlier coefficients vanish. The family has $156$ diagonal source slots and many indexed target coordinates. A proof must account for all mixed-coordinate terms and all cancellations uniformly over an arbitrary field.

Romani's published summary states the approximate-rank inequality but does not spell out a Lean-ready map between its trilinear forms and the platform's TensorObj.bigAdd coordinate spaces. A solver must therefore recover the source indexing carefully and prove that the resulting modewise linear maps have the required coefficients. Reversing the degeneration direction, conflating tensor rank with asymptotic rank, or silently assuming a characteristic-zero scalar identity would invalidate the result.

Formalization scope

All theorems quantify over an arbitrary type $K$ with [Field K], matching the existing Schönhage goal and the arbitrary-field statement of the source bound. Tensor spaces are finite-dimensional function spaces already packaged by MMObj; the three products are combined with TensorObj.bigAdd. Border rank is represented by the existing finitely supported polynomial-family predicate Degenerates. Because the source summary specifies approximate rank but not a leading order, the main degeneration milestone existentially quantifies that order instead of hard-coding one.

The mission includes no placeholder laser-value definition and makes no claim about the later $2.376$ analysis. It also excludes Schönhage's additional microscopic symmetrization improvement beyond $3\log52/\log110$ . A valid solution must construct the stated degeneration itself; a vacuous hypothesis or a redefinition of matMulExp is outside scope.

Reusable contributions include coefficient lemmas for polynomial tensor families, finite-index equivalences for direct sums, and generic aggregation identities that specialize to the $n=11$ , $k=5$ witness. Contributions that merely restate the target under stronger field hypotheses do not close the arbitrary-field milestone.

Selected references

A. Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.
Francesco Romani, Some Properties of Disjoint Sums of Tensors Related to Matrix Multiplication, CNR Nota Interna B80-4, February 1980, printed p. 6; journal version, SIAM Journal on Computing 11(2), 1982. Archived preprint and DOI 10.1137/0211020.
Avi Wigderson and Jeroen Zuiddam, Asymptotic Spectra: Theory, Applications and Extensions, 2023, for the tensor-preorder and asymptotic-rank framework reused by the Lean development. Author manuscript.

27 thms4 active usersReviewed

Completed

Captain: Chutong

CLRS — Chapter 20, §20.5: Strongly Connected Components (Kosaraju) — Correctness and Running TimeTextbook

The mutual-reachability partition

Two vertices belong to the same strongly connected component when each can reach the other by a directed path. The partition separates the mutually reachable parts of a directed graph without requiring the whole graph to be connected. This mission formalizes the two-pass DFS algorithm of CLRS, fourth edition, Chapter 20, §20.5, often called Kosaraju's algorithm. The fourth-edition contents place this material after DFS in §20.3.

Graph and returned component labels

The input graph has $n$ vertices numbered from zero and $m$ adjacency occurrences. Its representation is an array of integer adjacency arrays plus a degree sequence. Parallel arcs and self-loops are allowed; duplicate occurrences contribute separately to $m$ . Empty and disconnected graphs are included. Symmetric entries can represent an undirected graph, but no symmetry is assumed.

The source scc calls the shared dfs entry, constructs the transpose by reversing every adjacency occurrence, and calls the same dfs_ordered entry on that transpose. The first pass produces increasing finish order. A linear pass reverses the order prefix for the second traversal; no comparison sort is performed. The returned object is the second traversal's DFSResult.

Its component array contains integer labels, and components contains their count $k$ . Labels are contiguous identifiers $0,\ldots,k-1$ , each used by at least one vertex. They are not canonical vertex representatives and need not be stable under adjacency reordering. Only the component fields are specified by the SCC postcondition; the remaining result fields describe the second DFS pass on the transpose.

Formalization targets

The headline CLRS.SCC.scc_correctness_and_running_time requires a single terminating scc.Call whose result labels exactly the initial graph's mutual-reachability classes. For every valid pair $u,v$ ,

\operatorname{component}[u]=\operatorname{component}[v] \iff (u\leadsto v)\land(v\leadsto u).

The component count must satisfy

0\le k\le n,\qquad k=0\iff n=0,

and every label below $k$ must occur. The component array and result object are fresh, and the complete call preserves all previously allocated caller storage. Its named-event cost obeys one uniform bound:

\exists C\in\mathbb N,\ C>0:\quad T\le C(1+n+m).

A supporting SCC milestone requests the explicit bound

T\le20+21n+6m

for the same call and complete postcondition. This includes both DFS traversals, input-order construction, transpose construction, finish-order reversal, and fixed setup work.

The other supporting milestone, transpose_correctness_and_running_time, requests a fresh graph with exactly reversed adjacency occurrences, unchanged vertex and occurrence counts, caller-storage preservation, and a uniform linear event bound. Reversal retains multiplicity, not just the existence of edges. These are open goals; no mathematical or execution proof is supplied.

Composing a verified traversal

The desired result gives later callers an exact test for component membership by comparing labels. Its count and coverage clauses make the labels usable for a compact representation of the partition. An algorithm using the partition need not repeat the analysis of recursive exploration or inspect compiler transitions.

The separate DFS mission supplies CLRS.DFS.ordered_correctness_and_explicit_running_time as an open dependency, with the full forest and storage contract and the numerical budget $4+6n+2m$ for any valid supplied root permutation. Its identity-order companion, CLRS.DFS.correctness_and_explicit_running_time, requests $7+8n+2m$ for the first pass. These explicit budgets can be combined with transpose construction and finish-order reversal to establish this mission's complete event bound. This mission imports the same definitions and requests the new component theorem; it does not duplicate the DFS program. The main statement contains no hypothesis asserting that DFS or SCC is already correct. The mathematical two-pass algorithm and its linear bound are textbook results; formal verification of these particular generated calls is the contributor task. See CLRS, fourth edition, §§20.3 and 20.5.

What must be justified

A DFS tree in an arbitrary directed graph is not necessarily a strongly connected component. The second traversal's particular order and reversed edges are essential to the requested equivalence. Both directions matter: vertices assigned the same label must be mutually reachable, and mutually reachable vertices must not receive different labels. The cost obligation cannot omit the transpose or order-processing loops, and repeated arcs must be counted rather than treated as free duplicates.

Formalization scope

Reachability is defined by finite paths in the original graph, including zero-edge paths at valid vertices. Transposition preserves each edge occurrence. Every transpose row, including an empty row, is separately allocated before any edges are appended, so the program does not accidentally share mutable row storage. Caller input rows may alias because they remain read-only.

The shared prerequisites are the published Algo2Lean runtime, module-call support, and unweighted graph representation and specifications. All three missions reuse these same definitions by reference, without introducing duplicate prerequisite bundles. The existing Dijkstra graph definition uses weighted, object-linked adjacency lists; the shared unweighted module supplies the arrays-of-arrays storage contract used here.

The definitions use Algo2Lean v0.1.4, source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, in project mode with standalone=false. The source root contains the explicitly named modules below; the entry file is identified for each mission. The reproduction manifest records raw generation and platform import-path adaptations separately. Stable generated definitions supply the public Call relations.

The clock graph_work counts the marked source blocks, function entries, and evaluated loop guards, including final false guards. Each marked block contains a fixed amount of source work. Costs are differences between the caller's actual initial and final counters; other clocks are preserved. This model uses mathematical integer sequences and unbounded integers. It does not assert machine wall-clock time, integer bit complexity, stack-space bounds, or Lean proof-checking time. Construction of the caller's input graph is outside the traversal entry point.

All theorem bodies are open contributor tasks. Supplied definitions and well-formed goal statements are not correctness, termination, or running-time proofs. The requested results concern the displayed program's actual executions, not an assumed-correct replacement algorithm or a hypothesis containing its conclusion.

The complete entry is scc.algo; its dependencies are dfs.algo and graph_input.algo. The DFS source is shown unchanged to make the imports and counted work explicit. Supporting theorem references reuse the DFS mission's definitions and open contract.

`graph_input.algo`

# Unweighted directed graph: vertices are 0, ..., size-1.
# Row adj[u][0:degree[u]] lists outgoing targets, with one slot per arc.
# Traversals require nonnegative degrees and in-range targets. Duplicate arcs
# and self-loops are allowed. The constructor stores the supplied references.

class UnweightedGraph:
    size: Int
    adj: Seq[Seq]
    degree: Seq

    def __init__(self, size: Int, adj: Seq[Seq], degree: Seq) -> None:
        self.size = size
        self.adj = adj
        self.degree = degree

`dfs.algo`

# CLRS fourth edition, Section 20.3: depth-first search.
# dfs_ordered takes a permutation of the vertices as its outer-loop order.
# Result.order lists vertices in increasing finish time; reverse its valid
# prefix before using it as the second-pass order in the SCC algorithm.
# graph_work counts the explicitly marked blocks and loop-guard evaluations.

from graph_input import UnweightedGraph


class DFSResult:
    color: Seq
    parent: Seq
    discover: Seq
    finish: Seq
    order: Seq
    component: Seq
    clock: Int
    finished: Int
    components: Int

    def __init__(self) -> None:
        tick("graph_work")
        self.color = const(0)
        self.parent = const(-1)
        self.discover = const(0)
        self.finish = const(0)
        self.order = const(-1)
        self.component = const(-1)
        self.clock = 0
        self.finished = 0
        self.components = 0


def visit(graph: UnweightedGraph, result: DFSResult, u: Int, label: Int) -> None:
    tick("graph_work")
    result.clock += 1
    result.discover[u] = result.clock
    result.color[u] = 1
    result.component[u] = label
    neighbors: Seq = graph.adj[u]
    j: Int = 0
    tick("graph_work")
    # @scan_neighbors
    while j < graph.degree[u]:
        tick("graph_work")
        v: Int = neighbors[j]
        if result.color[v] == 0:
            tick("graph_work")
            result.parent[v] = u
            visit(graph, result, v, label)
        j += 1
        tick("graph_work")
    tick("graph_work")
    result.color[u] = 2
    result.clock += 1
    result.finish[u] = result.clock
    result.order[result.finished] = u
    result.finished += 1


def dfs_ordered(graph: UnweightedGraph, order: Seq) -> DFSResult:
    tick("graph_work")
    result: DFSResult = DFSResult()
    i: Int = 0
    tick("graph_work")
    # @scan_roots
    while i < graph.size:
        tick("graph_work")
        u: Int = order[i]
        if result.color[u] == 0:
            tick("graph_work")
            visit(graph, result, u, result.components)
            result.components += 1
        i += 1
        tick("graph_work")
    tick("graph_work")
    return result


def dfs(graph: UnweightedGraph) -> DFSResult:
    tick("graph_work")
    order: Seq = const(0)
    i: Int = 0
    tick("graph_work")
    # @identity_order
    while i < graph.size:
        tick("graph_work")
        order[i] = i
        i += 1
        tick("graph_work")
    tick("graph_work")
    return dfs_ordered(graph, order)

`scc.algo`

# CLRS fourth edition, Section 20.5: strongly connected components.
# The first DFS records increasing finish order. The second DFS visits the
# transpose in decreasing first-pass finish order. Its forest labels are SCCs.
# Adjacency rows in the transpose are separately allocated, including empty rows.
# graph_work counts the explicitly marked blocks and loop-guard evaluations.

from graph_input import UnweightedGraph
from dfs import DFSResult, dfs, dfs_ordered


def transpose(graph: UnweightedGraph) -> UnweightedGraph:
    tick("graph_work")
    adj: Seq[Seq] = const(const(0))
    degree: Seq = const(0)
    u: Int = 0
    tick("graph_work")
    # @allocate_rows
    while u < graph.size:
        tick("graph_work")
        adj[u] = const(0)
        u += 1
        tick("graph_work")

    u = 0
    tick("graph_work")
    # @scan_sources
    while u < graph.size:
        tick("graph_work")
        neighbors: Seq = graph.adj[u]
        j: Int = 0
        tick("graph_work")
        # @reverse_edges
        while j < graph.degree[u]:
            tick("graph_work")
            v: Int = neighbors[j]
            adj[v][degree[v]] = u
            degree[v] = degree[v] + 1
            j += 1
            tick("graph_work")
        u += 1
        tick("graph_work")

    tick("graph_work")
    return UnweightedGraph(graph.size, adj, degree)


def scc(graph: UnweightedGraph) -> DFSResult:
    tick("graph_work")
    first: DFSResult = dfs(graph)
    tick("graph_work")
    reversed_graph: UnweightedGraph = transpose(graph)
    tick("graph_work")
    order: Seq = const(-1)
    i: Int = 0
    tick("graph_work")
    # @decreasing_finish_order
    while i < graph.size:
        tick("graph_work")
        order[i] = first.order[graph.size - 1 - i]
        i += 1
        tick("graph_work")
    tick("graph_work")
    return dfs_ordered(reversed_graph, order)

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022. Publisher; fourth-edition table of contents.
Lunjia Hu and Chutong Yang, Algo2Lean, software release v0.1.4. Lunjia Hu is the project creator. Hosted compiler; fixed release source.

13 thms3 active usersReviewed

Completed

Captain: Chutong

CLRS — Chapter 20, §20.3: Depth-First Search — Correctness and Running TimeTextbook

A traversal forest that later algorithms can reuse

Depth-first search records a directed graph's exploration as a predecessor forest with discovery and finish times. Those outputs are used by algorithms that depend on the ordering of exploration, including strongly connected components. This mission targets CLRS, fourth edition, Chapter 20, §20.3; its companion component mission targets §20.5. Both references are fixed by the fourth-edition contents.

Ordered exploration and event times

The input is an unweighted directed graph on $n$ vertices, represented by integer adjacency arrays of arrays and a degree sequence. The number $m$ counts adjacency occurrences, including parallel arcs. Self-loops, disconnected graphs, and the empty graph are included. Prefix entries identify vertices; entries outside those prefixes have no specified meaning.

The reusable entry dfs_ordered receives an allocated root-order sequence whose first $n$ entries form a permutation of the vertices. The ordinary entry dfs constructs identity order and invokes it. Both use the same recursive visit routine. The result includes parent, discovery, finish, color, finish-order, and forest-component arrays, together with event, finished-vertex, and component counts.

Let $d[v]$ and $f[v]$ be discovery and finish times. An ancestor is defined by zero or more returned parent-child links. The output order lists vertices in increasing finish time. The companion SCC source explicitly reverses this prefix; the DFS result itself is not advertised as decreasing order.

Formalization targets

The headline CLRS.DFS.correctness_and_running_time concerns the complete identity-order call. It requests the complete forest and storage contract and one uniform runtime bound:

\exists C\in\mathbb N,\ C>0:\quad T\le C(1+n+m).

The constant is independent of the graph, heap, and initial clocks. Two supporting milestones make the counted work available for composition. CLRS.DFS.ordered_correctness_and_explicit_running_time covers every valid supplied root permutation and requests

T_{\mathrm{ordered}}\le 4+6n+2m.

CLRS.DFS.correctness_and_explicit_running_time covers the complete identity-order entry and requests

T_{\mathrm{dfs}}\le 7+8n+2m.

The identity-order wrapper contributes $3+2n$ marked events outside its ordered call, so the numerical targets compose directly. The explicit ordered budget also supports the second pass of SCC, where the caller supplies decreasing first-pass finish order. Each milestone includes the full postcondition and bounds that same terminating call. All three statements are open contributor tasks; no DFS correctness or runtime proof is supplied.

For every vertex, the returned event times must satisfy

1\le d[v]<f[v]\le2n,

with all $2n$ discovery and finish events distinct. Every non-root parent is an actual input predecessor. Ancestors correspond exactly to nested event intervals:

u\text{ is an ancestor of }v\iff d[u]\le d[v]\ \land\ f[v]\le f[u].

Unrelated intervals are disjoint. The white-path property additionally equates descendants of $u$ with vertices reachable from $u$ using only vertices whose discovery time is at least $d[u]$ . Root-order priority requires every earlier input-order vertex to finish before a later tree root is discovered. These are required structural properties of the ordered traversal; the generated Call relation fixes the concrete adjacency-scanning order.

The finish-order prefix is a vertex permutation with strictly increasing finish times. All output colors are black, the event clock is $2n$ , and the finished count is $n$ . Component labels are contiguous nonempty forest-tree identifiers; equal labels mean the same predecessor tree, not necessarily the same strongly connected component. Every target is an open theorem for contributors.

Reuse beyond a single traversal

A caller can retain the fresh result and continue with its heap, using the unchanged graph and all other pre-existing storage. The caller-facing predicate CLRS.DFS.Post before after result g inputOrder includes both the mathematical result and caller-storage preservation, matching the argument order and preservation placement used by BFS. It requires a fresh result object and six distinct fresh arrays. The goals combine that postcondition with the same terminating Call and its cost. Once proved, the explicit ordered contract supports a later caller's own root permutation without copying the DFS implementation or repeating its analysis.

This scope matters for the textbook SCC construction: its second traversal needs an order supplied by a first traversal. Merely returning timestamps would omit the structural properties that make those timestamps useful. Formalizing the complete contract makes the existing mathematical DFS analysis available through the generated public Call interface; no DFS proof is supplied here.

What must be justified

Valid parent edges and distinct timestamps alone do not identify a DFS forest. The open contract also relates ancestry, interval nesting, white paths, and the outer loop's priority. Directed reachability must not be confused with membership in one DFS tree: an edge may point into a tree that finished earlier. The event-count argument must cover recursive calls and the full outer scan, including already visited vertices, while the empty graph still returns allocated outputs.

Formalization scope

The graph and root-order sequence are read-only and may share input storage where their representation conditions permit it. Recursive calls share a fresh result object. Its component count equals the number of nonempty forest trees; labels follow tree-discovery order. The identity-order entry includes constructing that order in its own cost. The ordered entry's input permutation is supplied by its caller and is preserved.

The shared prerequisites are the published Algo2Lean runtime, module-call support, and unweighted graph representation and specifications. All three missions reuse these same definitions by reference, without introducing duplicate prerequisite bundles. The existing Dijkstra graph definition uses weighted, object-linked adjacency lists; the shared unweighted module supplies the arrays-of-arrays storage contract used here.

The definitions use Algo2Lean v0.1.4, source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, in project mode with standalone=false. The source root contains the explicitly named modules below; the entry file is identified for each mission. Raw generated definitions and platform import-path adaptations are recorded separately in the reproduction manifest. Stable generated definitions supply the public Call relations; optional named-line interfaces are not part of the goal statements.

The clock graph_work counts the marked source blocks, function entries, and evaluated loop guards, including final false guards. Each marked block contains a fixed amount of source work. Costs are differences between the caller's actual initial and final counters; other clocks are preserved. This model uses mathematical integer sequences and unbounded integers. It does not assert machine wall-clock time, integer bit complexity, stack-space bounds, or Lean proof-checking time. Construction of the caller's input graph is outside the traversal entry point.

All theorem bodies are open contributor tasks. Supplied definitions and well-formed goal statements are not correctness, termination, or running-time proofs. The requested results concern the displayed program's actual executions, not an assumed-correct replacement algorithm or a hypothesis containing its conclusion.

The complete entry is dfs.algo, with graph_input.algo as its shared dependency. CLRS.DFS.Forest and Post expose the reusable mathematical and storage contracts. Contributions should establish these open obligations against the displayed source.

`graph_input.algo`

# Unweighted directed graph: vertices are 0, ..., size-1.
# Row adj[u][0:degree[u]] lists outgoing targets, with one slot per arc.
# Traversals require nonnegative degrees and in-range targets. Duplicate arcs
# and self-loops are allowed. The constructor stores the supplied references.

class UnweightedGraph:
    size: Int
    adj: Seq[Seq]
    degree: Seq

    def __init__(self, size: Int, adj: Seq[Seq], degree: Seq) -> None:
        self.size = size
        self.adj = adj
        self.degree = degree

`dfs.algo`

# CLRS fourth edition, Section 20.3: depth-first search.
# dfs_ordered takes a permutation of the vertices as its outer-loop order.
# Result.order lists vertices in increasing finish time; reverse its valid
# prefix before using it as the second-pass order in the SCC algorithm.
# graph_work counts the explicitly marked blocks and loop-guard evaluations.

from graph_input import UnweightedGraph


class DFSResult:
    color: Seq
    parent: Seq
    discover: Seq
    finish: Seq
    order: Seq
    component: Seq
    clock: Int
    finished: Int
    components: Int

    def __init__(self) -> None:
        tick("graph_work")
        self.color = const(0)
        self.parent = const(-1)
        self.discover = const(0)
        self.finish = const(0)
        self.order = const(-1)
        self.component = const(-1)
        self.clock = 0
        self.finished = 0
        self.components = 0


def visit(graph: UnweightedGraph, result: DFSResult, u: Int, label: Int) -> None:
    tick("graph_work")
    result.clock += 1
    result.discover[u] = result.clock
    result.color[u] = 1
    result.component[u] = label
    neighbors: Seq = graph.adj[u]
    j: Int = 0
    tick("graph_work")
    # @scan_neighbors
    while j < graph.degree[u]:
        tick("graph_work")
        v: Int = neighbors[j]
        if result.color[v] == 0:
            tick("graph_work")
            result.parent[v] = u
            visit(graph, result, v, label)
        j += 1
        tick("graph_work")
    tick("graph_work")
    result.color[u] = 2
    result.clock += 1
    result.finish[u] = result.clock
    result.order[result.finished] = u
    result.finished += 1


def dfs_ordered(graph: UnweightedGraph, order: Seq) -> DFSResult:
    tick("graph_work")
    result: DFSResult = DFSResult()
    i: Int = 0
    tick("graph_work")
    # @scan_roots
    while i < graph.size:
        tick("graph_work")
        u: Int = order[i]
        if result.color[u] == 0:
            tick("graph_work")
            visit(graph, result, u, result.components)
            result.components += 1
        i += 1
        tick("graph_work")
    tick("graph_work")
    return result


def dfs(graph: UnweightedGraph) -> DFSResult:
    tick("graph_work")
    order: Seq = const(0)
    i: Int = 0
    tick("graph_work")
    # @identity_order
    while i < graph.size:
        tick("graph_work")
        order[i] = i
        i += 1
        tick("graph_work")
    tick("graph_work")
    return dfs_ordered(graph, order)

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022. Publisher; fourth-edition table of contents.
Lunjia Hu and Chutong Yang, Algo2Lean, software release v0.1.4. Lunjia Hu is the project creator. Hosted compiler; fixed release source.

10 thms3 active usersReviewed

Completed

Captain: Chutong

CLRS — Chapter 20, §20.2: Breadth-First Search — Correctness and Running TimeTextbook

Shortest paths in an unweighted graph

Breadth-first search computes which vertices can be reached from a source and the fewest edges needed to reach each one. Its predecessor information also records a shortest route. This mission belongs to the CLRS fourth-edition formalization series and targets Chapter 20, §20.2, including the algorithm's linear running-time guarantee. The section placement is given in the publisher's table of contents.

Graph, source, and outputs

A directed graph consists of vertices numbered $0,\ldots,n-1$ and outgoing adjacency rows. The field adj[u] is an integer sequence, and degree[u] determines its meaningful prefix. Every entry in that prefix must name a valid vertex. Let $m$ be the sum of these row lengths: parallel arcs count separately, and self-loops are permitted. An undirected graph is represented by symmetric directed entries, with both directions counted in $m$ .

The caller supplies a valid source $s$ , with $0\le s<n$ . Consequently, the source contract excludes the empty graph. The distance output uses $-1$ for an unreachable vertex; otherwise it records a nonnegative number of edges. The parent output uses $-1$ at the source and unreachable vertices. Other reached vertices have a predecessor. No particular choice between equally short routes is required.

Formalization targets

The headline CLRS.BFS.correctness_and_running_time asks for one actual terminating bfs.Call whose result satisfies correctness, preservation, allocation, and running time together. Write $D$ and $P$ for its output arrays and $s\leadsto v$ for a finite directed walk in the initial graph. For every vertex $v$ ,

D[v]=-1\iff\neg(s\leadsto v).

When $D[v]\ge0$ , the returned distance is attained and minimal:

\exists\text{ a walk }s\leadsto v\text{ of length }D[v],\qquad D[v]\le\text{length}(p)\text{ for every walk }p:s\leadsto v.

Moreover, $D[s]=0$ , $P[s]=-1$ , and each reached $v\ne s$ satisfies

P[v]\to v,\qquad D[P[v]]+1=D[v].

The running-time target is uniform over inputs, heaps, adjacency order, and initial counters:

\exists C\in\mathbb N,\ C>0:\quad T\le C(1+n+m).

Here $T$ is the increment of graph_work for that same call. The supporting milestone correctness_and_explicit_running_time retains the stronger numerical target

T\le 6n+2m+5

with the identical correctness and storage contract. Both statements are open; the numerical bound is a requested obligation, not an established result.

A reusable shortest-path contract

The result allows a later caller to read shortest distances and predecessor edges while continuing with the returned heap. The caller-facing predicate CLRS.BFS.Post before after result g source includes both the mathematical result and caller-storage preservation. It requires a fresh result object and two distinct fresh arrays, and preserves every previously allocated sequence, object, and collection. The goals combine that postcondition with the same terminating Call and its cost. Input graph storage therefore remains available for further traversals.

The textbook supplies the mathematical algorithm and analysis; the work here is their formal verification against a mutable source program. The finite-prefix specification gives callers useful facts without prescribing irrelevant sequence entries outside the vertex range. The source's discovery state is encoded by distance $-1$ , and its queue is a fresh sequence with head and tail indices. These are implementation choices within the stated BFS contract. The familiar correctness and complexity claims are discussed in CLRS, fourth edition, §20.2.

What must be justified

Returning a reachable predecessor alone does not establish shortestness. The contract also requires minimum distance and a correct unreachable sentinel. Cycles, repeated adjacency entries, and edges to vertices already discovered must not produce repeated queue insertion or invalidate the cost bound. An execution theorem must establish termination and the result together; reasoning only about executions that happen to return leaves a missing obligation.

Formalization scope

CLRS.GraphTraversal.GraphRep connects the input heap to a finite mathematical graph. Adjacency rows may share references, because traversal only reads them. Validity includes allocated rows and nonnegative degrees. The explicit initialization loop is counted even though the result constructor already gives the same default values. Outputs are fresh, so their mutation cannot change aliased input storage.

The shared prerequisites are the published Algo2Lean runtime, module-call support, and unweighted graph representation and specifications. All three missions reuse these same definitions by reference, without introducing duplicate prerequisite bundles. The existing Dijkstra graph definition uses weighted, object-linked adjacency lists; the shared unweighted module supplies the arrays-of-arrays storage contract used here.

The definitions use Algo2Lean v0.1.4, source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, in project mode with standalone=false. The source root contains the explicitly named modules below; the entry file is identified for each mission. Raw generated definitions and platform import-path adaptations are recorded separately in the reproduction manifest. Stable generated definitions supply the public Call relations; optional named-line interfaces are not part of the goal statements.

The clock graph_work counts the marked source blocks, function entries, and evaluated loop guards, including final false guards. Each marked block contains a fixed amount of source work. Costs are differences between the caller's actual initial and final counters; other clocks are preserved. This model uses mathematical integer sequences and unbounded integers. It does not assert machine wall-clock time, integer bit complexity, stack-space bounds, or Lean proof-checking time. Construction of the caller's input graph is outside the traversal entry point.

All theorem bodies are open contributor tasks. Supplied definitions and well-formed goal statements are not correctness, termination, or running-time proofs. The requested results concern the displayed program's actual executions, not an assumed-correct replacement algorithm or a hypothesis containing its conclusion.

The complete source entry is bfs.algo; its shared dependency is graph_input.algo. Contributors may add proof lemmas or named observations while retaining the main source-facing contract.

`graph_input.algo`

# Unweighted directed graph: vertices are 0, ..., size-1.
# Row adj[u][0:degree[u]] lists outgoing targets, with one slot per arc.
# Traversals require nonnegative degrees and in-range targets. Duplicate arcs
# and self-loops are allowed. The constructor stores the supplied references.

class UnweightedGraph:
    size: Int
    adj: Seq[Seq]
    degree: Seq

    def __init__(self, size: Int, adj: Seq[Seq], degree: Seq) -> None:
        self.size = size
        self.adj = adj
        self.degree = degree

`bfs.algo`

# CLRS, fourth edition, Chapter 20, Section 20.2: breadth-first search.
# Adjacency rows contain vertex identifiers; degree gives each finite row length.
# The graph is read-only. A valid source lies between 0 and graph.size - 1.

from graph_input import UnweightedGraph


class BFSResult:
    distance: Seq
    parent: Seq

    def __init__(self) -> None:
        tick("graph_work")
        self.distance = const(-1)
        self.parent = const(-1)


def bfs(graph: UnweightedGraph, source: Int) -> BFSResult:
    tick("graph_work")
    result = BFSResult()
    vertex: Int = 0

    tick("graph_work")
    while vertex < graph.size:
        tick("graph_work")
        result.distance[vertex] = -1
        result.parent[vertex] = -1
        vertex += 1
        tick("graph_work")

    tick("graph_work")
    queue: Seq = const(-1)
    head: Int = 0
    tail: Int = 1
    queue[0] = source
    result.distance[source] = 0

    tick("graph_work")
    while head < tail:
        tick("graph_work")
        vertex = queue[head]
        head += 1
        index: Int = 0

        tick("graph_work")
        while index < graph.degree[vertex]:
            tick("graph_work")
            neighbor: Int = graph.adj[vertex][index]
            if result.distance[neighbor] == -1:
                tick("graph_work")
                result.distance[neighbor] = result.distance[vertex] + 1
                result.parent[neighbor] = vertex
                queue[tail] = neighbor
                tail += 1
            index += 1
            tick("graph_work")

        tick("graph_work")

    tick("graph_work")
    return result

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022. Publisher; fourth-edition table of contents.
Lunjia Hu and Chutong Yang, Algo2Lean, software release v0.1.4. Lunjia Hu is the project creator. Hosted compiler; fixed release source.

6 thms3 active usersReviewed

Probability Quantum Information·Captain: mikedeng1

Quantum Amplitude Amplification and Estimation: Est_Amp(A, χ, M) Outputs ã with |ã − a| ≤ 2πk√(a(1−a))/M + k²π²/M² with Probability ≥ 8/π² for k = 1 and > 1 − 1/(2(k−1)) for k ≥ 2Research Paper

Motivation

Many quantum algorithms end in a measurement that succeeds only with some probability $a$ . Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude amplification generalizes Grover's search (Grover 1996) to an arbitrary algorithm $\mathcal A$ and an arbitrary notion of success. Amplitude estimation combines amplification with the quantum Fourier transform to estimate $a$ with error of order $1/M$ after $M$ applications of $\mathcal A$ , where classical sampling needs order $1/M^2$ samples. Quantum counting, quantum Monte Carlo integration (Montanaro 2015) and many quantum speedups for statistics and finance rest on this estimation step.

Timeline:

1996: Grover's search algorithm.
1997: Brassard and Høyer (arXiv:quant-ph/9704027) introduce the amplification operator $\mathbf Q$ for a general algorithm.
1998: Brassard, Høyer and Tapp (arXiv:quant-ph/9805082) give quantum counting.
2000: the paper formalized here presents amplification, estimation and counting in a unified form with explicit constants.

Setting

Let $\mathcal H = \mathbb C^\iota$ be a finite-dimensional Hilbert space with computational basis $\{|x\rangle : x\in\iota\}$ and a distinguished zero state $|0\rangle$ . A quantum algorithm without measurements is a unitary matrix $\mathcal A$ on $\mathcal H$ , and a Boolean function $\chi:\iota\to\{0,1\}$ calls a basis state good when $\chi(x)=1$ . Write $|\Psi\rangle=\mathcal A|0\rangle=|\Psi_1\rangle+|\Psi_0\rangle$ for the splitting into the projections onto the good and the bad subspaces. The initial success probability is $a=\langle\Psi_1|\Psi_1\rangle$ , the probability that measuring $|\Psi\rangle$ gives a good state, and $\theta_a\in[0,\pi/2]$ is the angle with $\sin^2\theta_a=a$ .

The operator $\mathbf S_\chi$ flips the sign of the amplitudes of good states, $\mathbf S_0$ flips the sign of the amplitude of $|0\rangle$ , and the amplification operator is

\mathbf Q=-\mathcal A\,\mathbf S_0\,\mathcal A^{-1}\,\mathbf S_\chi .

For an integer $M\ge1$ , the quantum Fourier transform is $F_M:|x\rangle\mapsto\frac1{\sqrt M}\sum_{y=0}^{M-1}e^{2\pi\imath xy/M}|y\rangle$ , and the controlled power is $\Lambda_M(U):|j\rangle|y\rangle\mapsto|j\rangle U^j|y\rangle$ . The phase state is $|S_M(\omega)\rangle=\frac1{\sqrt M}\sum_y e^{2\pi\imath\omega y}|y\rangle$ , and $d(\omega_0,\omega_1)=\min_{z\in\mathbb Z}|z+\omega_1-\omega_0|$ is the circular distance. The algorithm $\mathbf{Est\_Amp}(\mathcal A,\chi,M)$ applies $(F_M^{-1}\otimes I)\,\Lambda_M(\mathbf Q)\,(F_M\otimes I)$ to $|0\rangle\mathcal A|0\rangle$ , measures the first register to obtain $y\in\{0,\dots,M-1\}$ , and outputs $\tilde a=\sin^2(\pi y/M)$ .

Formalization targets

Goal: Theorem 12 (Amplitude Estimation)

For every positive integer $k$ , the event

|\tilde a-a|\le 2\pi k\frac{\sqrt{a(1-a)}}{M}+k^2\frac{\pi^2}{M^2}

has probability at least $8/\pi^2$ when $k=1$ , and greater than $1-\frac1{2(k-1)}$ when $k\ge2$ . If $a=0$ then $\tilde a=0$ with certainty. If $a=1$ and $M$ is even, then $\tilde a=1$ with certainty.

Milestones, in attack order

Lemma 1: $\mathbf Q$ acts on $|\Psi_1\rangle$ and $|\Psi_0\rangle$ by an explicit $2\times2$ matrix.
Equations (3)–(5): for $0<a<1$ , $|\Psi_\pm\rangle$ are orthonormal eigenvectors of $\mathbf Q$ with eigenvalues $e^{\pm\imath2\theta_a}$ .
Equation (6): $|\Psi\rangle$ in that eigenbasis.
Lemma 7: the error in the angle controls the error in $\sin^2$ .
Lemma 10: the overlap $|\langle S_M(\omega_0)|S_M(\omega_1)\rangle|^2$ .
Theorem 11: the exact law of phase estimation and its two tail bounds.
Two steps of the proof of Theorem 12 (p. 20): the state after $\Lambda_M(\mathbf Q)$ , and the outcome law as an even mixture of two phase-estimation laws.

Further statements from the same development are included as companion targets: the success probability $\sin^2((2m+1)\theta_a)$ after $m$ rounds, Theorem 2 (quadratic speedup), Lemma 5 (the phase-generalized $\mathbf Q$ ), Theorem 13 (counting) and Corollary 14.

Significance

Theorem 12 is the quantitative core of quantum estimation algorithms. Its error bound scales as $1/M$ in the number of applications of $\mathbf Q$ , and that scaling is the quadratic speedup behind quantum counting (Theorem 13), quantum mean estimation, and quantum Monte Carlo methods for option pricing and risk analysis. The exact clauses for $a\in\{0,1\}$ make the estimator usable as a zero-error test for the existence of a good state.

All results here are proved in the paper and widely reproduced in textbooks; none is open. What the mission adds is a machine-checked account with the paper's constants: $8/\pi^2$ , the strict tail bound $1-1/(2(k-1))$ , and the additive term $k^2\pi^2/M^2$ . It also covers every modulus $M\ge1$ , not only powers of two, and arbitrary $\mathcal A$ and $\chi$ , not only uniform search. Related statements are posed on the platform but unproved:

QAlgorithms.Nannicini.amplitudeEstimation_error is the special case $k=1$ , $M=2^m$ , with a bit-string presentation of the algorithm.
QAlgorithms.Nannicini.groverOperator_eigenstates states (3)–(4) for an abstract reflection.
QAlgorithms.DeWolf.amplitudeAmplification covers (8) and the $1-a$ half of Theorem 2.

The Grover theorems already proved on the platform treat a single marked item with a uniform start.

Difficulty

The obvious argument has two parts: $\mathbf Q$ rotates a plane by $2\theta_a$ , and phase estimation reads off $\theta_a$ . Neither part settles the measurement law. The outcome probability is a sum over the second register of the squared amplitudes of an entangled state. Reducing it to two independent phase-estimation laws requires orthonormality of $|\Psi_\pm\rangle$ , and that holds only for $0<a<1$ . The goal does not assume this: the degenerate cases $a\in\{0,1\}$ , where $|\Psi_\pm\rangle$ do not exist, must be handled separately.

On the phase-estimation side, the tail bound for $k\ge2$ must be strict and must hold for every $M\ge1$ . The bound $8/\pi^2$ for $k=1$ relies on a minimization over $\Delta\in[0,1/M]$ that needs $M>2$ , while the goal has no such hypothesis, so the small cases $M\le2$ need their own argument. Finally, the second eigenphase appears as $1-\theta_a/\pi$ , and the matching outcome $M-y$ wraps to $0$ at $y=0$ .

Formalization scope

States are vectors $\iota\to\mathbb C$ over a finite type $\iota$ (the paper writes $\chi:\mathbb Z\to\{0,1\}$ ), operators are matrices, and $\{0,1\}$ is Bool. $\mathcal A$ is assumed unitary and $\mathcal A^{-1}$ is written $\mathcal A^\dagger$ . The second register is Fin M with $M\ge1$ ; $F_M$ is the platform's published Fourier matrix ShorAlgorithms.Shared.fourierMatrix (same sign and normalization as (13)), $F_M^{-1}$ is its conjugate transpose, and $\Lambda_M$ is an explicit matrix on Fin M × ι. The outcome law is the sum over the second register of squared moduli of the final state, and an event's probability is the sum of the outcome probabilities over it. $a$ is computed from $\mathcal A$ , $\chi$ and $|0\rangle$ , and $\theta_a=\arcsin\sqrt a$ . The goal assumes neither $0<a<1$ nor $M>2$ , and it keeps the strict inequality for $k\ge2$ . The step "after step 2, ignoring global phase" is stated with its phase $-\imath$ written out.

A formalization that takes $a$ or $\theta_a$ as a free parameter, assumes the mixture form of the outcome law, or reasons about $|\Psi_\pm\rangle$ without deriving them from $\mathcal A$ and $\chi$ would make the goal trivial. The statements here do none of these: every quantity is computed from $\mathcal A$ , $\chi$ , $|0\rangle$ and $M$ . The clauses "uses exactly $M$ evaluations of $f$ " (Theorem 12) and "requires exactly $\lceil\sqrt N\rceil$ evaluations" (Corollary 14) are not formalized, because the matrix model has no oracle whose calls could be counted. Theorem 13 is stated for any unitary sending $|0\rangle$ to the uniform superposition, which includes $F_N$ , as the paper allows on p. 20.

A complete development needs:

geometric sums of roots of unity;
the Fejér-kernel identity of Lemma 10;
the inequality $\sin x\ge 2x/\pi$ on $[0,\pi/2]$ ;
a bound on $\sum_{j\ge k}1/j^2$ ;
Kronecker-product bookkeeping for two-register states.

The phase-estimation part (Lemma 10, Theorem 11) does not depend on amplification and can be reused by any later formalization of Fourier-based phase estimation. Proofs of individual milestones, and lemmas on Fin M Fourier sums, are welcome.

Selected references

G. Brassard, P. Høyer, M. Mosca, A. Tapp, Quantum Amplitude Amplification and Estimation, in Quantum Computation and Information, Contemporary Mathematics 305, AMS, 2002, pp. 53–74. arXiv:quant-ph/0005055
G. Brassard, P. Høyer, An exact quantum polynomial-time algorithm for Simon's problem, ISTCS 1997. arXiv:quant-ph/9704027
G. Brassard, P. Høyer, A. Tapp, Quantum counting, ICALP 1998. arXiv:quant-ph/9805082
L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
A. Montanaro, Quantum speedup of Monte Carlo methods, Proc. R. Soc. A 471, 2015. arXiv:1504.06987

14 thms3 active usersReviewed

Completed

Captain: Chutong

CLRS — Chapter 6, §§6.1–6.2, 6.5: Indexed-Heap Sorting — Correctness and Running TimeTextbook

Category: Textbook

Review status: This is a private draft revision for the owner's review. The existing published SortIndicesAnalysis.call is marked Proved on Prove2Me. The new headline theorem is a separate draft derived from that contract; its proof remains local. The reused proof library and the new correctness-and-runtime wrapper compile locally with Lean 4.33.1; their axiom checks contain no sorryAx. The new proof has not been submitted to Prove2Me. No public submission or publication is authorized by this revision.

CLRS scope and implementation

This mission belongs to the CLRS fourth-edition formalization series. It presents sorting through an indexed binary min-priority queue, using the heap representation and heap-order ideas of Chapter 6, §§6.1–6.2, and priority-queue operations of §6.5.

It reuses Lunjia Hu's published .algo implementation, definitions, and correctness-and-cost call contract unchanged. The program inserts identifiers $0,\ldots,n-1$ with their keys and then repeatedly extracts the minimum. The result is a fresh sequence of sorted identifiers; the original keys remain unchanged. Equal keys may occur in either order.

This implementation differs from the in-place max-heap HEAPSORT of §6.4: it allocates auxiliary sequences and constructs the heap by repeated insertion. Accordingly, this draft targets an $O(n\log(n+1))$ sorting bound. Constant extra space, linear-time bottom-up construction, stability, and a matching worst-case lower bound are outside this theorem's claims.

Correctness

For every initial heap, every allocated key-sequence reference, and every natural length $n$ , the source-facing sort_indices.Call terminates with a final heap and a fresh allocated result reference. Its first $n$ entries are a permutation of $0,\ldots,n-1$ , ordered by the corresponding original keys. Previously allocated caller sequences and objects, and all collections, are preserved. The output outside this prefix is unspecified.

Negative integer keys, duplicate keys, and $n=0$ are included. The key reference must be allocated even for the empty case. The sequence model is total on integer indices; $n$ specifies the finite input prefix. Integers are mathematical, unbounded integers.

Running time

The headline theorem retains the existing per-clock Budget n (2n) for the same completed call and adds a uniform asymptotic statement. There is a positive natural constant $C$ , chosen independently of the heap, keys, length, and initial counters, such that

T\le C\bigl(1+n(1+\lfloor\log_2(n+1)\rfloor)\bigr).

Here $T$ is the sum of the increments of sort_steps, heap_comparisons, and heap_swaps. Each clock may start at an arbitrary value. If $d=\lfloor\log_2(n+1)\rfloor$ , the existing contract bounds these increments by $2n$ , $4nd$ , and $2n(d+1)$ respectively. It therefore retains the reusable explicit bound

T\le 2n\bigl(3\lfloor\log_2(n+1)\rfloor+2\bigr).

The clocks count the source's marked sorting-loop iterations, heap comparisons, and heap swaps. They do not count every arithmetic operation, array access, allocation, or compiler transition, and do not measure integer bit complexity, Lean checking time, or elapsed machine time. For the empty input the named event count can be zero although initialization and allocation still occur.

Reusable results and milestone

The single supporting milestone is the existing, proved SortIndicesAnalysis.call. It combines termination, sorted-permutation correctness, preservation, freshness, and per-clock budgets. Its implementation reuses the published indexed-heap insertion and minimum-extraction contracts.

The new headline is CLRS.HeapSortIndices.correctness_and_running_time. It imports that established call theorem and derives a uniform asymptotic consequence without repeating the heap correctness proof. Clients can apply the same call contract with their actual initial heap and counters, obtain sorted identifiers, and continue with the resulting heap. No new copy of the heap or runtime definitions is required.

The checked proof of the new headline is retained locally for review. A draft theorem statement may display a sorry placeholder; that placeholder is not an accepted proof or a Prove2Me verification result. An independent read-back of the formal statement is included in the local review package.

Algorithm source

The following files are reproduced unchanged from Lunjia Hu's public v0.1.4 source. Project import root: examples/kruskal. Entry file: sort_indices.algo.

`indexed_heap.algo`

# An indexed binary min-heap for Dijkstra's priority queue.
# vertices[position] and positions[vertex] are inverse on the active prefix.
# keys is indexed by vertex; position -1 means the vertex is not in the heap.
# Clients use nonnegative vertex identifiers, so pop_min can use -1 for empty.

class MinHeap:
    vertices: Seq
    positions: Seq
    keys: Seq
    size: Int

    def __init__(self) -> None:
        self.vertices = const(0)
        self.positions = const(-1)
        self.keys = const(0)
        self.size = 0

    def swap(self, i: Int, j: Int) -> None:
        a = self.vertices[i]
        b = self.vertices[j]
        # @exchange
        self.vertices[i] = b
        self.vertices[j] = a
        self.positions[a] = j
        self.positions[b] = i
        tick("heap_swaps")

    def sift_up(self, i: Int) -> None:
        # @up_loop
        while i > 0:
            parent = (i - 1) // 2
            tick("heap_comparisons")
            if self.keys[self.vertices[parent]] <= self.keys[self.vertices[i]]:
                return
            self.swap(i, parent)
            i = parent

    def sift_down(self, i: Int) -> None:
        # @down_loop
        while 2 * i + 1 < self.size:
            child = 2 * i + 1
            right = child + 1
            if right < self.size:
                tick("heap_comparisons")
                if self.keys[self.vertices[right]] < self.keys[self.vertices[child]]:
                    child = right
            # @compare_child
            tick("heap_comparisons")
            if self.keys[self.vertices[i]] <= self.keys[self.vertices[child]]:
                return
            self.swap(i, child)
            i = child

    def push_or_decrease(self, vertex: Int, key: Int) -> None:
        i = self.positions[vertex]
        if i < 0:
            self.keys[vertex] = key
            i = self.size
            self.vertices[i] = vertex
            self.positions[vertex] = i
            self.size += 1
            self.sift_up(i)
        else:
            tick("heap_comparisons")
            if key < self.keys[vertex]:
                self.keys[vertex] = key
                self.sift_up(i)

    def pop_min(self) -> Int:
        if self.size <= 0:
            return -1
        vertex = self.vertices[0]
        last = self.size - 1
        self.swap(0, last)
        self.size = last
        self.positions[vertex] = -1
        if last > 0:
            self.sift_down(0)
        return vertex

    def is_empty(self) -> Bool:
        return self.size <= 0

`sort_indices.algo`

# Order the identifiers [0, count) by their keys using a reusable binary heap.
# This supplies Kruskal's sort-by-weight step: insert every identifier, then
# extract minima. It is not the in-place HEAPSORT procedure from CLRS Chapter 6.
# Only identifiers are reordered; keys are unchanged. Equal-key identifiers
# may appear in either order.
from indexed_heap import MinHeap


def sort_indices(keys: Seq, count: Int) -> Seq:
    queue = MinHeap()
    result = const(0)
    index = 0
    # @insert
    while index < count:
        tick("sort_steps")
        queue.push_or_decrease(index, keys[index])
        index += 1
    index = 0
    # @extract
    while index < count:
        tick("sort_steps")
        result[index] = queue.pop_min()
        index += 1
    return result

Compiler provenance and validation

The compiler is Algo2Lean, numbered release v0.1.4, public source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, with Lean 4.33.1. Generation uses project mode, the two source files above, entry sort_indices.algo, generated namespace Algo.«sort_indices», and standalone=false.

The hosted compiler archive was downloaded and verified against its release manifest and checksums. All 196 payload files agree with the pinned public source. Generation under that archive's native Python bridge and its released Pyodide 314.0.7 runtime produces identical bytes for all six generated modules and two shared libraries. The release archive and source identities were recorded separately.

The corresponding Prove2Me modules match those raw outputs after two recorded packaging adaptations: rewriting project/runtime imports to Definitions.Def_*, and adding the platform's autoImplicit/backward-definitional-equality option prelude. All remaining bytes, including declaration bodies, are unchanged. The compiler archive SHA-256 is 52b3978479b4f4cc473e11471d839c6c96aafe0ffc73bbeeea4e785228f4fdf0.

Separately, all 18 modules in the published proof dependency closure have been checked locally with Lean 4.33.1 using the accepted proof bodies. To combine separately submitted proof files locally, non-target helper declarations are made private and final solution declarations receive unique audit names; theorem statements and proof bodies are retained, and the named targets are checked against their published types. This local proof packaging is distinct from the generated-code import adaptation above. The axiom audit found only propext, Classical.choice, and Quot.sound, with no sorryAx in the reused results.

These reproduction checks establish generation and packaging correspondence. Lean proof checking is a separate check; neither establishes a proof of compiler correctness.

Attribution and references

Algorithm implementation and reused heap/sorting proofs: Lunjia Hu. This draft presents their reusable sorting contract in the CLRS series and adds the uniform-bound wrapper. The source and proof attribution are retained.

CLRS, fourth edition, Chapter 6, §§6.1–6.2 and §6.5.
Published sorting call contract.
Pinned source and analysis.
Numbered compiler release.

2 thms3 active usersReviewed

Completed

Complexity Theory·Captain: avi

Fast Integer Multiplication on Multitape Turing Machines: Schönhage–Strassen and the ToolkitResearch Paper

Motivation

Every fast integer-multiplication algorithm in the literature is stated for the multitape Turing machine. The algorithms are built from a small set of standard subroutines whose costs are usually quoted as "well known":

linear-time addition;
sorting by merging on tapes;
fast matrix transposition;
a crude $O(n^{1+\delta})$ multiplier, used for the small multiplications inside fixed-point arithmetic.

Harvey–van der Hoeven (2021) use all of these in §2.1, §2.3 and §4–§5 of their $O(n\log n)$ paper. They cite Brent–Zimmermann for the arithmetic, Knuth vol. 3 for merge sort, and Bostan–Gaudry–Schost for transposition.

This mission formalizes that toolkit in the shared machine model IntMul_MultitapeModel. Its goal is the classical Schönhage–Strassen bound $\mathsf M(n)=O(n\log n\log\log n)$ . The toolkit is exactly what is missing before the recursive step of the companion mission, Harvey–van der Hoeven Proposition 5.4, can be decomposed. Proposition 5.4 is the last open link on that mission's main line.

Timeline (multitape Turing model).

Folklore: schoolbook multiplication in $O(n^2)$ ; addition in $O(n)$ .
1962: Karatsuba–Ofman, $O(n^{\log_2 3})$ .
1963–1966: Toom and Cook, $O(n^{1+\epsilon})$ for every $\epsilon>0$ .
1971: Schönhage–Strassen, $O(n\log n\log\log n)$ .
1973 (2nd ed. 1998): Knuth, TAOCP vol. 3 §5.4, merge sorting on tapes.
2007: Bostan–Gaudry–Schost, Appendix: transposing an $m\times k$ matrix with $N$ bits in total in $O(N\log\min(m,k))$ on a multitape machine.
2019/2021: Harvey–van der Hoeven, $O(n\log n)$ , using all of the above.

Setting

The machine model, input and output conventions, and the time-bound predicate $\mathrm{MulTimeBound}$ are those of IntMul_MultitapeModel. That model follows Montanaro's lecture notes:

$k\ge2$ one-way tapes, with a read-only input tape and a separate output tape;
$\triangleright$ appears only in cell $0$ of each tape;
$\mathrm{START}\ne\mathrm{HALT}$ , and the halting state freezes the configuration.

For subroutines whose input is not of the form $x\#y$ , the new definitions file IntMul_MultitapeWords starts the machine on an arbitrary word over $\{0,1,\#\}$ . It also provides the encodings

$\mathrm{bits}(x)$ , a bit string written as a word;
$u_1\#u_2\#\cdots\#u_m$ , a list of words joined by separators.

Formalization targets

Goal: Schönhage–Strassen

$\mathrm{MulTimeBound}(n\mapsto n\ln n\ln\ln n)$ : a single multitape machine multiplies $n$ -bit integers for every $n\ge1$ in worst-case time $O(n\log n\log\log n)$ .

Milestones

Schoolbook multiplication: $\mathrm{MulTimeBound}(n^2)$ .
Karatsuba–Ofman: $\mathrm{MulTimeBound}(n^{\log_2 3})$ .
Linear-time addition: on input $x\#y$ with $|x|=|y|=n$ , output $\operatorname{bin}_{n+1}(\operatorname{val}x+\operatorname{val}y)$ within $c(n+1)$ steps.
Merge sort on tapes:
- Input: $m$ records, each a key of $\ell$ bits and a payload of $q$ bits, written as $k_1\#p_1\#k_2\#p_2\#\cdots$ .
- Output: the records stably sorted by key value, in the same format.
- Time: $c\,(N+1)(\lceil\log_2 m\rceil+1)$ , where $N$ is the input length.
Matrix transposition:
- Input: an $m\times k$ matrix ( $m,k\ge1$ ) with entries of $\ell\ge1$ bits, in row-major order. Entries are separated by $\#$ and rows by $\#\#$ .
- Output: the transpose, in the same format.
- Time: $c\,(N+1)(\lceil\log_2\min(m,k)\rceil+1)$ .

Formalization scope

Constants may depend only on the machine. All time bounds count exact steps of one fixed machine in the shared model. Building machines by composing smaller ones (subroutine calls, scratch tapes, recursion) is the solvers' business; any reusable infrastructure for it is welcome as published lemmas.

Selected references

A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7 (1971), 281–292.
A. Karatsuba, Yu. Ofman, Multiplication of multidigit numbers on automata, Soviet Physics Doklady 7 (1963), 595–596.
D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, 2nd ed., Addison-Wesley, 1998, §5.4.
A. Bostan, P. Gaudry, É. Schost, Linear recurrences with polynomial coefficients and application to integer factorization and Cartier–Manin operator, SIAM J. Comput. 36 (2007), 1777–1806, Appendix.
R. P. Brent, P. Zimmermann, Modern Computer Arithmetic, Cambridge University Press, 2011, Ch. 1.
D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$ , Ann. of Math. 193 (2021), §2.1.
A. Montanaro, Computational Complexity, lecture notes, §3–§4.

15 thms3 active usersReviewed

Complexity Theory·Captain: wurtle

Integer multiplication: κ = 0.000051016920170078 (community PR #62)Open Problem

Motivation

Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an $O(n\log n)$ bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.

Setting

A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.

An input consists of two bit strings $x,y$ of the same positive length $n$ , separated by $\#$ . The strings are read most significant bit first, with leading zeros permitted. If $\operatorname{val}(x)$ denotes the represented natural number, the required output is exactly the $2n$ -bit binary representation of $\operatorname{val}(x)\operatorname{val}(y)$ , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define $L(n)=\max(\lceil\log_2 n\rceil,1)$ .

Target

The full target is

\mathrm{IntMul.KappaBound}(0.000051016920170078).

This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants $c>0$ and $n_0$ such that every pair of $n$ -bit inputs, for $n\ge n_0$ and $n\ge1$ , halts within

c\,n\,L(n)^{1-0.000051016920170078}

steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger $\kappa$ gives a stronger asymptotic saving because $L(n)\ge1$ .

This entry targets the reviewed PR #62 checkpoint, $\kappa=0.000051016920170078=25508460085039/500000000000000000$ . The pinned repository attributes the selected construction to Avi Eisenberg’s interval strips and core-aware pair assembly, eumemic’s joint frame compiler, and Alejandro Zarzuelo Urdiales’s exact parameter refinement and scoped Lean certificates. Douglas Colkitt maintains the project and its integration. The checkpoint combines a bit network with 575-way branching and 137,151,806 physical roles with the retained complex construction. Its finite arithmetic checks do not prove the complete multiplication algorithm. The full theorem remains an open obligation.

Significance

A proof for any positive value would give a strict asymptotic improvement over $n\log n$ . Such an improvement would contradict the proposed $\Omega(n\log n)$ lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.

Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.

Difficulty

A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.

Formalization scope

The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.

The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.

Selected references

D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2), 563–617 (2021). Paper.
OpenAI, Integer multiplication below n log n, preprint (23 September 2026), pinned manuscript revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source.
D. Colkitt and community contributors, A sharper exponent for integer multiplication, research repository (2026), revision 56b66d58297deca1d7dd130247d720e960f77a37. Checkpoint and attribution.

6 thms3 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

What Can We Learn Privately? II: Parity Functions Are Privately PAC Learnable from O(d log(1/β)/(εα)) ExamplesResearch Paper

Learning parities under differential privacy

Differential privacy (Dwork, McSherry, Nissim and Smith, 2006) requires a randomized algorithm's output distribution to change little when one individual's record is changed. PAC learning asks an algorithm to output, from i.i.d. labeled examples, a hypothesis whose error is small with high probability. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith (arXiv:0803.0924v3; SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090) asked which concept classes can be learned under both requirements at once. All theorem, page and display numbers in this mission are those of the arXiv v3.

Their generic learner (§3, the subject of mission I of this series) learns every finite class privately with a polynomial number of examples, but its running time is exponential in the representation size for classes such as parity. Parity functions are the standard example of a class that is learnable efficiently by linear algebra and not learnable with statistical queries (Kearns, 1998; Blum et al., 1994), a model that was then the main known source of efficient private learners (Blum, Dwork, McSherry and Nissim, 2005). Section 4 of the paper gives an efficient private PAC learner for parity. The result separates efficient private learning from statistical-query learning, and the local (randomized-response) model from the centralized one (missions III–V).

Setting

For $d \ge 1$ and $r \in \{0,1\}^d$ , the parity function $c_r(x) = r \odot x$ is the inner product of $r$ and $x$ modulo 2; PARITY is $\{c_r : r \in \{0,1\}^d\}$ . A database is $z = (z_1,\dots,z_n)$ with $z_i = (x_i, y_i) \in \{0,1\}^d \times \{0,1\}$ . Two databases are neighbors if they differ in exactly one entry. A randomized algorithm $A$ , identified with the law $A(z)$ of its output, is $\varepsilon$ -differentially private if $\Pr[A(z) \in S] \le e^{\varepsilon}\Pr[A(z') \in S]$ for all neighbors $z, z'$ and all sets $S$ of outputs. $\mathrm{Lap}(s)$ is the Laplace distribution with density $\frac{1}{2s}e^{-|x|/s}$ .

For $S \subseteq [n]$ , $V_S \subseteq \mathbb Z_2^d$ is the solution space of the linear system $\{x_i \odot r = y_i : i \in S\}$ . The basic learner $\mathcal A(z,\varepsilon)$ outputs $\bot$ with probability $1/2$ ; otherwise it puts each $i \in [n]$ into $S$ independently with probability $p = \varepsilon/4$ and outputs $c_{r^*}$ for $r^*$ uniform in $V_S$ , or $\bot$ if $V_S = \emptyset$ .

The amplified learner $\mathcal A^*(z,\varepsilon,\alpha,\beta)$ sets $\beta' = \beta/2$ , $\alpha' = \alpha/5$ , $k = \lceil\log_{4/3}(1/\beta')\rceil$ , $n' = \lceil cd/(\varepsilon\alpha')\rceil$ , $s = \lceil (c'k/(\alpha'\varepsilon))\log_2(k/\beta')\rceil$ for constants $c, c'$ . If $n \le kn' + s$ it returns "insufficient samples". Otherwise it runs $\mathcal A$ on $k$ disjoint blocks of $n'$ examples, obtaining $h_1,\dots,h_k$ . It perturbs each training error on the next $s$ examples by independent $\mathrm{Lap}(k/(s\varepsilon))$ noise and outputs the $h_j$ with the least perturbed error.

For a distribution $\mathcal X$ on $\{0,1\}^d$ and a target $c_r$ , the error of $c_{r'}$ is $\mathrm{err}(c_{r'}) = \Pr_{x\sim\mathcal X}[c_{r'}(x) \ne c_r(x)]$ , and probabilities of the learner's success are over $x_1,\dots,x_n \sim \mathcal X$ i.i.d., $z_i = (x_i, c_r(x_i))$ , and the learner's coins.

Formalization targets

Goal: Theorem 4.4

There are constants $c, c', C > 0$ such that for all $d \ge 1$ , $0 < \varepsilon \le 1/2$ , $\alpha, \beta \in (0,1/2)$ : $\mathcal A^*(\cdot,\varepsilon,\alpha,\beta)$ is $\varepsilon$ -differentially private on databases of every size, and

n \ge C\,\frac{(d + \log_2(1/\beta))\log_2(1/\beta)}{\varepsilon\alpha} \implies \Pr\big[\mathcal A^* \text{ outputs } h^* \text{ with } \mathrm{err}(h^*) \le \alpha\big] \ge 1-\beta

for every distribution $\mathcal X$ and every target $c_r$ . When $\log_2(1/\beta) \le d$ the bound is the paper's $O(d\log(1/\beta)/(\varepsilon\alpha))$ . The constants are fixed before all other parameters. The goal is literally the conjunction of Lemma 4.5 and Lemma 4.6.

Milestones

\text{Thm 2.3 (Laplace mechanism)},\quad \text{Claim 2.2 (composition)},\quad \text{Thm A.1 (Chernoff)},\quad \text{Occam's razor for } |H| = 2^d,

\text{Lemma 4.1: } n \ge \tfrac{8}{\varepsilon\alpha}(d\ln 2 + \ln 4) \Rightarrow \Pr[\mathcal A(z,\varepsilon) = h,\ \mathrm{err}(h)\le\alpha] \ge \tfrac14,

|V_T| \le 2|V_{T\cup\{i\}}| \text{ if } V_{T\cup\{i\}} \ne \emptyset,\quad \text{Claim 4.3},\quad \text{Lemma 4.2 (}\mathcal A\text{ private)},\quad \text{Lemma 4.5 (}\mathcal A^*\text{ private)},\quad \text{Lemma 4.6 (}\mathcal A^*\text{ learns)}.

Significance

The theorem shows that the restriction to private algorithms does not separate efficient learnability from statistical-query learnability: parity is efficiently and privately PAC learnable, yet not SQ learnable. Its sample complexity exceeds the non-private $O((d + \ln(1/\beta))/\alpha)$ by a factor $O(\ln(1/\beta)/\varepsilon)$ (remark, p. 18). The private amplification step (private model selection with Laplace-perturbed test errors) is a general technique that converts any private learner with constant success probability into a private PAC learner.

The result is proved in the paper; none of it is machine-checked as far as we know. The mission produces a formal library of the basic privacy calculus (Laplace mechanism, composition and post-processing), the $\mathbb Z_2$ solution-space estimate behind the privacy of $\mathcal A$ , and the analysis of both learners. Formalizing it also repairs the paper's statement: the printed sample bound fails when $\log(1/\beta)$ is large compared with $d$ (see the scope section), and the base of the logarithm defining $k$ is misprinted.

Difficulty

The obvious private learner, "solve the linear system on all examples and output a random solution", is not private. One changed example can make the system inconsistent and turn every hypothesis output into failure, so the output law on neighboring databases differs by an unbounded factor. Two devices restore privacy: subsampling each example with probability $\varepsilon/4$ , and failing with probability $1/2$ unconditionally. The privacy proof then needs a quantitative fact about $\mathbb Z_2$ : adding one consistent equation at most halves the solution space. The proof must also handle databases labeled by no parity at all, where solution spaces are empty.

Utility has its own difficulty. The amplified learner selects among candidates through noisy test errors, so three failure events (no good candidate, unrepresentative test set, large Laplace noise) must be bounded together. The sizes $k$ , $n'$ , $s$ must also be shown to fit inside the claimed sample bound.

Formalization scope

Bits are ZMod 2; $\{0,1\}^d$ is Fin d → ZMod 2; $c_r(x)$ is dotProduct r x. Databases are Fin n → (Fin d → ZMod 2) × ZMod 2, with 0-based indices.
An algorithm is the law of its output. $\mathcal A$ 's output is Option (Fin d → ZMod 2) (none = $\bot$ ). $\mathcal A^*$ 's output is "insufficient samples", $\bot$ , or a hypothesis $c_r$ . Every set of outputs is measurable, and differential privacy is required for all measurable sets.
The distribution $\mathcal X$ is a PMF on the finite set $\{0,1\}^d$ . The probability over the examples is a finite sum weighted by $\prod_i \mathcal X(x_i)$ , and $\bot$ has error 1.
Corrections and explicit hypotheses. (1) $k = \lceil\log_{4/3}(1/\beta')\rceil$ : the printed base $3/4$ gives $k \le 0$ , and the proof needs $(3/4)^k \le \beta'$ . (2) Sizes are ceilings; $\log$ is base 2 and $\ln$ is natural, as on p. 8. (3) Privacy is stated for $0 < \varepsilon \le 1/2$ : the proof of Lemma 4.2 uses $\varepsilon \le 1/2$ , and its step $2p/(1-p) + 1 \le \varepsilon + 1$ fails beyond that. Utility statements need only $0 < \varepsilon \le 4$ , so that $p = \varepsilon/4$ is a probability. (4) The printed bound $O(d\log(1/\beta)/(\varepsilon\alpha))$ is false when $\log(1/\beta) \gg d$ , because $\mathcal A^*$ refuses unless $n > kn' + s$ and $s$ grows like $\log^2(1/\beta)/(\varepsilon\alpha)$ . Utility is therefore stated with the bound $C(d + \log_2(1/\beta))\log_2(1/\beta)/(\varepsilon\alpha)$ , the order of $kn' + s$ , which equals the printed order whenever $\log_2(1/\beta) \le d$ . The privacy conjunct does not depend on the sample bound. (5) A $\bot$ candidate does not take part in the argmin, and ties go to the least index. (6) Lemma 4.1 assumes $\alpha \le 1/2$ , which its proof uses. (7) Claim 4.3 is stated in product form (no division). (8) Theorem 2.3 takes any positive bound $\Delta$ on the global sensitivity.
"Efficiently" (polynomial running time) is not modelled.
Ruling out trivial readings. The constants $c, c', C$ are existentially quantified once, outside every other quantifier. A constant chosen after $d$ , $\varepsilon$ , $\alpha$ , $\beta$ would make the utility claim trivial. Success requires an actual hypothesis output, so "insufficient samples" and $\bot$ are failures. Privacy quantifies over all databases, not only consistently labeled ones.
Reused results: ComputationalLearning.chernoff_bounds (Theorem A.1) and ComputationalLearning.occam_cardinality (Occam's razor), both proved on the platform.
Contributions welcome: proofs of the privacy calculus (Theorem 2.3, Claim 2.2) for general use, the $\mathbb Z_2$ halving lemma, and the utility analysis. The first two are reusable well beyond this mission.

Selected references

S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090
C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. DOI 10.1007/11681878_14
A. Blum, C. Dwork, F. McSherry, K. Nissim, Practical Privacy: The SuLQ Framework, PODS 2005. DOI 10.1145/1065167.1065184
M. Kearns, Efficient Noise-Tolerant Learning from Statistical Queries, J. ACM 45(6) (1998) 983–1006. DOI 10.1145/293347.293351
A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly Learning DNF and Characterizing Statistical Query Learning Using Fourier Analysis, STOC 1994. DOI 10.1145/195058.195147
M. Kearns, U. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994. DOI 10.7551/mitpress/3897.001.0001

14 thms3 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

What Can We Learn Privately? I: The Exponential Mechanism Privately Agnostically Learns Any Finite Concept Class from O((ln|C| + ln(1/β))·max{1/(εα), 1/α²}) ExamplesResearch Paper

Motivation

Many learning tasks run on data about people: medical records, purchase histories, survey answers. A learner whose output reveals too much about any one training example is unusable on such data, however accurate it is. Differential privacy (Dwork, McSherry, Nissim and Smith, 2006) makes "reveals too much" precise: changing one individual's record may change the probability of any outcome of the algorithm by at most a factor $e^{\varepsilon}$ .

Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith asked which concept classes can be learned under this constraint, and at what cost in examples. This mission formalizes their first answer (§3 of the paper): every finite concept class can be learned privately in the agnostic model, with a sample size that grows only logarithmically in the size of the class. The result is the private counterpart of the cardinality version of Occam's razor (Kearns and Vazirani, An Introduction to Computational Learning Theory, 1994, p. 35). The paper appeared in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; all indices below are those of arXiv:0803.0924v3.

The learner is an instance of the exponential mechanism of McSherry and Talwar (FOCS 2007), which selects an output with probability exponentially weighted by a quality score.

Setting

A database of size $n$ over a domain $D$ is a vector $z=(z_1,\dots,z_n)\in D^n$ . Databases $z,z'$ are neighbors if they differ in exactly one entry. A randomized algorithm $A$ is described by the law $A(z)$ of its output on each input. It is $\varepsilon$ -differentially private (Definition 2.1) if

\Pr[A(z)\in S]\le e^{\varepsilon}\Pr[A(z')\in S]

for all neighbors $z,z'$ and all measurable sets $S$ of outputs.

Learning uses a finite set $X$ of examples and labels $\{0,1\}$ . A hypothesis is a map $h:X\to\{0,1\}$ , and $H$ is a finite nonempty class of hypotheses; in the theorem $H=C_d$ , the concept class itself. Data are drawn i.i.d. from an arbitrary probability distribution $P$ on $X\times\{0,1\}$ (the agnostic setting, Definition 2.5). The error of $h$ is $\mathrm{err}(h)=\Pr_{(x,y)\sim P}[h(x)\neq y]$ , and $\mathrm{OPT}=\min_{f\in H}\mathrm{err}(f)$ . On a database $z=((x_i,y_i))_{i\le n}$ the score is $q(z,h)=-|\{i:y_i\neq h(x_i)\}|$ and the training error is $\mathrm{err}_T(h)=-q(z,h)/n$ .

The exponential mechanism $\mathcal A^{\varepsilon}_q$ outputs $h\in H$ with probability proportional to $\exp(\varepsilon q(z,h)/2)$ . In Lean these objects are IsDP, err, OPT, score, errT and expMech in the namespace PrivLearn.Generic.

Formalization targets

Goal: Theorem 3.4 (generic private learner)

There is an absolute constant $C>0$ such that for every finite $X$ , every finite nonempty $H$ , every $\varepsilon>0$ and all $\alpha,\beta\in(0,1/2)$ :

$\mathcal A^{\varepsilon}_q$ is $\varepsilon$ -differentially private on databases of every size;
for every distribution $P$ on $X\times\{0,1\}$ and every

n\ \ge\ C\Big(\ln|H|+\ln\tfrac1\beta\Big)\max\Big\{\tfrac1{\varepsilon\alpha},\tfrac1{\alpha^2}\Big\},

the mechanism run on $n$ i.i.d. samples from $P$ satisfies

\Pr\big[\mathrm{err}(\mathcal A^{\varepsilon}_q(z))>\mathrm{OPT}+\alpha\big]\le\beta .

The constant is left unspecified, as the paper's $O(\cdot)$ leaves it. The qualitative first sentence of Theorem 3.4 (classes of size $\exp(\mathrm{poly}(d))$ are privately agnostically learnable) follows at once, because then $\ln|H|$ is polynomial in $d$ .

Milestones

Lemma 3.3: $\mathcal A^{\varepsilon}_q$ is $\varepsilon$ -differentially private.
Theorem A.2: for i.i.d. $X_i\in[a,b]$ with mean $\mu$ , $\Pr[|\frac1n\sum_iX_i-\mu|\ge\delta]\le2\exp(-2\delta^2n/(b-a)^2)$ .
Uniform convergence (proof of Theorem 3.4, p. 11): $\Pr[\exists h\in H:\ |\mathrm{err}(h)-\mathrm{err}_T(h)|\ge\rho]\le2|H|e^{-2n\rho^2}$ .
Exponential weights (proof of Theorem 3.4, p. 12): if $|\mathrm{err}(h)-\mathrm{err}_T(h)|<\rho$ for all $h\in H$ , then $\mathcal A^{\varepsilon}_q(z)$ outputs some $h$ with $\mathrm{err}_T(h)\ge\mathrm{OPT}+2\rho$ with probability at most $|H|e^{-\varepsilon n\rho/2}$ .
Corollary 3.6: the same guarantee with $\ln|H|$ replaced by $\mathrm{VCDIM}(C_d)\cdot\ln|X|$ .

Significance

Theorem 3.4 shows that privacy costs little in sample complexity when computation is unconstrained. Any class that some learner with polynomially long output can learn is learnable privately from polynomially many examples. The non-private agnostic bound is $O((\log|C_d|+\log(1/\beta))/\alpha^2)$ ; the private one is larger by a factor $O(\alpha/\varepsilon)$ when $\alpha>\varepsilon$ , and is the same otherwise (Remark, p. 12). The theorem is the baseline the rest of the paper refines: an efficient private learner for parity (§4) and the equivalence of local privacy with statistical query learning (§5). It also underlies later work on the sample complexity of private learning, such as Beimel, Kasiviswanathan and Nissim (TCC 2010).

The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a checked statement of the exponential mechanism's privacy and of its learning guarantee with an explicit dependence on $|H|$ , $\varepsilon$ , $\alpha$ and $\beta$ . It also provides a reusable bounded i.i.d. Hoeffding inequality (Theorem A.2) in the form learning theory uses. Formalizing the proof with any explicit constant is welcome. The constant $6$ printed at the end of the proof does not, by itself, make the last inequality close (the two error terms add to more than $\beta$ ), so a correct constant is a genuine contribution.

Difficulty

Privacy and accuracy pull in opposite directions. Empirical risk minimization, the obvious learner, is not private: replacing one example can change which hypothesis minimizes the training error, and the output then changes with probability one. Smoothing the choice must not destroy accuracy, and the accuracy argument must hold simultaneously for every hypothesis in the class, with the mechanism's randomness and the sample's randomness combined into one failure probability. In Lean the measure-theoretic bookkeeping is non-trivial: the output is a measure on a function space, the failure probability integrates the mechanism's law against the product measure $P^n$ , and the privacy bound must hold for every measurable event, not only for single hypotheses.

Formalization scope

Databases are vectors Fin n → X × Bool, indexed from $0$ ; neighbors differ in exactly one coordinate.
Algorithms are output laws: $\mathcal A^{\varepsilon}_q(z)$ is the measure $\sum_{h\in H}p_z(h)\,\delta_h$ on X → Bool with the product σ-algebra. It is a probability measure because $H$ is nonempty and all weights are positive; the theorems assume $H$ nonempty, and the definition does not build normalization in.
Privacy is required on every measurable set of outputs and for every database size $n$ , with no assumption on how the data arise.
The example domain is a finite type with the discrete σ-algebra (the paper's $X_d$ has representations of size at most $d$ ). The goal quantifies it over Type so that the absolute constant can precede it.
Labels are Bool, standing for $\{0,1\}$ . Logarithms are natural (Real.log), as in the paper's $\ln$ .
Parameters are $\varepsilon>0$ and $\alpha,\beta\in(0,1/2)$ as in Definitions 2.4 and 3.1. The failure event is the strict $\mathrm{err}(h)>\mathrm{OPT}+\alpha$ , as on p. 11, and OPT is the minimum over $H=C_d$ .
$O(\cdot)$ is formalized as one absolute constant $C>0$ quantified before the domain, the class, the distribution and all parameters. A constant chosen after them would make the statement trivially true.
Theorem A.2 assumes measurable, mutually independent, pairwise identically distributed variables with values in $[a,b]$ at every point. It makes no assumption $n\ge1$ or $a<b$ ; in those cases the right side is $2$ by Lean's division conventions.
Corollary 3.6 uses the platform's VC dimension ComputationalLearning.vcDim (Kearns–Vazirani's Definition 9, the same notion as the paper's Definition 3.5) and references the platform's proved Sauer lemma.

Contributions welcome: proofs of any milestone, a measurable-structure library for finite output laws, and a general exponential-mechanism privacy theorem from which Lemma 3.3 follows.

Selected references

S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090
C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. DOI 10.1007/11681878_14
F. McSherry, K. Talwar, Mechanism Design via Differential Privacy, FOCS 2007. DOI 10.1109/FOCS.2007.66
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. DOI 10.1080/01621459.1963.10500830
M. Kearns, U. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994. DOI 10.7551/mitpress/3897.001.0001
A. Beimel, S. P. Kasiviswanathan, K. Nissim, Bounds on the Sample Complexity for Private Learning and Private Data Release, TCC 2010. DOI 10.1007/978-3-642-11799-2_26

10 thms3 active usersReviewed

Completed

Complexity Theory Operations Research Optimization·Captain: mikedeng1

Convex Quadratic and Semidefinite Programming Relaxations in Scheduling V: 3-Occurrence Max3Sat L-Reduces to R | rⱼ | Σ Cⱼ with Constants 32 and 1Research Paper

Motivation

The scheduling problem $R\,|\,r_j\,|\sum C_j$ asks for a nonpreemptive schedule of jobs on unrelated parallel machines, each job with a machine-dependent processing time and a release date, so that the total completion time is minimal. It is NP-hard, and the question that remains is how well it can be approximated in polynomial time. Positive results include the 2-approximation of Skutella (J. ACM 2001), based on a convex quadratic relaxation. This mission covers the negative side, from §7 of the same paper: the problem has no polynomial-time approximation scheme unless P = NP.

The standard route to such a statement is an L-reduction (Papadimitriou and Yannakakis 1991) from a problem already known to be MaxSNP-hard. MaxSNP-hard problems have no approximation scheme unless P = NP, by the PCP theorem (Arora et al. 1998).

Timeline.

1991: Papadimitriou and Yannakakis define MaxSNP and L-reductions, and show that MAX3SAT with a bounded number of occurrences per variable is MaxSNP-complete.
1998: Hoogeveen, Schuurman and Woeginger prove that $R\,|\,|\sum w_jC_j$ and $R\,|\,r_j\,|\sum C_j$ are MaxSNP-hard, by a reduction from a MaxSNP-hard variant of 3-dimensional matching.
2001: Skutella (§7, pp. 32–33) gives a shorter reduction from 3-OCCURRENCE MAX3SAT, the variant of MAX3SAT in which every variable occurs at most three times (MaxSNP-hard, see Ausiello et al. 1999, Corollary 8.15).

Setting

An instance $I$ of 3-OCCURRENCE MAX3SAT has $n$ variables and $m$ clauses. Each clause is a set of one to three literals (a variable $x$ or its negation $\neg x$ ), and each variable occurs at most three times in total. A truth assignment $t$ gives each variable the value true or false and satisfies a clause when one of the clause's literals is true. $\#(t)$ denotes the number of satisfied clauses, and $\mathrm{OPT}_{\mathrm{SAT}}(I)=\max_t \#(t)$ .

The scheduling instance $R(I)$ has $n+m$ jobs and $2n$ machines.

Every variable $x$ has a true machine and a false machine, and one v-job. The v-job is released at time $0$ , has processing time $4$ on the two machines of $x$ , and cannot run anywhere else.
Every clause $c$ has one c-job, released at time $3$ , with processing time $0$ . It may run on the false machine of $x$ when $x$ occurs in $c$ , on the true machine of $x$ when $\neg x$ occurs in $c$ , and nowhere else.

A schedule $S$ gives every job $j$ a machine and a start time $S_j\ge r_j$ , with no two jobs on one machine overlapping. Its value is the total completion time $\mathrm{VAL}(S)=\sum_j (S_j+p_j)$ . The truth assignment $\mathrm{SAT}(S)$ sets $x$ true exactly when the v-job of $x$ runs on the true machine. $\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ is the minimum of $\mathrm{VAL}$ over feasible schedules.

Formalization targets

Goal: the L-reduction inequalities (Lemma 7.1 b) and the proof of Theorem 7.2, p. 33)

$R(I)$ has an optimal schedule $S_0$ , and

\mathrm{VAL}(S_0)=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I),\qquad \mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{VAL}(S_0)

for every feasible schedule $S$ . These are the two conditions of an L-reduction, with constants $\alpha=32$ and $\beta=1$ .

Milestones

Lemma 7.1 a) (p. 32): $\#(\mathrm{SAT}(S))\ge 4n+4m-\mathrm{VAL}(S)$ for every feasible $S$ .
Lemma 7.1 b) (p. 33): $\mathrm{OPT}_{\mathrm{SCH}}(R(I))=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)$ .
The two counting facts of the proof of Theorem 7.2: $\mathrm{OPT}_{\mathrm{SAT}}(I)\ge m/2$ and $n\le 3m$ .
The first L-reduction condition: $\mathrm{OPT}_{\mathrm{SCH}}(R(I))\le 12m+4m\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I)$ .
The second L-reduction condition: $\mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ .

Significance

The result. The two inequalities are what an L-reduction requires. Combined with the MaxSNP-hardness of 3-OCCURRENCE MAX3SAT, they show that $R\,|\,r_j\,|\sum C_j$ is MaxSNP-hard (Theorem 7.2, due to Hoogeveen, Schuurman and Woeginger), and therefore has no polynomial-time approximation scheme unless P = NP. Together with the constant-factor algorithms of the earlier sections of the paper, this places the problem in APX but outside PTAS. The identity of Lemma 7.1 b) is exact, so the reduction transfers solutions in both directions with no loss beyond the affine shift $k\mapsto 4n+4m-k$ .

Formalizing it. The result is proved, on paper, by both the 1998 and the 2001 reductions. As far as the platform's corpus shows, neither is machine-checked. This mission produces a checked version of the combinatorial core of Skutella's reduction: the exact relation between optimal schedules of $R(I)$ and optimal truth assignments of $I$ , and the two L-reduction constants. A Lean model of 3-OCCURRENCE MAX3SAT and of nonpreemptive schedules with release dates and machine eligibility is a by-product.

Difficulty

The obvious argument is the paper's intuition: given a truth assignment, a c-job can start at time $3$ without conflicting with a v-job exactly when its clause is satisfied. That is not enough for Lemma 7.1 a), which concerns every feasible schedule. In an arbitrary schedule a v-job may be delayed so that c-jobs of unsatisfied clauses run before it on its machine, and v-jobs and c-jobs may start at arbitrary real times. To compare such a schedule with a normalized one, its total completion time has to be bounded from below by $4n+4m-\#(\mathrm{SAT}(S))$ . The bound depends on the occurrence limit of three, which caps how many c-jobs can share a machine with a given v-job; without that limit Lemma 7.1 a) is false. Lemma 7.1 b) also needs the existence of an optimal schedule, which the paper takes for granted.

Formalization scope

Variables and clauses are Fin n and Fin m; here $n$ and $m$ count variables and clauses, not jobs and machines as in the rest of the paper. A literal is a pair (x, b) with b = true for $x$ and b = false for $\neg x$ , and a clause is a Finset of literals. Jobs are Fin n ⊕ Fin m and machines Fin n × Bool. Infinite processing times are encoded by an eligibility relation. Start times are real numbers, and $\mathrm{VAL}$ is a real number; $\#$ and $\mathrm{OPT}_{\mathrm{SAT}}$ are natural numbers cast to the reals, so no natural-number subtraction occurs. $\mathrm{OPT}_{\mathrm{SCH}}$ is never a primitive: statements assert, or assume, a feasible schedule that is no worse than every feasible schedule.

Two conventions are fixed that the page leaves implicit:

Every clause has between one and three literals. An empty clause would leave its c-job with no machine, so $R(I)$ would have no schedule, and "at least $m/2$ " would fail.
Every variable occurs at least once. The bound $n\le 3m$ , and with it the constant $32$ , needs this: a variable that occurs nowhere adds $4$ to $\mathrm{OPT}_{\mathrm{SCH}}$ and nothing to $\mathrm{OPT}_{\mathrm{SAT}}$ .

Zero-length jobs need a precise non-overlap rule. Two distinct jobs on one machine must satisfy $S_j+p_j\le S_k$ or $S_k+p_k\le S_j$ . Under this rule a c-job at time $3$ conflicts with a v-job running over $[0,4)$ , but several c-jobs may share a start time. Reading jobs as half-open intervals $[S_j,S_j+p_j)$ would let a zero-length c-job sit inside a v-job, so every clause would count as satisfied: that formalization is ruled out.

Not formalized: MaxSNP, MaxSNP-hardness and Theorem 7.2's statement itself; the definition of an L-reduction as a pair of polynomial-time maps; the polynomial running time of $R$ and $\mathrm{SAT}$ ; the weighted variant for $R\,|\,|\sum w_jC_j$ in the last paragraph of §7, which the paper does not prove. Contributions are welcome on the counting facts, on a normal form for schedules of $R(I)$ (v-jobs at time $0$ , c-jobs at time $3$ or $4$ ), and on the existence of optimal schedules.

Selected references

M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2), 206–242, 2001. https://doi.org/10.1145/375827.375840
J. A. Hoogeveen, P. Schuurman, G. J. Woeginger, Non-approximability results for scheduling problems with minsum criteria, IPCO 1998, LNCS 1412, 353–366. https://doi.org/10.1007/3-540-69346-7_27
C. H. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
G. Ausiello, P. Crescenzi, G. Gambosi, V. Kann, A. Marchetti-Spaccamela, M. Protasi, Complexity and Approximation, Springer, 1999. https://doi.org/10.1007/978-3-642-58412-1
S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306

7 thms3 active usersReviewed

Completed

Machine Learning Operations Research·Captain: mikedeng1

The Weighted Majority Algorithm 4: The Continuous Master WMC Has Total Absolute Loss at Most ln(w_init/w_fin)/(1−β)Research Paper

Motivation

In sequential prediction, several forecasters can issue different answers for the same instance. A master algorithm must combine their advice before the true label is known. Littlestone and Warmuth's Weighted Majority framework gives worst-case guarantees for this setting: the instances and labels need not come from a probability distribution. The paper first studies binary predictions and then allows real predictions and labels in the unit interval. The continuous version matters when the distance between a prediction and a label carries information that a binary mistake count discards. The formal target here is the paper's total absolute-loss guarantee for that continuous master, WMC (Littlestone and Warmuth 1994, §5).

The result is part of the paper's generalized analysis, which also covers a binary master WMG and a randomized master WMR. These algorithms share a range of allowed weight updates, but their predictions and losses differ. This mission isolates WMC's deterministic, continuous-label theorem and the numbered lemmas on which its statement rests. The finite-sequence convention is explicit in the paper's notations and assumptions (Littlestone and Warmuth 1994, p. 220).

Setting

Fix a finite nonempty pool of $n$ forecasters and a finite sequence of $t$ trials. At trial $j$ , expert $i$ predicts $x_i^{(j)}\in[0,1]$ , and after the master predicts, a label $\rho^{(j)}\in[0,1]$ is revealed. Expert $i$ has weight $w_i^{(j)}$ before that trial. Every initial weight is positive, and weights remain nonnegative. The total weight and weighted mean prediction are

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

WMC predicts $\gamma^{(j)}$ . Its loss on the trial is the absolute error $|\gamma^{(j)}-\rho^{(j)}|$ , and its total absolute loss is $m=\sum_{j=1}^{t}|\gamma^{(j)}-\rho^{(j)}|$ . Write $w_{\mathrm{init}}=s^{(1)}$ and $w_{\mathrm{fin}}=s^{(t+1)}$ for total weight before the first and after the final update (Littlestone and Warmuth 1994, pp. 232–233).

WMC updates on every trial. For $0\le\beta<1$ , it multiplies each weight by a factor $F_i^{(j)}$ in the interval

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

The factor may depend on both trial and expert. The paper permits any choice in this interval, so WMC denotes a class of runs rather than one fixed recurrence. Its convention $0^0=1$ is used when $\beta=0$ and an expert has zero error (Littlestone and Warmuth 1994, p. 233, eq. (5.1)).

Formalization targets

Theorem 5.2: WMC total loss

For every run with positive final total weight, the target is the paper's explicit inequality

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

The bound uses the run's actual initial and final weights, so it applies whether the upper or lower permitted update factor was selected, or a factor between them. The finite-valued statement assumes $w_{\mathrm{fin}}>0$ ; the paper regards the bound as vacuous when the denominator of the logarithm is zero (Littlestone and Warmuth 1994, p. 236, Theorem 5.2).

Supporting numbered results

Lemma 5.1 states $\beta^r\le1+r(\beta-1)$ for $\beta\ge0$ and $0\le r\le1$ , ensuring the update interval is nonempty. Lemma 5.2 states the logarithmic potential estimate under only the update's upper inequality, including the special case in which $\beta=0$ and a master's unit loss forces the final total weight to zero. Lemma 5.3 turns those same conditions into the displayed total-loss bound. Each is a separate milestone with the paper's statement and page provenance (Littlestone and Warmuth 1994, pp. 233–236).

Significance

The theorem controls the master's accumulated real-valued prediction error by an observable change in the total pool weight. It requires no distributional assumption on the trial sequence and no single choice of update factor. That breadth lets the same estimate be used for different update rules within the allowed range, while the explicit $1/(1-\beta)$ constant records the dependence on the algorithm's parameter. The paper also uses Lemma 5.3 in its analysis of WMR's expected loss (Littlestone and Warmuth 1994, pp. 236, 240).

The paper proves these results; this mission asks for machine-checked proofs of their exact Lean statements. Its definition of a permitted continuous run and its upper-update potential conditions can also support subsequent formalizations of WMG and WMR. Lemma 5.1, the potential estimate, and the final loss bound remain distinct proof targets so that a solver can use or improve the underlying analytic infrastructure without changing the goal.

Difficulty

A binary mistake indicator cannot express the magnitude of an error between two unit-interval values. The generalized update contains a real exponent, absolute values, and a range of legal factors. An argument that handles only a selected endpoint of that range would leave permitted WMC runs uncovered. A further boundary occurs at $\beta=0$ : an allowed update can reduce a positive weight to zero, and real logarithms in Lean have a defined value at zero although the paper's logarithmic bound is infinite there. The formal statements therefore distinguish the zero-final-weight clause from the finite-logarithm clause.

Formalization scope

The pool is Fin n with $n>0$ and the trials are Fin t; an empty sequence of trials is allowed. Lean's trial index starts at zero, so w 0 represents $w^{(1)}$ and w t represents the weights after all $t$ trials. The inputs are the prediction array and label array. Instances are not stored separately because the theorem refers to them only through expert predictions. Values, factors, totals, and losses are real numbers. The run predicate requires positive initial weights, nonnegative weights, predictions and labels in $[0,1]$ , $0\le\beta<1$ , and a permitted factor for every expert on every trial.

The theorem quantifies over every permitted run. A sorry-free local example exhibits a one-trial run with positive final weight, ruling out a globally empty run predicate. For positive final weight, the update conditions ensure earlier total weights are positive, so every weighted mean used in the loss has its intended denominator. The finite logarithmic conclusions assume positive final weight because Real.log 0 would otherwise introduce an unrelated total-function value. The definition layer supplies total weight, weighted mean, loss, base conditions, the upper-update conditions, and WMC runs; the proof development needs finite-sum and real logarithm inequalities from Mathlib. Contributions that establish the three numbered lemmas or the goal under this interface are in scope.

Selected references

Nick Littlestone and Manfred K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. DOI: 10.1006/inco.1994.1009.

6 thms3 active usersReviewed

Completed

Combinatorics·Captain: marwahaha

3SUM in O(n^1.999074) Time on a Word RAMOpen Problem

Prove a deterministic $O(n^{1.999074})$ algorithm for integer 3SUM in the campaign's shared word-RAM model, improving the verified $1.999112$ bound.

A promising parameter choice is $c=22$ , $\theta=0.11229$ , $D=\lfloor n^{0.054}\rfloor$ , and $g=\lceil D^{0.0343}\rceil$ . Lean-checked arithmetic certificates give $\gamma>0.0686$ , $q\le0.431369<0.4314$ , and $0.054<R_c$ . The predicted Exact Triangle saving is $\delta=0.0018522$ , giving a 3SUM cutoff of $1.9990739$ and a strict margin below the target.

The algorithmic claim remains open. The milestones are to establish the faster inner solver, then verify the integer computations for $D$ and $g$ and prove the total Exact Triangle cost, including preprocessing and scans. The existing verified reductions and foundation definitions can then be reused. The numerical certificates alone do not prove the mission.

41 thms3 active usersReviewed

Completed

Combinatorics Number Theory Probability·Captain: mikedeng1

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

Motivation

A pseudorandom number generator replaces repeated random sampling with a deterministic update of a small state. Its useful lifetime depends on the length and structure of the resulting orbit. In Marsaglia and Zaman’s 1991 paper, the subtract-with-borrow generators use only digit subtraction and a one-bit borrow while attaining cycles that can be almost as long as the whole set of digit tuples. The mathematical question is exact: which fraction encodes an output sequence, when does an arbitrary seed enter a cycle, and how long is that cycle?

This mission concerns the paper’s first subtract-with-borrow rule, called Method 1 in §4.5. The paper also studies a second rule that reverses the order of the two subtracted digits. Its modulus and period analysis differ. The distinction matters because the same state format supports both rules while their arithmetic claims are different.

Setting

Choose an integer base $b\ge2$ and lags $0<s<r$ . A state is a row of $r$ digits and one borrow bit, $(x_1,\ldots,x_r,c)$ , where each $x_i$ is in $\{0,\ldots,b-1\}$ and $c\in\{0,1\}$ . The leftmost digit $x_1$ is the oldest. One update discards it, shifts the remaining digits left, and appends a new digit. Put $t=x_{r+1-s}-x_1-c$ . If $t\ge0$ , the appended digit is $t$ and the new borrow is zero. If $t<0$ , the appended digit is $t+b$ and the new borrow is one. Write this deterministic map as $f$ .

The digits emitted after the seed obey $x_n=x_{n-s}-x_{n-r}-c$ modulo $b$ , with $c$ updated at each step. The associated modulus is $m=b^r-b^s+1$ . For $0\le k<m$ , write $d_j(k/m)$ for the $j$ th digit after the point in the base- $b$ expansion of $k/m$ , with $j\ge1$ . The digit stream is read in reverse order when it is matched to an expansion: the latest generated digit in a finite block is the first fractional digit. A state is strictly periodic when it is already on a cycle under $f$ ; otherwise it may pass through a transient before reaching one.

Two states have period one: $(0,\ldots,0,0)$ and $(b-1,\ldots,b-1,1)$ . These are the trivial seeds. They are exceptions to the order-of-base period formula. A third useful object is the multiplicative order $\operatorname{ord}_m(b)$ , the least positive $p$ for which $b^p\equiv1\pmod m$ . Since $m\equiv1\pmod b$ , the base is coprime to this modulus.

Formalization targets

Exact cycle period

For prime $m=b^r-b^s+1$ and any nontrivial seed $z$ , the goal identifies the minimal state period after the transient:

\operatorname{period}_f\bigl(f^r(z)\bigr)=\operatorname{ord}_m(b).

The assertion includes both that $f^r(z)$ is on a cycle and that its period is exactly the order. It makes no primitive-root assumption. If $b$ is a primitive root modulo $m$ , the right side specializes to $m-1=b^r-b^s$ , the full period discussed in §3 of the paper.

Supporting results

The milestones state that the fractional digits of $k/m$ have least period $\operatorname{ord}_m(b)$ when $k$ and $b$ are coprime to $m$ ; that a primitive root yields digit period $m-1$ ; that the two trivial seeds are precisely the fixed points; and that every seed reaches a cycle after at most $r$ updates. They also formalize the reverse-digit relation for every finite generated block and the paper’s Method 1 inequalities that classify nontrivial seeds already on a cycle. These targets use the paper’s own claims in §§4.1, 4.3, and 4.5 rather than an arbitrary decomposition of the goal.

Significance

The result converts the orbit-length problem of a digit-and-borrow machine into a multiplicative-order calculation in a finite residue ring. A prime modulus and a primitive base produce a nontrivial cycle of length $m-1$ ; a nonprimitive base still has the exact order-of-base period. The seed classification separates states already on that cycle from states with an initial transient. These statements are what allow a proposed numerical parameter set to be assessed mathematically before the generator is used.

Marsaglia and Zaman proved these results in the cited paper. This mission asks for machine-checked Lean proofs of the statements, starting from an explicit finite-state update. The reusable output includes exact base- $b$ digit arithmetic, links between digit periods and multiplicative order, and methods for reasoning about the eventual cycles of finite-state digit generators. The present proposal consists of compiled statements and definitions; the theorem bodies are open proof targets.

Difficulty

Finiteness alone shows that every state eventually repeats, but it gives neither the bound of $r$ steps nor the exact cycle length. Likewise, observing that a generated digit block matches a prefix of some fraction does not by itself identify one period for the whole state orbit. The proof must keep track of the borrow bit and the direction in which the digit block is read. It must also show that a nontrivial seed does not collapse to one of the two fixed states. The source’s integer tableaux explain the arithmetic link, but turning their finite strings into a statement uniform over every seed and every block length is the main formalization challenge.

Formalization scope

Lean represents digits by Fin b, the borrow by Fin 2, and the row by a function on Fin r. Lean index zero is $x_1$ , so the digit used in the update, $x_{r+1-s}$ , has index $r-s$ . The update branches on an ordinary integer comparison before any natural-number subtraction can truncate a negative value. The modulus is a natural number, and $0<s<r$ with $b\ge2$ makes $b^r-b^s$ an exact subtraction. The $j$ th fractional digit is computed by an exact quotient and remainder; only $j\ge1$ has the mathematical meaning used in the theorems. The generated stream is one-based, and the first digit beyond the seed is $x_{r+1}$ .

The paper’s “after a few iterations” is pinned to its stated upper bound “at most $r$ .” Its “period” is the minimal positive state period of $f^r(z)$ , not a mere period divisor or the period of an arbitrarily selected digit window. “Appropriately chosen” parameters mean a prime $m$ for the goal and exclusion of the two named fixed seeds. The reverse-digit milestone permits the numerator $k$ to depend on the finite endpoint, as the tableau argument does. No seed is excluded from the at-most- $r$ milestone.

The discussion on pp. 473–474 prints the Method 1 seed inequalities in the opposite direction from the Method 1 listing on p. 472. The Lean seed-classification milestone uses the p. 472 directions, which agree with the step map on p. 466 and with direct finite checks. The §5 claim that every five-tuple except the $100$ patterns $xyxyx$ appears once in the special $b=10,r=5,s=2$ full cycle is left for a later extension. The other subtraction order, its modulus $b^r-b^s-1$ , and the paper’s large parameter certificates are outside this mission.

An encoding that merely asserts the existence of some period, allows an impossible seed hypothesis, or replaces the update by a different subtraction order would make the goal vacuous or change the result. The intended development needs Mathlib’s ZMod, multiplicative order, finite iterations, periodic points, and natural-number quotient and remainder. Contributions proving the numbered milestones, strengthening their arithmetic interfaces, or closing the goal are in scope.

Selected references

G. Marsaglia and A. Zaman, A new class of random number generators, The Annals of Applied Probability 1(3), 462–480 (1991). DOI: 10.1214/aoap/1177005878.

17 thms3 active usersReviewed

Completed

Combinatorics Linear Optimization Operations Research·Captain: mikedeng1

Approximation Algorithms for Scheduling Unrelated Parallel Machines 2: Enumerating Long Assignments and Rounding the LP Gives a (1 + ε)-Approximation for MakespanResearch Paper

Motivation

Scheduling independent jobs on unrelated parallel machines to minimize the makespan is one of the basic NP-hard problems of scheduling theory: each job has its own processing time on each machine, with no relation between machines, and the goal is to finish all jobs as early as possible. When the number of machines is part of the input, Lenstra, Shmoys and Tardos showed that no polynomial algorithm can come within a factor below 3/2 of the optimum unless P = NP. When the number of machines $m$ is a fixed constant, the picture is different: the problem admits a polynomial approximation scheme, a family of algorithms that reach any accuracy $1+\varepsilon$ .

Such a scheme was already known. Horowitz and Sahni (1976) gave a fully polynomial approximation scheme for fixed $m$ , but its space requirement grows like $(nm/\varepsilon)^m$ . The second application of the Rounding Theorem in the 1987 report of Lenstra, Shmoys and Tardos is a scheme whose space is polynomial in the input size, in $m$ , and in $\log(1/\varepsilon)$ . This mission formalizes the approximation guarantee of that scheme (Theorem 3 of the report).

Timeline:

1976. Horowitz and Sahni, a fully polynomial approximation scheme for a fixed number of unrelated machines, with exponential space in $m$ .
1985. Potts, a 2-approximation for unrelated machines whose running time is $m^{m-1}$ times a polynomial, based on LP rounding with enumeration.
1987. Lenstra, Shmoys and Tardos, the Rounding Theorem, a polynomial 2-approximation for arbitrary $m$ , and, for fixed $m$ , the scheme formalized here (FOCS 1987; journal version in Mathematical Programming 46, 1990).

Setting

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

Fix an integer deadline $d\ge0$ and an accuracy $\varepsilon>0$ . Assigning job $j$ to machine $i$ is long if $p_{ij}>\varepsilon d$ and short otherwise. A schedule of long assignments $L$ is a partial assignment of jobs to machines using only long assignments; its long load on machine $i$ is $t_i$ , and $L$ is admissible if $t_i\le d$ for every $i$ .

For a threshold $t$ and deadlines $d_1,\dots,d_m$ , the linear program (LP) of the Rounding Theorem has a variable $x_{ij}\ge0$ for every pair with $p_{ij}\le t$ , the constraints $\sum_i x_{ij}=1$ for each job, and $\sum_j p_{ij}x_{ij}\le d_i$ for each machine. The residual LP of $(d,L)$ is (LP) for the jobs left unassigned by $L$ , with $d_i=d-t_i$ and $t=\varepsilon d$ .

The procedure $A_\varepsilon$ , on input $d$ , tries every admissible $L$ ; if the residual LP is feasible it takes a vertex $\tilde x$ , rounds it to a 0-1 solution of the integer program (IP) of the Rounding Theorem, and combines the result with $L$ . It answers 'no' if no residual LP is feasible. A $\rho$ -relaxed decision procedure answers 'no' only when no schedule has makespan at most $d$ , and otherwise returns a schedule of makespan at most $\rho d$ . The binary search of Lemma 1 runs such a procedure on deadlines between $\lceil t/m\rceil$ and $t$ , where $t$ is the makespan of the greedy schedule, and returns the best schedule found.

Formalization targets

Goal: Theorem 3

For every $m\ge1$ , every positive integer matrix $P$ , every $\varepsilon>0$ , every LP solver $V$ , the procedure $A_\varepsilon$ run with $V$ exists, and the binary search driven by any such procedure returns a schedule $\sigma$ with

\mathrm{makespan}(\sigma)\le(1+\varepsilon)\,\mathrm{OPT}.

Milestones (§3, p. 6)

Every machine in an admissible $L$ carries fewer than $1/\varepsilon$ long assignments, and for $n,m\ge1$

\#\{L\text{ admissible}\}<(n+1)^{m/\varepsilon}.

If some schedule has makespan at most $d$ , its long part is admissible and its short part is a feasible solution of the residual LP.
If the short assignments take at most $d-t_i+\varepsilon d$ on machine $i$ , the combined schedule has load at most $(1+\varepsilon)d$ on every machine.
$A_\varepsilon$ exists for every LP solver and is a $(1+\varepsilon)$ -relaxed decision procedure.

Significance

Theorem 3 shows that for a fixed number of unrelated machines, the makespan can be approximated to any accuracy in polynomial time while keeping the memory polynomial in $\log(1/\varepsilon)$ . It is an early instance of the pattern "enumerate the large items, solve an LP for the small ones, round", which recurs in later approximation schemes for scheduling and packing. Together with the 2-approximation of the same paper (mission 1 of this series) and the 3/2 hardness bound (mission 3), it delimits what is achievable for unrelated machines.

The theorem is proved in the paper; none of it is known to have a machine-checked proof. Formalizing it requires a precise account of the enumeration of long assignments, the residual LP, and the binary search, and it exercises the Rounding Theorem, which this series poses in mission 1, outside its original setting (with a non-integral threshold $t=\varepsilon d$ ).

Difficulty

The arithmetic of the scheme is short; the content lies in the Rounding Theorem, which turns a vertex of the residual LP into a 0-1 schedule exceeding each deadline by at most the threshold. The obvious argument, rounding an arbitrary feasible LP solution, fails: a non-vertex solution may split many jobs across many machines, and rounding them can overload a machine by far more than $t$ . The bound depends on the structure of vertices of (LP), which an arbitrary feasible point does not have. A second difficulty is the count of milestone 1, which must be done with a real exponent $m/\varepsilon$ and a strict inequality.

Formalization scope

Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive. Load, makespan and optimal schedules are those of the published MatousekLP.Scheduling.Schedule, applied to the real cast of P.
A vertex of an LP is a point of Set.extremePoints of its feasible region. Variables absent from the paper's (LP) are kept as matrix entries fixed to $0$ , which leaves the vertices unchanged.
The LP solver is a parameter (a vertex selector) and $A_\varepsilon$ is a predicate on procedures: each answer must extend an admissible schedule of long assignments, round the selected vertex within its support, and satisfy the (IP) load bound. The guarantee is proved for every such procedure. The output is thereby tied to what the algorithm computes, so the bound is not witnessed by an optimal schedule.
The binary search is a definition: greedy start, $l=\lceil t/m\rceil$ (the paper's $t/m$ rounded up because makespans are integers), $d=\lfloor(u+l)/2\rfloor$ , best stored schedule as output.
Not formalized: that $m$ is fixed, the polynomial running time, and the space bound polynomial in $m$ , $\log(1/\varepsilon)$ and the input size. The guarantee is stated for every $m\ge1$ . The count $(n+1)^{m/\varepsilon}$ of milestone 1, on which the running-time claim rests, is formalized, with the real power Real.rpow.
The constants are exact: $1+\varepsilon$ , $(n+1)^{m/\varepsilon}$ , $d-t_i+\varepsilon d$ . Milestone 1 needs $n\ge1$ and $m\ge1$ for strictness.
Theorem 1 (the Rounding Theorem) and Lemma 1 are milestones of mission 1 of this series and are not restated here.

Welcome contributions: a proof of the Rounding Theorem in the generality of real deadlines and thresholds, proofs of the counting bound, and lemmas on the binary search that are reusable for any relaxed decision procedure.

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; Theorem 3, p. 6). Journal version: Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951
C.N. Potts, Analysis of a linear programming heuristic for scheduling unrelated parallel machines, Discrete Applied Mathematics 10 (1985) 155–164. https://doi.org/10.1016/0166-218X(85)90009-5
D.S. Hochbaum, D.B. Shmoys, Using dual approximation algorithms for scheduling problems: theoretical and practical results, Journal of the ACM 34 (1987) 144–162. https://doi.org/10.1145/7531.7535

10 thms3 active usersReviewed

Completed

Linear algebra Number Theory·Captain: mikedeng1

Factoring Polynomials with Rational Coefficients II: The Basis Reduction Algorithm Terminates and Returns a Reduced Basis of the LatticeResearch Paper

Why lattice basis reduction matters

A lattice is the set of integer combinations of $n$ linearly independent vectors in $\mathbb R^n$ . Many computational problems — factoring polynomials over $\mathbb Q$ , simultaneous diophantine approximation, integer programming in fixed dimension, breaking knapsack cryptosystems, and the analysis of lattice-based cryptography — reduce to finding a good basis of a given lattice: one whose vectors are short and nearly orthogonal. In 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász gave a polynomial-time algorithm that turns any basis into a reduced one, now called the LLL algorithm (Math. Ann. 261, 1982). It was the key step of their polynomial-time factoring algorithm for $\mathbb Z[X]$ , and it has since become a standard tool of computational number theory, combinatorial optimization and cryptanalysis.

This mission formalizes the algorithm itself, as described in (1.15) of the paper, and the paper's proof (1.23) that it terminates and returns a reduced basis of the input lattice. A companion mission of the same series treats the properties of reduced bases ((1.6)–(1.12)); a third treats the factoring application (Sect. 2).

Setting

Let $b_1,\dots,b_n\in\mathbb R^n$ be linearly independent and $L=\sum_{i=1}^n\mathbb Z b_i$ ; the $b_i$ form a basis for $L$ . The Gram–Schmidt vectors $b_i^*$ and coefficients $\mu_{ij}$ are defined by

b_i^*=b_i-\sum_{j<i}\mu_{ij}b_j^*,\qquad \mu_{ij}=\frac{(b_i,b_j^*)}{(b_j^*,b_j^*)} .

The basis is reduced if $|\mu_{ij}|\le\tfrac12$ for $1\le j<i\le n$ and $|b_i^*+\mu_{i,i-1}b_{i-1}^*|^2\ge\tfrac34|b_{i-1}^*|^2$ for $1<i\le n$ .

The algorithm keeps a current basis $b$ and a subscript $k\in\{1,\dots,n+1\}$ , starting at $k=2$ . While $k\le n$ it performs one step:

if $k>1$ and $|\mu_{k,k-1}|>\tfrac12$ , replace $b_k$ by $b_k-rb_{k-1}$ with $r$ an integer nearest to $\mu_{k,k-1}$ ;
case 1: if $k\ge2$ and $|b_k^*+\mu_{k,k-1}b_{k-1}^*|^2<\tfrac34|b_{k-1}^*|^2$ , interchange $b_{k-1}$ and $b_k$ and set $k:=k-1$ ;
case 2: otherwise, repeatedly take the largest $l<k$ with $|\mu_{kl}|>\tfrac12$ and replace $b_k$ by $b_k-rb_l$ with $r$ an integer nearest to $\mu_{kl}$ , until $|\mu_{kj}|\le\tfrac12$ for all $j<k$ ; then set $k:=k+1$ .

The algorithm stops when $k=n+1$ . Before and after every step the situation (1.16)–(1.17) holds: the first $k-1$ vectors satisfy both conditions of reducedness among themselves.

The termination proof uses the Gram determinants $d_i=\det\big((b_j,b_l)\big)_{1\le j,l\le i}$ ( $d_0=1$ ), the potential $D=\prod_{i=1}^{n-1}d_i$ , and the minimum $m(L)=\min\{|x|^2:x\in L,\ x\ne0\}$ .

Formalization targets

Goal: the algorithm terminates and returns a reduced basis

For every basis $b$ of $\mathbb R^n$ ( $n\ge1$ ):

\neg\,\exists\,(s_t)_{t\in\mathbb N}:\ s_0=(b,2),\ s_t\to s_{t+1}\ \text{for all }t,

every reachable state with $k\le n$ admits a step, and every reachable state $(b',n+1)$ has $b'$ a reduced basis for $L=\sum\mathbb Z b_i$ .

Milestones, in attack order

every step keeps $b$ a basis for the same lattice (p. 519);
the situation (1.16)–(1.17) holds at $k=2$ , implies reducedness at $k=n+1$ , and is restored by every step (pp. 519–520);
$d_i=\prod_{j\le i}|b_j^*|^2$ , so $d_i>0$ , $d_0=1$ , $d_n=d(L)^2$ (1.25);
in case 1, $d_{k-1}$ drops by a factor $<\tfrac34$ , the other $d_i$ are unchanged, and $D$ drops by a factor $<\tfrac34$ ; case 2 changes no $d_i$ (1.23);
$m(L)>0$ is attained and $d_i\ge(3/4)^{i(i-1)/2}m(L)^i$ for every basis of $L$ (1.23);
along any run, case 2 occurs at most $n-1$ more times than case 1 (1.23).

Further targets (integral input, proof of (1.26))

For $b_i\in\mathbb Z^n$ with $|b_i|^2\le B$ , $B\ge2$ : the number $c$ of case-1 steps satisfies $(4/3)^c\le B^{n(n-1)/2}$ ; the identities (1.27)–(1.29) making the $d_i$ common denominators; and $|b_i^*|^2\le B$ throughout.

Significance

The termination theorem is what makes reduced bases computable: the bounds of (1.6)–(1.12) on reduced bases are useful only because the algorithm produces such a basis from any input, and the factoring algorithm of Sect. 3 calls it as a subroutine. The explicit count $(4/3)^c\le B^{n(n-1)/2}$ is the step bound behind the paper's $O(n^4\log B)$ operation count (1.26).

On the formal side, Mathlib has Gram–Schmidt orthogonalization and Minkowski's convex body theorem, but no lattice basis reduction. A verified LLL implementation exists in Isabelle/HOL (the Archive of Formal Proofs entry A verified LLL algorithm, 2018), with its own algorithm description and representation. No Lean 4 formalization of the paper's algorithm or its termination proof exists, as far as could be determined. The result is proved; what is open here is its formalization.

Difficulty

The naive termination argument — "each case-1 step makes a vector shorter" — fails: case 1 can lengthen $b_k$ , and $k$ moves back and forth. The paper's argument needs a potential that decreases by a fixed factor in case 1 and is invariant in case 2, the identity $d_i=\prod|b_j^*|^2$ to see that only $d_{k-1}$ moves, and a lower bound on $d_i$ depending only on $L$ . That lower bound rests on the Hermite-type estimate that a lattice of rank $i$ with Gram determinant $d$ has a nonzero vector with $|x|^2\le(4/3)^{(i-1)/2}d^{1/i}$ , which is not in Mathlib and must be derived from the geometry of numbers for sublattices of lower rank. The invariant (1.16)–(1.17) requires tracking how the Gram–Schmidt data of the first $k$ vectors change under a swap and under the size reductions of case 2.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), with Lean indices $0,\dots,n-1$ for the paper's $1,\dots,n$ ; $b_i^*$ is Mathlib's unnormalised InnerProductSpace.gramSchmidt, and $\mu_{ij}$ is (1.3) verbatim. A state is a pair $(b,k)$ with $k$ stored as the paper's subscript; $b^*$ and $\mu$ are recomputed from $b$ , so the update formulae (1.22) are consequences, not definitions. One step is a relation: "the integer nearest to $x$ " is any integer $r$ with $|x-r|\le\tfrac12$ , so every tie rule is covered. The loop of case 2 picks the largest bad index $l$ , as on the page, and runs until (1.21) holds. The relation follows the text of (1.15), not Fig. 1 (which never visits $k=1$ and stops at $k=n$ ). The standing hypotheses are $n\ge1$ and linear independence of the input basis.

A trivializing formalization is excluded: termination alone would hold for a relation that never fires, so the goal also asserts that a step exists at every reachable state with $k\le n$ , and a sorry-free sanity file exhibits both cases firing for $n=2$ . The goal does not mention $D$ , $d_i$ or $m(L)$ , which appear only in milestones.

Not formalized: the operation count $O(n^4\log B)$ and binary-length bound of (1.26), which need a cost model; the bounds (1.30)–(1.34) on intermediate states and the bounds "throughout the course of the algorithm" on p. 524, which concern states inside a step; and Remark (1.37). Contributions welcome: a reusable Hermite-constant bound $\gamma_i\le(4/3)^{(i-1)/2}$ , Gram determinant identities, and invariance of Gram determinants under unimodular changes.

Selected references

A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982), 515–534. https://doi.org/10.1007/BF01457454
J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959 (reference [4] of the paper). https://doi.org/10.1007/978-3-642-62035-5
R. Bottesch, J. Divasón, M. Haslbeck, S. Joosten, R. Thiemann, A. Yamada, A verified LLL algorithm, Archive of Formal Proofs, 2018. https://www.isa-afp.org/entries/LLL_Basis_Reduction.html

10 thms3 active usersReviewed

Completed

Graph Theory Linear Optimization·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms I: Every Uniform Multicommodity Flow Problem Has Ω(𝒮/log n) ≤ f ≤ 𝒮Research Paper

Motivation

A multicommodity flow problem asks to route several commodities simultaneously through a capacitated network, each from its own source to its own sink. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest routable flow equals the capacity of the smallest separating cut. For many commodities the natural analogue fails: the max-flow can be strictly smaller than the min-cut, already for four commodities (Okamura and Seymour, 1981). Leighton and Rao asked how large the gap can be, and showed that for uniform demands it is at most logarithmic in the number of nodes. The result turned the min-cut, an NP-hard quantity, into something approximable by a linear program, and became the basis of the first polylogarithmic approximation algorithms for sparsest cut, balanced cut, minimum feedback arc set, crossing number and VLSI layout (Leighton–Rao, J. ACM 1999).

Timeline:

1956–1963. Ford and Fulkerson prove max-flow = min-cut for one commodity; Hu (1963) proves equality for two commodities.
1981–1990. Okamura and Seymour give a 4-commodity example with max-flow 3/4 and min-cut 1. Schrijver (1990), combining Lomonosov and Papernov, characterizes demand graphs for which equality always holds. Shahrokhi and Matula (1990) prove equality for uniform demands under a condition on the dual.
1988. Leighton and Rao (FOCS 1988) prove the $\Theta(\log n)$ gap for uniform demands; the journal version (1999) is the source of this mission.
1995. Linial, London and Rabinovich, and independently Aumann and Rabani, extend the bound to arbitrary demands with $O(\log k)$ for $k$ commodities, via metric embeddings (Combinatorica 1995).

Setting

A network is a finite set $V$ of $n$ nodes with a capacity $C(u,v)=C(v,u)\ge0$ for every pair; the pair is an edge when $C(u,v)>0$ . For $U\subseteq V$ with complement $\bar U$ , the cut capacity $C(U,\bar U)$ is the total capacity of the edges joining $U$ to $\bar U$ . As in the paper, the network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$ .

In the uniform multicommodity flow problem (UMFP) every unordered pair of nodes is a commodity with demand one. A routing of value $\lambda$ sends $\lambda$ units between every pair simultaneously, so that the total flow of all commodities over each edge, in both directions together, is at most its capacity. The max-flow $f$ is the largest such $\lambda$ (the concurrent max-flow).

The min-cut (sparsest cut) of the UMFP is

\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|},

the minimum over cuts of the cut capacity divided by the demand separated by the cut. The quantity $C(U,\bar U)/(|U||\bar U|)$ is the ratio cost of the cut.

The milestones use the dual objects. A distance function $d$ assigns a nonnegative length to each edge; $d(u,v)$ is then the shortest-path distance, $d(T,u)=\min_{t\in T}d(t,u)$ , and the total weight is $W=\sum_{e}C(e)d(e)$ . The distance constraint (5) is $\sum_{\{u,v\}}d(u,v)\ge1$ , summed over unordered pairs. A set of nodes has radius at most $\Delta$ if some centre reaches all its nodes by walks inside the set of length at most $\Delta$ . Throughout, $\log n=\log_2 n$ .

Formalization targets

Goal: Theorem 2 (p. 795)

\Omega\!\left(\frac{\mathcal S}{\log n}\right)\le f\le\mathcal S

for every uniform multicommodity flow problem: there is one absolute constant $c>0$ such that $c\,\mathcal S/\log n\le f\le\mathcal S$ for every connected network with $n\ge2$ nodes. The goal fixes no constant, so it is the form any improved argument would still prove.

Milestones, in the order the argument uses them

Weak duality (§1.2, pp. 789–790): every concurrent flow of value $\lambda$ satisfies $\lambda\,|U||\bar U|\le C(U,\bar U)$ for every cut.
LP duality (§2.2, p. 796): every distance function satisfying (5) has $W\ge f$ , and some such function has $W=f$ .
Lemma 3 (p. 797): for every $\Delta>0$ , $V$ splits into components of radius at most $\Delta$ with at most $4W\log n/\Delta$ capacity between components.
Corollary 4 (pp. 798–799): either a set of at least $2n/3$ nodes has radius at most $1/(2n^2)$ , or some cut has ratio cost at most $36W\log n$ .
Lemma 5 (p. 799): if $|T|\ge 2n/3$ and $\sum_{u\notin T}d(T,u)\ge 1/(2n)$ , some cut has ratio cost at most $6W$ .
Lemma 6 (p. 800): a distance function satisfying (5) yields a cut of ratio cost at most $36W\log n$ .

Companion

$\mathcal S\le 36\,f\log n$ and $f\le\mathcal S$ : Theorem 2 with the constant its proof produces.

Significance

The theorem says that the LP relaxation of uniform sparsest cut has integrality gap $O(\log n)$ , and the expander example of §2.1 (Theorem 1) shows this is tight. Combined with the cut-finding argument, it gives an $O(\log n)$ -approximation for sparsest cut and, through the paper's Section 3, approximation algorithms for balanced separators, minimum cut linear arrangement, crossing number, VLSI layout area, feedback arc set and the emulation of networks. Region-growing decompositions of the kind in Lemma 3 reappear in low-diameter decompositions, multicut (Garg–Vazirani–Yannakakis), and metric embedding.

The result is proved; no machine-checked proof of it is known. A formalization would provide: concurrent multicommodity flow and its LP dual on finite graphs, the uniform sparsest cut, a verified region-growing decomposition, and the max-flow min-cut gap theorem itself. The LP-duality milestone, which the paper cites rather than proves, is a reusable piece of flow theory in its own right.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the content. The natural idea, rounding an optimal dual distance function by a threshold and cutting the long edges, does not work: the paper notes (p. 797) that no thresholding rule is known that always yields a good cut, because edges with large distance need not form a sparse cut. Any argument must convert the fractional dual into a single cut while losing only a $\log n$ factor against the total weight $W$ , which requires a global property of the distance function rather than the lengths of individual edges. The LP-duality step needs a correct dual for the concurrent flow problem with shortest-path distances, which Mathlib does not provide off the shelf.

Formalization scope

Nodes and capacities. V is a Fintype with decidable equality; capacities are a symmetric nonnegative real function vanishing on the diagonal, and the graph is the simple graph of pairs with positive capacity. Goal-level statements assume 2 ≤ Fintype.card V and connectivity in the form $C(U,\bar U)>0$ for every nonempty proper $U$ (the paper's standing assumption, p. 789).
Demands and flows. Each unordered pair is encoded as two ordered commodities with demand $\tfrac12$ (the paper's footnote 2). Flows are arc flows with conservation per commodity, and both directions of an edge share its capacity. The max-flow is the real supremum of feasible values; with $n\ge2$ that set is nonempty and bounded.
Cuts. The min-cut ranges over nonempty proper subsets only. Including $U=\emptyset$ or $U=V$ would give $0/0$ , which Lean evaluates to $0$ and which would make the goal trivially true; this formalization excludes it.
Distances. $d(u,v)$ is an infimum over walks in the graph, meaningful under connectivity; the radius of a component is measured by walks inside it.
Constants. The goal keeps the page's $\Omega$ with a single universal constant chosen before the network. The milestones carry the constants computed in the paper's proofs ( $36$ in Corollary 4 and Lemma 6, $6$ in Lemma 5), and each statement says so.
Algorithms. "We can find" is formalized as existence. Running times and the remark that the proofs yield polynomial-time algorithms (p. 801) are out of scope.

Contributions welcome: proofs of any milestone; a general LP-duality theorem for concurrent multicommodity flow, reusable for the product and directed variants; and a general region-growing 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
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
H. Okamura and P. D. Seymour, Multicommodity flows in planar graphs, J. Combin. Theory Ser. B 31:75–81, 1981. https://doi.org/10.1016/S0095-8956(81)80012-3
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
V. Chvátal, Linear Programming, W. H. Freeman, 1983.

10 thms3 active usersReviewed

Completed

Combinatorics Linear algebra·Captain: mikedeng1

Quick Approximation to Matrices and Applications I: Every Real Matrix Is a Sum of at Most 1/ε² Cut Matrices plus an Error W with |W(S,T)| ≤ ε√(|S||T|)‖A‖_FResearch Paper

Motivation

Many dense combinatorial optimization problems (Max-Cut, graph bisection, quadratic assignment on dense instances) have objective functions that are sums of matrix entries over rectangles $S\times T$ . If a matrix can be replaced by a simple surrogate that agrees with it on every rectangle up to a small error, such problems can be solved approximately on the surrogate. Frieze and Kannan's paper Quick approximation to matrices and applications (Combinatorica 19 (1999) 175–220) supplies this surrogate: a sum of a bounded number of cut matrices. Their decomposition is a "weak" form of Szemerédi's regularity lemma whose number of pieces grows only like $1/\varepsilon^2$ , against a tower-type bound for Szemerédi's lemma. It underlies constant-time sampling algorithms for dense instances, the theory of graph limits (the cut distance of Lovász and Szegedy), and the cut-norm approximation algorithm of Alon and Naor.

Timeline:

1978: Szemerédi's regularity lemma, with a number of parts of tower type in $1/\varepsilon$ .
1996: Frieze and Kannan announce the weak regularity lemma (FOCS 1996).
1999: the journal paper proves the matrix version, its algorithmic forms, and applications to Max-Cut, Max-SNP problems and pseudo-regular partitions.
2004–2006: Alon and Naor approximate the cut norm via Grothendieck's inequality; Lovász and Szegedy build graph limits on the cut distance.

Setting

Let $R$ and $C$ be finite sets, $|R|=m$ , $|C|=n$ , and let $A$ be a real $R\times C$ matrix. For $S\subseteq R$ , $T\subseteq C$ write

A(S,T)=\sum_{(i,j)\in S\times T}A(i,j).

The Frobenius norm is $\|A\|_F=\big(\sum_{i,j}A(i,j)^2\big)^{1/2}$ , and the cut norm is $\|A\|_C=\max_{S\subseteq R,\,T\subseteq C}|A(S,T)|$ .

For $S\subseteq R$ , $T\subseteq C$ and $d\in\mathbb R$ , the cut matrix $\mathrm{CUT}(S,T,d)$ has entry $d$ on $S\times T$ and $0$ elsewhere; it has rank at most one. A cut decomposition of width $s$ writes

A=D^{(1)}+\dots+D^{(s)}+W,\qquad D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t),

with error matrix $W$ . In the Lean development these are blockSum, frobNorm, cutNorm, cutMatrix and cutSum in the namespace FriezeKannan.CutDecomp.

Formalization targets

Goal: Theorem 7 (p. 188)

For every real $R\times C$ matrix $A$ and every $\varepsilon>0$ there are $s\le1/\varepsilon^2$ cut matrices $D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t)$ such that $W^{(s)}=A-(D^{(1)}+\dots+D^{(s)})$ satisfies

|W^{(s)}(S,T)|\le\varepsilon\sqrt{|S|\,|T|}\;\|A\|_F\qquad\forall S\subseteq R,\ T\subseteq C. \tag{17}

Milestones (the steps of the proof, p. 188)

With $d=W(S,T)/(|S||T|)$ for nonempty $S,T$ :

\|W-\mathrm{CUT}(S,T,d)\|_F^2-\|W\|_F^2=-|S|\,|T|\,d^2=-\frac{W(S,T)^2}{|S|\,|T|}.

If $|W(S,T)|>\varepsilon\sqrt{|S||T|}\,\|A\|_F$ , this drop is at most $-\varepsilon^2\|A\|_F^2$ .
If $\|W^{(t)}\|_F^2\le(1-\varepsilon^2t)\|A\|_F^2$ , then either $W^{(t)}$ satisfies (17), or one more cut matrix gives $\|W^{(t+1)}\|_F^2\le(1-\varepsilon^2(t+1))\|A\|_F^2$ .

Companion statements

The Remark after Theorem 7 (the case $m=1$ ): a real $n$ -vector $a$ is a weighted sum of at most $\varepsilon^{-2}$ 0-1 vectors plus an error $w$ with $|w(S)|\le\varepsilon\sqrt n\,|a|$ for all $S$ .
Inequality (1), p. 178: $\|M\|_C\le\sup_{x\ne0}\|Mx\|_1/\|x\|_\infty\le4\|M\|_C$ .
§2.3, p. 179: the symmetrised error $\bar W=(W+W^T)/2$ satisfies $\|\bar W\|_C\le\|W\|_C$ .

Significance

Theorem 7 says that the width needed to approximate a matrix on all rectangles, with error measured against $\sqrt{|S||T|}\|A\|_F$ , depends on $\varepsilon$ only, not on $m$ or $n$ . Since $|S||T|\le mn$ , it gives a cut decomposition with $\|W\|_C\le\varepsilon\sqrt{mn}\|A\|_F$ , the error of the paper's algorithmic Theorem 2. It is the existence statement behind the paper's constant-time approximation schemes for dense Max-Cut and Max-SNP problems and behind its pseudo-regular partitions of graphs (§5.1), and it is the matrix form of the weak regularity lemma used throughout the theory of dense graph limits.

The result is proved in the paper, by an elementary argument. Its formalization adds a machine-checked weak regularity lemma for real matrices with explicit constants, stated in a form (finite index types, block sums, cut matrices) that downstream developments in graph limits, property testing and approximation algorithms can import. To the best of the curators' knowledge it has no machine-checked proof; Mathlib contains Szemerédi's regularity lemma for graphs but not this matrix decomposition or the cut norm of matrices.

Difficulty

The obvious decomposition, one cut matrix per nonzero entry, achieves $W=0$ but has width $mn$ ; the content is that width $1/\varepsilon^2$ suffices uniformly in the dimensions. Bounding the error on a single rectangle is easy; bounding it on all $2^{m+n}$ rectangles at once, with an error that scales as $\sqrt{|S||T|}$ rather than as $\sqrt{mn}$ , is the point. The bound is also against the Frobenius norm of the original matrix $A$ , not of the current error, so the argument must track a single global quantity across all steps. In Lean, the main friction is bookkeeping: real casts of cardinalities inside square roots, the division by $|S||T|$ , and the identification of the squared Frobenius norm with a double sum.

Formalization scope

Index sets are arbitrary finite types R, C with decidable equality; subsets are Finsets, and $|S|$ is the cardinality cast to $\mathbb R$ . Empty $R$ or $C$ is allowed.
$\|A\|_F$ is the real square root of the sum of squares (frobNorm); Mathlib's scoped matrix norms are not used. The cut norm is a genuine maximum over the finite nonempty set of pairs of subsets.
A family of $s$ cut matrices is three functions on Fin s; $s=0$ is allowed (for $\varepsilon\ge1$ or $A=0$ no cut matrix is needed). No nonemptiness, disjointness or sign condition is imposed on $R_t$ , $C_t$ , $d_t$ .
Added hypotheses, each disclosed in the statement's Formalization Note: $\varepsilon>0$ (the paper's implicit range of the error parameter; $\varepsilon<1$ is not assumed); nonempty $S,T$ in milestone 1 (they make $d$ well defined); the strict inequality $>$ in milestone 2 (the negation of (17); the page prints $\ge$ ); a nonempty column set for inequality (1) (the supremum over $\mathbb R^n\setminus\{0\}$ needs $n\ge1$ ). Inequality (1) is stated without division, as the existence of a nonzero $x$ with $\|M\|_C\|x\|_\infty\le\|Mx\|_1$ together with $\|Mx\|_1\le4\|M\|_C\|x\|_\infty$ for all $x$ .
The width bound $s\le1/\varepsilon^2$ is the theorem; without it the statement is trivial (one cut matrix per entry gives $W=0$ ). A formalization that drops it, bounds the error by $\|W\|_F$ instead of $\|A\|_F$ , or uses $\sqrt{mn}$ in place of $\sqrt{|S||T|}$ proves a different theorem.
Reusable infrastructure: the identity $\|M\|_F^2=\sum_{i,j}M(i,j)^2$ , block sums of cut matrices and their sums, and the cut norm with its basic properties (transpose invariance, comparison with the $\infty\to1$ norm). Contributions of these as standalone lemmas, and of the milestones in the listed order, are welcome.

Selected references

A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19(2) (1999) 175–220. https://doi.org/10.1007/s004930050052
A. Frieze and R. Kannan, The regularity lemma and approximation schemes for dense problems, Proc. 37th FOCS (1996) 12–20. https://doi.org/10.1109/SFCS.1996.548459
E. Szemerédi, Regular partitions of graphs, Problèmes combinatoires et théorie des graphes, Colloq. Internat. CNRS 260 (1978) 399–401.
N. Alon and A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35(4) (2006) 787–803. https://doi.org/10.1137/S0097539704441629
L. Lovász and B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96(6) (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002

5 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments IV: Uniform Pricing Earns OPT/(1 + ln(v_m/v_1)) in Unit-Demand Min-PricingResearch Paper

Pricing with unit-demand consumers

A seller with $n$ distinct items faces $m$ consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the guarantees of simple pricing rules matter. The simplest such rule is uniform pricing: put one price $q$ on every item and choose $q$ to maximise revenue.

Aggarwal, Feder, Motwani and Zhu (ICALP 2004) and Guruswami, Hartline, Karlin, Kempe, Kenyon and McSherry (SODA 2005) analysed uniform pricing; in the min-buying model it recovers a $1/(1+\ln m)$ fraction of the optimum, a bound Berbeglia and Joret attribute to Aggarwal et al. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) observed that the min-buying problem is a special case of assortment optimisation under a regular discrete choice model, and that uniform pricing then coincides with the revenue-ordered assortments heuristic. Their general guarantee for that heuristic yields a second bound for uniform pricing, in terms of the spread of the valuations rather than the number of consumers. This mission formalizes that bound (Corollary 4.7) together with the reduction it rests on (Theorem 4.6).

Setting

Unit-demand min-pricing ( $\mathrm{UDP}_{\min}$ ). There are items $[n]$ and consumers $[m]$ , $m\ge 1$ . Consumer $i$ is interested in a set $B_i\subseteq[n]$ and has a valuation $v_i>0$ . Given a price assignment $p:[n]\to\mathbb R_{>0}$ , consumer $i$ buys a cheapest item of $B_i$ if its price is at most $v_i$ , and nothing otherwise. The seller's revenue is

\mathrm{rev}_{\mathrm{UDP}}(p)=\sum_{i:\ B_i\ne\emptyset,\ \min_{x\in B_i}p(x)\le v_i}\ \min_{x\in B_i}p(x),

the optimum is $\mathrm{OPT}_{\mathrm{UDP}}=\sup_{p>0}\mathrm{rev}_{\mathrm{UDP}}(p)$ , and uniform pricing earns $\mathrm{UP}=\sup_{q>0}\mathrm{rev}_{\mathrm{UDP}}(q,\dots,q)$ . Write $v_{\max}=v_m$ and $v_{\min}=v_1$ for the extreme valuations.

Regular choice models. A finite product set $\mathcal C$ carries choice probabilities $\mathcal P(x,S)$ for $x\in\mathcal C$ , $S\subseteq\mathcal C$ , with no-purchase probability $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ . The model is regular if (i) all probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$ , (iii) $\sum_{x\in S}\mathcal P(x,S)\le1$ , and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$ . With revenues $r:\mathcal C\to\mathbb R_{>0}$ , an assortment earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)r(x)$ and $\mathrm{OPT}=\max_S\mathrm{rev}(S)$ . If $r_1<\dots<r_k$ are the distinct revenues and $S_i=\{x: r(x)\ge r_i\}$ , revenue-ordered assortments earn $\mathrm{RO}=\max_i\mathrm{rev}(S_i)$ .

The reduction. From a $\mathrm{UDP}_{\min}$ instance the paper builds $\mathcal C=[n]\times\{v_1,\dots,v_m\}$ , $r((x,v))=m\,v$ , and $\mathcal P=\frac1m\sum_i\mathcal P_i$ , where $\mathcal P_i$ spreads probability one over the set $Q_i(S)$ of pairs $(x,v)\in S$ with $x\in B_i$ , $v\le v_i$ and $v$ minimal among the pairs of $S$ whose item lies in $B_i$ .

Formalization targets

Goal: Corollary 4.7

\mathrm{OPT}_{\mathrm{UDP}}\ \le\ \Big(1+\ln\frac{v_{\max}}{v_{\min}}\Big)\cdot\mathrm{UP}.

The bound is the paper's "approximates the optimum revenue to within a factor of $1/(1+\ln\rho)$ , $\rho:=v_m/v_1$ ", stated in product form.

Milestones

Lemma 4.5. Some optimal price assignment takes only valuations as prices; in particular $\mathrm{OPT}_{\mathrm{UDP}}$ is attained.
Regularity of the reduction's choice model (proof of Theorem 4.6, pp. 17–18).
Assortments to prices: $\mathrm{rev}(S)=\mathrm{rev}_{\mathrm{UDP}}(p_S)$ with $p_S(x)=\min\{v:(x,v)\in S\}$ (p. 19).
Prices to assortments: for valuation-valued $p$ , $\mathrm{rev}(S_p)=\mathrm{rev}_{\mathrm{UDP}}(p)$ with $S_p=\{(x,v): v\ge p(x)\}$ (p. 19).
Theorem 4.6 for the explicit instance: regularity, positive revenues, equal optima, and the two-way correspondence between threshold sets and uniform valuation prices.
Theorem 3.2 for an arbitrary regular model:

\mathrm{OPT}\le\Big(\sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\Big)\mathrm{RO},\qquad \sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\le 1+\ln\frac{r_k}{r_1},\qquad r_0:=0.

Significance

The corollary gives a uniform-pricing guarantee that is independent of the number of consumers and items: when valuations lie within a factor $\rho$ of each other, a single price recovers a $1/(1+\ln\rho)$ fraction of the optimum, which improves on $1/(1+\ln m)$ whenever $\rho<m$ . More broadly, Theorem 4.6 places $\mathrm{UDP}_{\min}$ inside the class of regular choice models, so every guarantee proved for revenue-ordered assortments under regularity transfers to uniform pricing.

All results here are proved in the paper. Nothing in this mission is formalized elsewhere as far as a search of the platform shows: there is no regular choice model, no $\mathrm{UDP}_{\min}$ problem and no revenue-ordered guarantee on Prove2Me. The mission produces the reduction as reusable infrastructure, a machine-checked version of the paper's Lemma 4.5 (whose appendix proof is an informal repair argument), and the first formal guarantee for uniform pricing.

Difficulty

The reduction is where the work sits. Regularity hinges on the no-purchase case of axiom (iv): enlarging an assortment can only make $Q_i$ nonempty, never empty, and this must be checked for the specific sets $Q_i(S)$ whose definition depends on the whole of $S$ . The revenue identities require tracking the minimum over $B_i$ of a price function obtained from an assortment, including items absent from $S$ , which receive the paper's " $+\infty$ " price. Lemma 4.5 is needed to make the optimum of the uncountable pricing problem coincide with that of a finite assortment problem, and the statement is about a supremum over a continuum of price vectors whose attainment is not obvious. Theorem 3.2 has to relate the optimum to threshold sets of an arbitrary regular model, where products may share revenues and the optimal assortment need not be a threshold set.

The naive route of comparing uniform pricing to the optimum directly, consumer by consumer, does not give a bound in terms of $v_m/v_1$ ; the reduction to a regular model is what supplies it.

Formalization scope

Items and consumers are finite types X and M, with Nonempty M ( $m\ge1$ ). Valuations satisfy $v_i>0$ as a field of the instance; the paper says "non-negative", but its reduction ( $r=m\,v>0$ ) and its ratio $v_m/v_1$ need positivity.
A consumer with $B_i=\emptyset$ pays $0$ . Ties among cheapest items do not affect payments, so payments are defined directly.
$\mathrm{OPT}_{\mathrm{UDP}}$ and $\mathrm{UP}$ are real suprema over positive price assignments and positive uniform prices; both index sets are nonempty and the revenues are bounded by $\sum_i v_i$ . Uniform pricing ranges over all $q>0$ , not only valuations.
The no-purchase option is not a product: it is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$ , and regularity includes axiom (iv) for it. OPT is a maximum over all Finset C; RO is a maximum over the $k$ threshold sets only. Distinct revenues are sorted 0-based (Fin k), with $r_0=0$ handled as a separate case.
The paper's $+\infty$ price for $p_S$ is the real $1+\sum_i v_i$ , which exceeds every valuation, as its Remark on p. 18 allows. The valuation set collapses equal valuations.
Approximation factors are in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$ ; $\ln$ is Real.log applied to ratios $\ge1$ .
Trivializing readings are excluded: Theorem 4.6 is stated for the explicit instance of its proof, not as the bare existence of a regular instance with the same optimum (a single product of revenue $\mathrm{OPT}_{\mathrm{UDP}}$ would satisfy that); $\mathrm{OPT}_{\mathrm{UDP}}$ ranges over all positive price assignments, not uniform ones; valuations are positive, so no logarithm takes a junk value.
Theorem 3.2 is restated here for this mission's copy of the regular model; it is also the goal of mission I of this series. Reusable pieces: the regular choice model and revenue-ordered value, and the $\mathrm{UDP}_{\min}$ model. Contributions of any milestone, and alternative proofs of Lemma 4.5, are welcome.

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; Algorithmica 82 (2020). https://arxiv.org/abs/1606.01371
G. Aggarwal, T. Feder, R. Motwani and A. Zhu, Algorithms for multi-product pricing, ICALP 2004. https://doi.org/10.1007/978-3-540-27836-8_8
V. Guruswami, J. D. Hartline, A. R. Karlin, D. Kempe, C. Kenyon and F. McSherry, On profit-maximizing envy-free pricing, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070598
P. Rusmevichientong, B. Van Roy and P. W. Glynn, A nonparametric approach to multiproduct pricing, Operations Research 54(1), 2006. https://doi.org/10.1287/opre.1050.0236
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.1754

13 thms3 active usersReviewed

Complexity Theory Probability Quantum Information·Captain: mikedeng1

Strengths and Weaknesses of Quantum Computing I: Relative to a Random Oracle, a Quantum Algorithm Needs Ω(2^{n/2}) Queries to Decide Whether 1ⁿ Has a PreimageResearch Paper

Motivation

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs $\Omega(2^{n/2})$ queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).

Timeline:

1996: Grover's algorithm searches $N$ items with $O(\sqrt N)$ queries.
1997: the paper proves $\mathbf{BQTime}(o(2^{n/2})) \not\supseteq \mathbf{NP}$ relative to a random oracle with probability 1 (Theorem 3.5), and the $\Omega(2^{n/3})$ bound for random permutations (Theorem 3.6).
1998: Boyer, Brassard, Høyer and Tapp give tight bounds for quantum searching.
1999: Zalka shows Grover's algorithm is exactly optimal.

Setting

A $T$ -query algorithm acts on vectors $\varphi \in \mathbb{C}^{(X \cup \{\bot\}) \times R \times W}$ , where $X$ is the set of query strings, $R$ the set of answers (an additive group) and $W$ a finite workspace. A basis configuration $(x, z, w)$ with $x \in X$ is querying $x$ ; $(\bot, z, w)$ is not querying. For an oracle $f : X \to R$ the oracle operator is

O_f\,|x, z, w\rangle = |x, z + f(x), w\rangle, \qquad O_f\,|\bot, z, w\rangle = |\bot, z, w\rangle .

The algorithm consists of a unit vector $\varphi_0$ , unitaries $U_0, \dots, U_{T-1}$ that do not depend on the oracle, and a set of accepting configurations. With oracle $A$ its states are $\varphi_{i+1} = U_i O_A \varphi_i$ ; the acceptance probability is the squared norm of the accepting part of $\varphi_T$ . The query magnitude of $y$ in $\varphi$ is $q_y(\varphi) = \sum_{z, w} |\varphi(y, z, w)|^2$ (Definition 3.2). The algorithm decides a property if it accepts with probability at least $2/3$ when the property holds and at most $1/3$ when it fails.

In the main theorem $X = R = \{0,1\}^n$ with bitwise addition, and the oracle is a uniformly random function $A : \{0,1\}^n \to \{0,1\}^n$ . The question is whether $1^n$ belongs to $\mathcal{L}_A = \{y : \exists x\ A(x) = y\}$ .

Formalization targets

Goal: Theorem 3.5 (finite form)

\exists\, c > 0\ \exists N\ \forall n \ge N\ \forall M \text{ with } T \le c\, 2^{n/2} \text{ queries}: \quad \Pr_A\bigl[M^A \text{ fails to decide } \exists x\ A(x) = 1^n\bigr] \ge \tfrac18 .

The constant is existential, matching the theorem's hypothesis $T(n) = o(2^{n/2})$ ; $c$ and $N$ do not depend on the workspace or the algorithm.

Milestones

Theorem 3.1: unit vectors at distance $\varepsilon$ have measurement distributions within total variation $4\varepsilon$ .
Theorem 3.3 (corrected): changing oracle answers on time–string pairs of total query magnitude $\le \varepsilon^2/T$ moves the final state by at most $2\varepsilon$ .
Corollary 3.4 (corrected): outside a set of at most $4T^2/\varepsilon^2$ strings, changing the oracle at one string moves the final state by at most $\varepsilon$ .
$\Pr[1^n \text{ has no preimage}] = ((2^n-1)/2^n)^{2^n} \ge 1/4$ .
$\Pr[1^n \text{ has a unique preimage}] = ((2^n-1)/2^n)^{2^n-1} \ge 1/e$ .
Final states within $1/13$ for $A$ and $A_y$ force failure on one of them.
The double counting: failing oracles with a unique preimage are at least half the successful oracles with none.

Significance

The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle $\mathbf{NP} \not\subseteq \mathbf{BQP}$ ; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).

The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.

Difficulty

The obvious argument — each query reveals one bit about where the preimage is, so $\Omega(2^n)$ queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across $T$ unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.

Formalization scope

The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running $T$ steps is a $T$ -query algorithm: oracle answers on lengths other than $n$ are fixed and absorbed into the unitaries, as the proof fixes them, and the input $1^n$ is absorbed into $\varphi_0$ . Queries return the full value $A(x) \in \{0,1\}^n$ ; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with $c$ halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all $(2^n)^{2^n}$ functions; total variation distance is the paper's $\sum_x |\mathcal D(x) - \mathcal D'(x)|$ without the factor $1/2$ .

Corrections: Theorem 3.3 is printed with conclusion $\le \varepsilon$ , which fails (one query string, $T = 1$ , distance $2$ at $\varepsilon = 1$ ; machine-checked); the true bound is $2\varepsilon$ . Corollary 3.4 is printed with $|S| \le 2T^2/\varepsilon^2$ , which fails (16 strings, $T = 1$ , $\varepsilon = 0.45$ ); the true bound is $4T^2/\varepsilon^2$ . The printed constant $T(n) \le 2^{n/2}/20$ in the proof of Theorem 3.5 does not support the step $2^n - \mathrm{card}(S) \ge 2^{n-1}$ even with the paper's own count; the goal states an existential constant, and $c = 1/37$ works with the corrected Corollary 3.4. The closing probability- $1$ argument over countably many machines and the class statement about $\mathbf{BQTime}$ are not formalized.

A formalization in which algorithms query at every step on every branch (no $\bot$ sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.

Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.

Selected references

C. H. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and weaknesses of quantum computing, SIAM J. Comput. 26(5):1510–1523, 1997. arXiv:quant-ph/9701001
L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
M. Boyer, G. Brassard, P. Høyer, A. Tapp, Tight bounds on quantum searching, Fortschr. Phys. 46, 1998. arXiv:quant-ph/9605034
C. Zalka, Grover's quantum searching algorithm is optimal, Phys. Rev. A 60, 1999. arXiv:quant-ph/9711070
R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, Quantum lower bounds by polynomials, J. ACM 48, 2001. arXiv:quant-ph/9802049
A. Ambainis, Quantum lower bounds by quantum arguments, J. Comput. Syst. Sci. 64, 2002. arXiv:quant-ph/0002066

9 thms3 active usersReviewed

Complexity Theory Operations Research·Captain: mikedeng1

Complexity of Machine Scheduling Problems 5: KNAPSACK Reduces to Two-Machine Flow Shop Makespan with a Release Date or Tree Precedence and to Two- and Three-Machine Job Shop MakespanResearch Paper

Motivation

In 1975 P. Brucker, J. K. Lenstra and A. H. G. Rinnooy Kan classified a large part of deterministic machine scheduling by computational complexity, using the then new theory of NP-completeness of Cook and Karp. Their report, Complexity of Machine Scheduling Problems (Mathematisch Centrum, Amsterdam, 1975; published in Annals of Discrete Mathematics 1, 1977), gives for many problems either a polynomial algorithm or a polynomial reduction from a known NP-complete problem. It drew the boundary between easy and hard scheduling problems that later surveys and the standard three-field classification build on.

This mission covers four reductions of the report's Theorem 4 that concern shops with several machines. A flow shop processes every job on machines $M_1, \dots, M_m$ in this order; a job shop lets each job follow its own route. For two machines and no further constraints, the flow shop is solved by Johnson's rule (Johnson, 1954) and the job shop with at most two operations per job by Jackson's extension of it (1956). The four reductions show that these positive results stop exactly where one more feature is added: one job with a nonzero release date, tree-shaped precedence constraints, a third operation per job, or a third machine.

Setting

A general shop instance has jobs $J_1,\dots,J_n$ and machines $M_1,\dots,M_m$ . Job $J_j$ consists of $m_j$ operations; its $r$ -th operation runs on machine $\mu_{jr}$ for $p_{jr}\in\mathbb N$ time units, and the tuple $\mu_j$ is the job's machine order (a machine may occur more than once). Each job has a release date $r_j$ , and some pairs of jobs carry a precedence constraint $J_j<J_k$ .

A schedule gives every operation a start time. It is feasible if no operation of $J_j$ starts before $r_j$ ; the operations of each job run in the order $\mu_j$ , each after the previous one completes; two operations on the same machine never overlap; and $J_j<J_k$ implies $C_j\le B_k$ , where $C_j$ is the completion time of $J_j$ and $B_k$ the starting time of $J_k$ . The makespan is $C_{\max}=\max_j C_j$ .

In the report's notation $n|m|\ell,\lambda|C_{\max}$ , $\ell=F$ means a flow shop and $\ell=G$ a job shop; $\lambda$ may contain $r_n\ge 0$ (only the last job has a release date), tree (the precedence graph is a branching: no directed cycle, and either every indegree or every outdegree is at most one) and $m_j\le m_*$ (at most $m_*$ operations per job). The recognition version of a problem asks, for an instance and a number $y$ , whether a feasible schedule with $C_{\max}\le y$ exists.

KNAPSACK asks, for positive integers $a_1,\dots,a_t$ and $b$ , whether some $S\subseteq T=\{1,\dots,t\}$ has $\sum_{j\in S}a_j=b$ . A problem $P'$ is reducible to $P$ ( $P'\propto P$ ) if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer.

Formalization targets

Goal: Theorem 4(g)–(j)

\mathrm{KNAPSACK}\ \propto\ n|2|F,r_n{\ge}0|C_{\max},\quad n|2|F,\mathit{tree}|C_{\max},\quad n|2|G,m_j{\le}3|C_{\max},\quad n|3|G,m_j{\le}2|C_{\max}.

Each part is a polynomial-time many-one reduction between languages of binary strings. The other six parts of Theorem 4 (single-machine problems) belong to other missions of this series.

Milestones: the four equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A=\sum_{j\in T}a_j$ , and for each of the paper's four constructions with its threshold $y$ ,

\exists\,S\subseteq T:\ \sum_{j\in S}a_j=b\iff\text{the constructed instance has a feasible schedule with } C_{\max}\le y,

with $y=A+1$ for (i), $y=2A$ for (j), $y=t(A+1)$ for (g) and $y=t(A+1)+1$ for (h). The milestones are stated directly about the printed constructions, in the order (i), (j), (g), (h) of the report.

Significance

With the NP-completeness of KNAPSACK (Karp, 1972), the goal makes the four problems NP-complete. As the report notes, (i) and (j) together with the elementary reductions of its Theorem 1 make the general job shop $n|m|G|C_{\max}$ NP-complete for every fixed $m\ge 2$ . Parts (g) and (h) show that Johnson's two-machine algorithm admits neither release dates nor precedence constraints in general. Because KNAPSACK can be solved in pseudo-polynomial time, these results establish NP-hardness in the ordinary sense only; strong NP-hardness of some of these problems came later (Garey, Johnson and Sethi, 1976, for the three-machine flow shop).

The results are proved in the report; no machine-checked proof of any of them is known to exist. A formalization adds explicit constructions and complete equivalence proofs where the report is brief: in (h) it proves one inequality and states that the rest "is analogous to that of reduction (g)", and the forward directions are given by figures. It also produces a reusable formal model of general shops with integral start times, release dates, precedence and repeated machines.

Difficulty

Polynomial-time computability of the constructions is routine in principle but laborious in Cook's Turing-machine model, which is the setting of the goal: binary arithmetic for $A$ , $t a_j$ and $t(A-b)$ , and parsing of the KNAPSACK code.

The mathematical difficulty is the reverse direction of each equivalence. The report's arguments are phrased in terms of "a processing order on $M_1$ " and treat the jobs before and after an extra job as two blocks. A formal proof must derive such an order from arbitrary start times and must handle every interleaving, including idle time and the case where the extra job's operations do not fit the printed pattern. In (j) the printed bound for the case $c<0$ contains a minimum of two quantities whose justification is left to the reader. In (h) the printed case uses $t a_j\ge t$ , so the positivity of the data matters, and the remaining cases are only said to be analogous to (g).

Formalization scope

Jobs are Fin n and machines Fin m, both 0-based. A job's operations form a list of (machine, processing time) pairs, so machine orders may repeat machines, as $\mu_n=(M_2,M_1,M_2)$ in (i) does. Start times are natural numbers. The report computes schedules from processing orders on integer data, the makespan is a regular criterion, and release dates and precedence survive shifting operations left, so integral start times lose no value. $C_{\max}\le y$ is stated as $C_j\le y$ for every $j$ ; no maximum over an empty set is formed. Precedence $J_j<J_k$ is between jobs: every operation of $J_k$ starts no earlier than $C_j$ . A branching is an acyclic precedence graph in which every indegree is at most one or every outdegree is at most one; the report's "either … or" is read for the whole graph. Job-shop classes require at least one operation per job. A flow-shop job has exactly the operations $(M_1,M_2)$ , with times allowed to be zero.

The following readings of the report are made explicit. "Reducible" is Karp reducibility, CookPvsNP.PolyReducible from the published definitions CookPvsNP_defs. The languages are over the four-letter alphabet with binary numbers of the published definition ProjSchedTW.Complexity.Encoding. Its subsetSumLang allows zero sizes, while the report's KNAPSACK is over positive integers, so KNAPSACK is defined locally with positivity in the language. "We may assume that $0<b<A$ " becomes a hypothesis of every equivalence; the goal's reduction must still handle the other inputs. The printed "value $C_{\max}=y$ " of the forward directions is read as " $\le y$ ", as Section 2 defines the recognition version. The remark that (h) is analogous to (g) becomes the full equivalence for (h). An instance outside the problem's class is not in its language. NP-membership is not part of the goal.

The formal two-stage flow-shop models of Johnson's paper (JohnsonFlowShop.TwoStage.IsFeasible) and the job-shop model of Jansen, Solis-Oba and Sviridenko (JobShopLTAS.Core.Instance) use real start times and have neither release dates nor precedence. They were consulted, but the model here is local.

Ruled out as trivializing: a goal without the polynomial-time condition (the bare equivalence of yes-instances), a target language that accepts instances outside the class, and equivalences about some instance rather than the printed construction.

Contributions are welcome on any milestone, on a general lemma that turns a feasible schedule into a processing order per machine, and on polynomial-time computability of list arithmetic in the Turing-machine model, which every reduction of this series needs.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110
J. R. Jackson, An extension of Johnson's results on job lot scheduling, Naval Research Logistics Quarterly 3 (1956) 201–203. https://doi.org/10.1002/nav.3800030307
M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1 (1976) 117–129. https://doi.org/10.1287/moor.1.2.117
S. A. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

11 thms3 active usersReviewed

Completed

Machine Learning Operations Research·Captain: mikedeng1

The Weighted Majority Algorithm 2: On Any Partition into Segments, WML Makes at Most Σ min(l_i, (log(n/(βγ)) + m_i log(1/β))/log(1/u)) MistakesResearch Paper

Motivation

Prediction with expert advice asks a master algorithm to combine the binary predictions of a pool of $n$ prediction algorithms, trial after trial, so that it makes few more mistakes than the best member of the pool, without any probabilistic assumption on the data. Littlestone and Warmuth's Weighted Majority Algorithm WM (Littlestone and Warmuth 1994) keeps a weight per member, predicts with the weighted vote, and multiplies the weights of the wrong members by a factor $\beta<1$ after each of its own mistakes. Its mistake bound is of order $\log n + m$ , where $m$ is the number of mistakes of the best member on the whole sequence.

That bound compares the master with a single fixed member. In many applications the member that predicts well changes over time: one algorithm is accurate for a while, then a second one, then a third. Against a shifting target of this kind, WM can do badly, because the weight of a member that was wrong for a long time has become so small that it takes many mistakes to recover it. Section 3 of the paper introduces the variant WML, which never decreases a weight that is already small relative to the total, and proves that it pays only a logarithmic cost per change of target. This was the first result of what is now called tracking the best expert; it was later refined by Herbster and Warmuth's Fixed-Share algorithm (Herbster and Warmuth 1998).

Timeline. 1989: a conference version of the paper appears at FOCS. 1994: the journal version, the source of this mission, gives Lemma 3.1 and Theorem 3.1 in their present form. 1998: Herbster and Warmuth's Tracking the Best Expert generalizes the shifting bound to other loss functions.

Setting

A run takes place over $T$ trials $t = 0, \dots, T-1$ . In trial $t$ each member $i \in \{1,\dots,n\}$ of the pool predicts $x_i^{(t)} \in \{0,1\}$ , the master predicts $\lambda^{(t)} \in \{0,1\}$ , and the label $\rho^{(t)} \in \{0,1\}$ is revealed. The predictions of the pool and the labels are arbitrary.

The master keeps weights $w_i^{(t)} > 0$ , the weights at the beginning of trial $t$ . Let $W^{(t)} = \sum_j w_j^{(t)}$ be the total weight and $q_b^{(t)}$ the total weight of the members predicting $b$ . WML has parameters $0 < \beta < 1$ and $0 \le \gamma < \tfrac12$ :

it predicts $0$ if $q_0^{(t)} > q_1^{(t)}$ , $1$ if $q_1^{(t)} > q_0^{(t)}$ , and either value on a tie;
if $\lambda^{(t)} \ne \rho^{(t)}$ , each member $i$ with $x_i^{(t)} \ne \rho^{(t)}$ and $w_i^{(t)} > \frac{\gamma}{n} W^{(t)}$ has its weight multiplied by $\beta$ ; all other weights stay;
if $\lambda^{(t)} = \rho^{(t)}$ , no weight changes.

With $\gamma = 0$ this is WM. Write $m$ for the number of mistakes of the master and

u = \frac{1+\beta}{2} + (1-\beta)\gamma ,

which lies in $[\tfrac12, 1)$ for the stated parameter ranges.

Formalization targets

Goal: Theorem 3.1 (p. 224)

Split the sequence into consecutive segments $\mathcal S_1, \dots, \mathcal S_k$ , with $l_i$ trials in $\mathcal S_i$ , and let $m_i$ be the smallest number of mistakes any single pool member makes on $\mathcal S_i$ . If $\gamma > 0$ and every initial weight is at least $\beta\gamma/n$ times the total initial weight, then

m \le \sum_{i=1}^{k} \min\left( l_i,\ \frac{\log\big(n/(\beta\gamma)\big) + m_i \log(1/\beta)}{\log(1/u)} \right).

The partition is arbitrary and unknown to the algorithm; the bound holds for all partitions simultaneously.

Milestone: Lemma 3.1 (pp. 223–224)

The single-segment case, $k = 1$ , together with the statement that the weight floor survives the run: if every initial weight is at least $\beta\gamma/n$ times the total, then

m \le \frac{\log\big(n/(\beta\gamma)\big) + m_0 \log(1/\beta)}{\log(1/u)},

and every final weight is at least $\beta\gamma/n$ times the total final weight.

Milestone: the contraction step (p. 224, proof of Lemma 3.1)

On every mistake trial, $W^{(t+1)} \le u\, W^{(t)}$ .

Significance

The result. Theorem 3.1 shows that an online algorithm with no knowledge of when or how often the best predictor changes can compete with the best sequence of predictors, at a price of $O(\log(n/(\beta\gamma)))$ mistakes per segment. The $\min$ with $l_i$ says that a segment never costs more than its length. The bound is the template for later tracking and adaptive-regret results in online learning and for algorithms whose weights are kept bounded away from zero.

Formalizing it. The result is proved in the paper; no machine-checked proof of a shifting-target bound exists on Prove2Me or, to our knowledge, in Mathlib. This mission produces a formal model of WML in which ties are arbitrary (a run is a relation, so the bounds cover every tie-breaking rule), the per-mistake contraction, the single-sequence bound with its preserved invariant, and the segment bound. The model of trials, majority votes and mistake counts is reusable for the other algorithms of the paper.

Difficulty

The standard argument for WM compares the decrease of the total weight with the final weight of the best member. For a shifting target this fails twice. First, the best member of a later segment may have been wrong during all earlier segments; under WM its weight has shrunk by $\beta$ per mistake, and the master has to make many mistakes before that member regains influence. Second, the floor that prevents this also prevents some wrong members from being penalized, so the total weight shrinks by less on each mistake than under WM. The statement has to control both effects at once, and the per-segment accounting has to restart from whatever weights the previous segments left behind. A natural first idea, applying the single-sequence bound to each part of an arbitrary (interleaved) partition, does not work: for interleaved subsequences the inequality is false, and the theorem is about consecutive segments.

Formalization scope

The pool is Fin n with $n > 0$ ; trials are Fin T; binary values are Bool; weights are real, w : ℕ → Fin n → ℝ, with w t the weights at the beginning of trial $t$ , w 0 the initial and w T the final weights. A run is the relation IsWMLRun β γ x ρ w lam; it fixes positive initial weights, the majority rule with arbitrary ties, and the update, whose threshold is strict and uses the total weight at the beginning of the trial. Logarithms are natural logarithms; the base cancels in every ratio. The minimum over the pool is an infimum in ℕ over Fin n. Segments are given by monotone boundaries b : Fin (k+1) → ℕ with b 0 = 0 and b (Fin.last k) = T; empty segments are allowed and contribute $0$ .

The paper allows $\gamma = 0$ for the algorithm, but then the bounds read $\log(n/0) = +\infty$ . In Lean, n / 0 = 0, so the bounds assume $\gamma > 0$ ; the contraction milestone holds for $0 \le \gamma < \tfrac12$ and is stated so. The hypothesis $\gamma < \tfrac12$ is kept as stated in the paper, not replaced by $u < 1$ . A trivializing formalization, such as fixing the tie-breaking rule, dropping the strict weight test, letting the floor hypothesis be unsatisfiable, or allowing interleaved subsequences (which makes the goal false), is ruled out: a run exists for every input from every positive initial weights, and equal initial weights satisfy the floor.

Contributions welcome: proofs of the three statements, and lemmas on restricting a WML run to a block of trials, which the goal needs and which apply to any segment-wise analysis.

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
N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proc. 30th IEEE FOCS, 256–261, 1989. https://doi.org/10.1109/SFCS.1989.63487
M. Herbster, M. K. Warmuth, Tracking the Best Expert, Machine Learning 32, 151–178, 1998. https://doi.org/10.1023/A:1007424614876

4 thms3 active usersReviewed

Complexity Theory Operations Research·Captain: mikedeng1

Complexity of Machine Scheduling Problems 4: KNAPSACK Reduces to Single-Machine Total Completion Time with One Release DateResearch Paper

Motivation

Minimizing the total completion time $\sum_j C_j$ of jobs on a single machine is one of the oldest problems in scheduling theory. When every job is available at time $0$ , processing the jobs in order of nondecreasing processing time is optimal (the shortest-processing-time rule), so the problem is solved by sorting. Release dates, times before which a job may not start, change the picture. In their 1975 report Complexity of Machine Scheduling Problems (Mathematisch Centrum Report BW 43/75; journal version in Annals of Discrete Mathematics 1, 1977), Brucker, Lenstra and Rinnooy Kan used the then-new theory of NP-completeness (Cook 1971, Karp 1972) to map which classical scheduling problems are polynomially solvable and which are NP-complete. Theorem 4 of that report lists ten problems to which KNAPSACK reduces. Part (a) shows that total completion time on one machine is already hard when a single job has a nonzero release date and all weights are equal.

The result is a sharp boundary. With all release dates zero the problem is easy; with one nonzero release date it is NP-complete. It is a standard entry in the complexity classification of single-machine problems that later surveys (Lawler, Lenstra, Rinnooy Kan and Shmoys, 1993) and the scheduling-complexity databases build on.

Setting

An instance of KNAPSACK consists of positive integers $a_1,\dots,a_t$ and $b$ ; with $T=\{1,\dots,t\}$ , it has a solution if $\sum_{j\in S}a_j=b$ for some $S\subseteq T$ .

In the scheduling problem there are $n$ jobs $J_1,\dots,J_n$ and one machine. Job $J_j$ has a processing time $p_j$ , a weight $w_j$ and a release date $r_j$ , all nonnegative integers. A schedule assigns each job a starting time $B_j\ge r_j$ ; the job completes at $C_j=B_j+p_j$ , and no two jobs are processed at the same time. The problem written $n|1|r_n\ge0,w_j=1|\sum w_jC_j$ in the paper's notation is the class of instances in which every weight is $1$ and every job except the last one, $J_n$ , has release date $0$ . Its recognition version asks, given such an instance and an integer $y$ , whether some schedule has $\sum_jC_j\le y$ .

A problem $P'$ is reducible to $P$ (written $P'\propto P$ ) when every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer. The paper's construction maps $a_1,\dots,a_t,b$ (with $0<b<A=\sum_ja_j$ and $a_*=\max_ja_j$ ) to an instance with $n=t+t'+u+1$ jobs in four groups $T$ , $T'$ , $U$ and $\{J_n\}$ , with processing times $\tau+a_j$ , $\tau$ , $\upsilon$ and $1$ , the release date $r_n=t\tau+b$ , and threshold $y=\upsilon+\tfrac12u(u+1)\upsilon$ , where $t'$ , $\tau$ , $u$ , $\sigma$ , $\upsilon$ are explicit polynomials in $t$ , $a_*$ , $b$ and $A$ .

Formalization targets

Goal: Theorem 4(a)

\text{KNAPSACK}\ \propto\ n|1|r_n\ge0,w_j=1|\textstyle\sum w_jC_j ,

stated as CookPvsNP.PolyReducible knapsackLang sumCLangMult: a polynomial-time computable map on binary strings that sends codes of solvable KNAPSACK instances, and only those, to codes of yes-instances of the scheduling problem.

Milestones

Forward direction (p. 22). If $\sum_{j\in S}a_j=b$ , the processing order $(S',S,J_n,T'-S',T-S,U)$ , with $S'=\{t+j\mid j\in T-S\}$ , gives a feasible schedule with $\sum_{j\notin U}C_j\le u$ , $\sum_{j\in U}C_j=u\sigma+\tfrac12u(u+1)\upsilon$ and $\sum_jC_j\le y$ .
Claim (A). In every schedule with $\sum_jC_j\le y$ , all jobs outside $U$ precede all jobs of $U$ .
Claim (B). In every such schedule some job of $U$ starts by time $\sigma$ ; consequently $\sum_{j\notin U}C_j\le u$ .
Claim (C). Exactly $t$ jobs precede $J_n$ .
Claim (D). $B_n=t\tau+b$ .
Equivalence (pp. 22–23). For $0<b<A$ , KNAPSACK has a solution iff the constructed instance has a schedule with $\sum_jC_j\le y$ .

Significance

Together with the NP-completeness of KNAPSACK (Theorem 2(b), quoted from Karp), Theorem 4(a) shows that $n|1|r_n\ge0,w_j=1|\sum w_jC_j$ is NP-complete; with general release dates the problem $1|r_j|\sum C_j$ is then NP-hard as well. The hardness here is in the ordinary sense: the construction is polynomial only in the multiplicity encoding (see below), and the reduction is from KNAPSACK, which has a pseudo-polynomial algorithm.

The result is proved on paper. A formalization adds a machine-checked complexity reduction whose correctness proof is a sequence of delicate counting estimates with large explicit constants; the paper closes the converse with "as is easily seen", and the forward computation and claims (C), (D) contain displayed identities that a formal proof must verify exactly. The definitions (single-machine schedules with release dates, the schedule of a processing order, the multiplicity encoding) are reusable for the other single-machine reductions of the same paper and for later classification results.

Difficulty

The forward direction is a direct computation. The converse is where the difficulty lies: a schedule with $\sum_jC_j\le y$ is arbitrary, may contain idle time, and may interleave the groups. Such a schedule must be shown to be rigid (claims (A)–(D)), and the claims are statements about every schedule, not about a convenient one. Each step compares sums of the form $\sum jτ$ against $u$ with an additive slack smaller than $\tau$ , so the constants must be tracked exactly; an estimate that loses a single $\tau$ breaks the argument. Extracting the knapsack subset at the end requires recognizing which $t$ jobs fill $[0,t\tau+b)$ and why their extra lengths $a_j$ sum to exactly $b$ .

For the goal, the polynomiality of the reduction is not automatic: the constructed instance has $t'=t(t+1)a_*$ and $u$ jobs, which is exponential in the length of the binary KNAPSACK input. The paper's Remark (p. 23) resolves this by encoding groups of identical jobs by their cardinality and one copy of their data, and the formal statement adopts that encoding.

Formalization scope

Reducibility is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (polynomial-time many-one reducibility in Cook's machine model). Numbers are coded in binary over the four-letter alphabet BSym with encNats from the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's formalization); its own subsetSumLang allows zero entries, so KNAPSACK over positive integers is defined here.
Jobs are indexed by Fin n, 0-based; the groups $T$ , $T'$ , $U$ and $J_n$ are index ranges. Starting times are natural numbers: the paper computes them from processing orders on integer data (Section 3), and claim (D) is false for real starting times.
A schedule is feasible when every job starts at or after its release date and the occupied half-open intervals $[B_j,B_j+p_j)$ are pairwise disjoint; idle time is allowed.
"Precedes" in claims (A) and (C) means "starts earlier on the machine"; there are no precedence constraints.
The claims are stated with exactly the hypotheses the proof uses: the schedule is feasible and $\sum_jC_j\le y$ , for positive $a_j$ , $b$ with $0<b<A$ (the paper's "We may assume that $0<b<A$ ", p. 16).
The halves in $u$ and $y$ are exact natural-number divisions, since the products are even. The letter $u$ is both the size of $U$ and the bound $\sum_{j\notin U}C_j\le u$ , as in the paper.
The goal's target language uses the multiplicity encoding: a list of job types (count, processing time, weight, release date) and $y$ ; the class conditions (unit weights, release date $0$ for every job but the last) are checked on the expanded job list. A one-entry-per-job encoding would make the paper's construction non-polynomial, and the statement would not be the paper's.
Trivializing formalizations are ruled out: the goal includes polynomial-time computability (not just an equivalence of yes-instances), the KNAPSACK language requires positive entries as in the paper, and the target language requires class membership, so mapping to an instance outside the class is not a way out.
Welcome contributions: the arithmetic identities of the construction, the schedule of a processing order and its feasibility, the counting lemmas behind (C) and (D), and polynomial-time computability of the multiplicity-encoded construction in the CookPvsNP model.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
S. A. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 1971, 151–158. https://doi.org/10.1145/800157.805047
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, D. B. Shmoys, Sequencing and scheduling: algorithms and complexity, Handbooks in OR & MS 4, 1993, 445–522. https://doi.org/10.1016/S0927-0507(05)80189-6

14 thms3 active usersReviewed

Combinatorics Operations Research·Captain: mikedeng1

One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties 1: Minimizing the Total Discrepancy from Preferred Times Is NP-CompleteResearch Paper

Motivation

Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.

Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.

A short history of the model:

Kanet (1981) minimized total absolute deviation from a common due date that is large enough not to constrain the schedule, by a sorting rule. The special case in the middle of §2.1 is the midtime version of this problem.
Garey, Tarjan and Wilfong (1988) proved the problem with arbitrary preferred times NP-complete (THEOREM 1, this mission), and gave an $O(N\log N)$ algorithm for a fixed task order.
Hall, Kubiak and Sethi (1991) proved that the common-due-date problem becomes NP-hard when the due date is restrictive. The reduction of THEOREM 1 already uses a common preferred midtime that is not large, together with one extra task that pins the right end.

Setting

There are $N$ tasks $T_1,\dots,T_N$ . Task $T_i$ has a length $l_i$ and a preferred midtime $M_i$ . A schedule $S$ assigns every task a starting time $s_i\ge0$ such that no two tasks overlap on the single processor: for $i\ne j$ , either $s_i+l_i\le s_j$ or $s_j+l_j\le s_i$ . Idle time is allowed. The actual midtime of $T_i$ is $m_i(S)=s_i+l_i/2$ , and the total discrepancy of $S$ is

\mathrm{cost}(S)=\sum_{i=1}^N |m_i(S)-M_i| .

The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times $a_i$ are interchangeable through $a_i=M_i-l_i/2$ .

Total discrepancy (the decision problem). Given $N,k\in\mathbb Z^+$ and $M_i,l_i\in\mathbb Z^+$ , is there a schedule with $\mathrm{cost}(S)\le k$ ?

Even-odd partition. Given positive integers $x_1<x_2<\dots<x_{2n}$ , can they be split into two sets of equal sum so that each set contains exactly one of $x_{2i-1},x_{2i}$ for every $i$ ?

The special case. For tasks $T_0,\dots,T_{2n}$ with $0<l_0<l_1<\dots<l_{2n}$ and one common preferred midtime $M>\sum_i l_i$ , write $A(S)=\{T_i: m_i(S)<M\}$ and $B(S)=\{T_i:m_i(S)>M\}$ . A schedule is ordered if, on each side of $M$ , shorter tasks lie nearer to $M$ . The bracket $[A_n,\dots,A_1,T_0@M,B_1,\dots,B_n]$ is the schedule that puts $T_0$ at midtime $M$ and packs the listed tasks against it in the listed order.

Formalization targets

Goal: THEOREM 1

\text{Partition is NP-complete}\ \Longrightarrow\ \text{Total discrepancy is NP-complete.}

The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.

Milestones, in attack order

Even-odd partition is in NP; the instance $x_1=1$ , $x_{2i}=x_{2i-1}+y_i$ , $x_{2i+1}=x_{2i}+1$ built from a Partition instance $Y$ is a yes-instance if and only if $Y$ is; and LEMMA 1, even-odd partition is NP-complete.
The special case: a minimum cost schedule has no gaps and is ordered; LEMMA 2 (some $m_i(S)=M$ ), LEMMA 3 ( $|A(S)|=|B(S)|$ ), LEMMA 4 ( $m_0(S)=M$ ), LEMMA 5 (swapping $A_i$ and $B_i$ in a bracket keeps the cost), LEMMA 6 ( $\{A_i,B_i\}=\{T_{2i},T_{2i-1}\}$ in a minimum cost bracket), and the minimum cost

k=\sum_{i=1}^n(l_{2i}+l_{2i-1})\left(n-i+\tfrac12\right)+l_0\,n .

At the midtime $M=\frac12\sum_{i=0}^{2n}l_i$ used in the reduction, every schedule of $T_0,\dots,T_{2n}$ costs at least $k$ ; equality forces the ordered, gap-free form in item 2.
The reduction: the instance D with $l_0=x_1-1$ , $l_i=x_i$ , $l_{2n+1}=2$ , $M_j=M=\sum_{i\le 2n}l_i/2$ , $M_{2n+1}=2M+1$ has a schedule of cost at most $k$ if and only if $X$ has an even-odd partition. Total discrepancy is in NP.

Significance

THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at $M$ , the $i$ -th pair of lengths in the $i$ -th positions on either side, either member on either side. This characterization holds independently of the reduction.

The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with $M=\sum_i l_i/2$ , so they must be restated for every $M$ . Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.

Difficulty

The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint $s_i\ge0$ never binds. In D the midtime is $M=\sum_{i=0}^{2n}l_i/2$ , exactly half the total length, and the reduction works because the constraint binds. The tasks before $M$ must fit in $[0,M-l_0/2]$ , and the extra task $T_{2n+1}$ must sit at $[2M,2M+2]$ . Together these force the two sides to have equal total length. A proof that only cites the large- $M$ lemmas proves nothing about D. Conversely, dropping $s_i\ge 0$ makes the reduction false: put the shorter element of every pair after $M$ .

The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of $X$ , double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.

Formalization scope

Everything is real-valued except the instance codes. Schedules have real starting times $s_i\ge0$ , and integer data are cast to $\mathbb R$ . Restricting to integer starting times would be a different problem and is not what is stated.
Nonnegative starting times are a standing assumption. The paper uses them ("scheduled between 0 and $M-l_0/2$ ", p. 336) without writing them into the model. Nonoverlap is "one task finishes before the other starts", the reading of "intersect only at their endpoints".
Tasks are indexed by Fin N from $0$ . In the special case $T_i$ is index $i$ , and the paper's $T_{2i-1},T_{2i}$ ( $1\le i\le n$ ) are the indices $2k+1,2k+2$ for $k=i-1$ .
Languages use the published CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.
The goal is not the combinatorial equivalence of milestone 4. It states NP-completeness, so it contains the polynomial-time computation of the reduction and membership in NP. Taking NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.
Running times of the algorithms of §2.2–§2.4 are out of scope for this mission, as are all results after §2.1.

Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.

Selected references

M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28(4):643–651, 1981. https://doi.org/10.1002/nav.3800280411
N. G. Hall, W. Kubiak, S. P. Sethi, Earliness–tardiness scheduling problems, II: Deviation of completion times about a restrictive common due date, Operations Research 39(5):847–856, 1991. https://doi.org/10.1287/opre.39.5.847
S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

19 thms3 active usersReviewed

Complexity Theory Operations Research·Captain: mikedeng1

Complexity of Machine Scheduling Problems 7: Makespan Reduces to Total Completion Time on Identical Machines with Precedence ConstraintsResearch Paper

Motivation

Scheduling jobs on parallel machines under precedence constraints is the core model of project and parallel-processing scheduling: a job may start only after its predecessors have finished. Two criteria dominate the literature, the makespan $C_{\max}$ (when does the last job finish?) and the total completion time $\sum_j C_j$ (how long do jobs wait on average?). Knowing that one criterion is at least as hard as the other lets a hardness proof for one transfer to the other without a new reduction from a combinatorial problem.

Brucker, Lenstra and Rinnooy Kan's report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; later in Annals of Discrete Mathematics 1, 1977) collected the complexity status of the standard scheduling problems and stated a set of elementary reductions among them as Theorem 1. Part (l) reduces makespan to total completion time for identical machines with precedence constraints and bounded processing times.

Timeline.

1971–1972: Cook (doi:10.1145/800157.805047) and Karp (doi:10.1007/978-1-4684-2001-2_9) introduce NP-completeness and polynomial reducibility.
1975: Ullman (doi:10.1016/S0022-0000(75)80008-0) proves that the makespan problems $n|2|I,\mathit{prec},1\le p_{j1}\le 2|C_{\max}$ and $n|m|I,\mathit{prec},p_{j1}=1|C_{\max}$ are NP-complete, by reductions from 3-SATISFIABILITY.
1975: Brucker, Lenstra and Rinnooy Kan state Theorem 1(l); their Table III (p. 13) applies it to Ullman's two problems and concludes that the corresponding total completion time problems are NP-complete.

Setting

An instance has $n$ jobs $J_1,\dots,J_n$ , a number $m \ge 1$ of identical machines, a processing time $p_j$ for each job, and a precedence relation $<$ on the jobs: $J_j < J_k$ means that $J_k$ may start only after $J_j$ has completed. Each job is one operation, processed without interruption on any one machine. For a constant $p_*$ , the class $n|m|I,\mathit{prec},1\le p_{j1}\le p_*$ requires $1 \le p_j \le p_*$ for every job and an acyclic precedence relation.

A schedule assigns to every job a machine and a starting time $B_j \in \mathbb N$ ; the completion time is $C_j = B_j + p_j$ . It is feasible if two jobs on the same machine never overlap and $J_j < J_k$ implies $C_j \le B_k$ .

Following the paper, each optimization problem is replaced by its recognition version. Problem $P'$ asks, for an instance and a threshold $y'$ , whether some feasible schedule has $C_{\max} = \max_j C_j \le y'$ . Problem $P$ asks, for an instance of the same class and a threshold $y$ , whether some feasible schedule has $\sum_j C_j \le y$ (all weights $w_j = 1$ ).

$P'$ is reducible to $P$ , written $P' \propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer.

Formalization targets

Goal: Theorem 1(l)

For every constant $p_* \ge 1$ ,

n'|m|I,\mathit{prec},1\le p_{j1}\le p_*|C_{\max} \;\propto\; n|m|I,\mathit{prec},1\le p_{j1}\le p_*,w_j=1|\textstyle\sum w_jC_j .

Milestones

A trivial upper bound. Every instance of $P'$ with $n'$ jobs has a feasible schedule with $C_{\max} \le n'p_*$ .
The construction and the forward direction. For $0 \le y' \le n'p_*$ let $n'' = (n'-1)y'$ , $n = n'+n''$ and $y = ny' + \tfrac12 n''(n''+1)$ , and add $n''$ unit-time jobs $J_{n'+k}$ , each required to follow every original job and every earlier added job. If $P'$ has a schedule with $C_{\max} \le y'$ , the new instance has a feasible schedule with $\sum_j C_j \le y$ .
The backward direction. If every feasible schedule of $P'$ has $C_{\max} > y'$ , every feasible schedule of the new instance has $\sum_j C_j > y$ .

Significance

The result. Theorem 1(l) makes the total completion time problem at least as hard as the makespan problem in the same class. Combined with Ullman's NP-completeness results and Theorem 1(b) (reducibility transfers NP-completeness), it shows that minimizing $\sum_j C_j$ on identical machines with precedence constraints is NP-complete, already for two machines with $p_j \in \{1, 2\}$ and for unit processing times on $m$ machines. These are two rows of the paper's Table III.

Formalizing it. The result is proved on one page of a typewritten report; no machine-checked version exists. The mission produces a scheduling model for identical machines with precedence constraints, binary languages for the two recognition problems, and the reduction in Cook's Turing-machine model. The proof's displayed bounds contain a misprinted index range, which the formal statements correct.

Difficulty

The two criteria are not monotonically related: a schedule with a smaller makespan can have a larger total completion time than one with a larger makespan. So the obvious reduction, keeping the instance and asking for $\sum_j C_j \le n'y'$ , is not an equivalence: a no-instance of $P'$ can have a schedule with small total completion time. The instance has to be changed so that the total completion time is governed by the makespan, and the comparison of the two thresholds must be exact, including the strict inequality on the "no" side, which depends on integral completion times and positive processing times.

The main formal difficulty lies in the reduction itself. A polynomial-time Turing machine must decode the binary instance, check that it belongs to the class (including acyclicity of the precedence relation), compare $y'$ with $n'p_*$ , and write out an instance with $n'' = (n'-1)y'$ additional jobs and a quadratic-size precedence matrix. The size of that output is polynomial only because $p_*$ is a constant: a version with $p_*$ part of the input would make $n''$ exponential in the input length.

Formalization scope

Jobs and machines are indexed from $0$ (Fin n, Fin m). Starting times are natural numbers; Section 3 derives all times from processing orders on nonnegative integer data, and both criteria are regular. " $C_{\max} \le y$ " is written as " $C_j \le y$ for every $j$ ".
The precedence relation is a Boolean matrix. Its acyclicity and $m \ge 1$ are part of the problem class; the paper leaves both implicit, and the claim "any instance has a solution with $C_{\max} \le n'p_*$ " fails without them.
$p_*$ is a constant of the class and a parameter of both languages, not part of the input. All weights in the target problem equal $1$ and are not written.
The threshold $y = ny' + \tfrac12 n''(n''+1)$ is stated in $\mathbb Q$ exactly as printed in the milestones; it is an integer, and the reduction uses its natural-number value.
The paper's displayed bounds $n'y' + \sum_{k=n'+1}^{n}(y'+k) = y$ and $y' + \sum_{k=n'+1}^{n}(y'+1+k) = y$ have a misprinted index range (the sums must run over $k = 1,\dots,n''$ ). The milestones state the end-to-end bounds $\sum_j C_j \le y$ and $\sum_j C_j > y$ .
" $C_{\max} > y'$ " in the backward direction is read as the negation of the forward hypothesis: no feasible schedule of $P'$ has $C_{\max} \le y'$ .
"Reducible" is Cook's polynomial-time many-one reducibility from the published definition CookPvsNP_defs; numbers are written in binary with the alphabet and code encNats of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). The unit-time model ResourceScheduling.Chain.Model (Błażewicz, Lenstra and Rinnooy Kan) has the same feasibility conditions but unit processing times and real start times, so the model here is defined anew.
A trivializing formalization is ruled out: the goal asserts a polynomial-time computable map, not the bare equivalence, and codes of instances outside the class are excluded from both languages, so the reduction cannot exploit malformed inputs.
Contributions welcome: proofs of the three milestones, a Turing-machine library for arithmetic on binary codes (reusable across this series), and a proof of the goal from the milestones.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; published in Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
J. D. Ullman, NP-complete scheduling problems, Journal of Computer and System Sciences 10 (1975) 384–393. doi:10.1016/S0022-0000(75)80008-0
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9

9 thms3 active usersReviewed

Theoretical Computer Science

Missions

Schönhage–Pan–Winograd Bound: omega < 2.522Research Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

CLRS — Chapter 20, §20.5: Strongly Connected Components (Kosaraju) — Correctness and Running TimeTextbook

The mutual-reachability partition

Graph and returned component labels

Formalization targets

Composing a verified traversal

What must be justified

Formalization scope

graph_input.algo

dfs.algo

scc.algo

Selected references

CLRS — Chapter 20, §20.3: Depth-First Search — Correctness and Running TimeTextbook

A traversal forest that later algorithms can reuse

Ordered exploration and event times

Formalization targets

Reuse beyond a single traversal

What must be justified

Formalization scope

graph_input.algo

dfs.algo

Selected references

CLRS — Chapter 20, §20.2: Breadth-First Search — Correctness and Running TimeTextbook

Shortest paths in an unweighted graph

Graph, source, and outputs

Formalization targets

A reusable shortest-path contract

What must be justified

Formalization scope

graph_input.algo

bfs.algo

Selected references

Quantum Amplitude Amplification and Estimation: Est_Amp(A, χ, M) Outputs ã with |ã − a| ≤ 2πk√(a(1−a))/M + k²π²/M² with Probability ≥ 8/π² for k = 1 and > 1 − 1/(2(k−1)) for k ≥ 2Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 12 (Amplitude Estimation)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

CLRS — Chapter 6, §§6.1–6.2, 6.5: Indexed-Heap Sorting — Correctness and Running TimeTextbook

CLRS scope and implementation

Correctness

Running time

Reusable results and milestone

Algorithm source

indexed_heap.algo

sort_indices.algo

Compiler provenance and validation

Attribution and references

Fast Integer Multiplication on Multitape Turing Machines: Schönhage–Strassen and the ToolkitResearch Paper

Motivation

Setting

Formalization targets

Goal: Schönhage–Strassen

Milestones

Formalization scope

Selected references

Integer multiplication: κ = 0.000051016920170078 (community PR #62)Open Problem

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

What Can We Learn Privately? II: Parity Functions Are Privately PAC Learnable from O(d log(1/β)/(εα)) ExamplesResearch Paper

Learning parities under differential privacy

Setting

`graph_input.algo`

`dfs.algo`

`scc.algo`

`graph_input.algo`

`dfs.algo`

`graph_input.algo`

`bfs.algo`

`indexed_heap.algo`

`sort_indices.algo`