Theoretical Computer Science

Prove2Me mission category: Textbook.

Reusable minimum spanning tree algorithms

A minimum spanning tree connects a weighted network at minimum total edge cost. When this routine is part of a larger algorithm, its caller also needs termination, preservation of existing data, and a bound on the work performed. These guarantees belong in a reusable contract, together with the returned mathematical result.

Prim reuses the Fibonacci heap already formalized for Dijkstra, including its published correctness and amortized running-time proofs.

This development follows Introduction to Algorithms (CLRS), fourth edition, Chapter 21, §21.2 for Prim and Theorem 21.1 in §21.1 for safe edges. The Fibonacci-heap analysis is in the publisher's online supplement, retained Chapter 19, §§19.2–19.4, including Corollary 19.5. That supplement is distinct from printed fourth-edition Chapter 19, which concerns disjoint sets. CLRS, fourth edition; official Fibonacci-heap supplement.

Graph, returned tree, and measured work

An undirected weighted graph has vertices 0, …, V−1 and finite adjacency lists. Every edge occurs in both directions with the same integer weight. Weights may be negative. Parallel edges retain separate occurrence identities, and self-loops are permitted. Let m count undirected edge occurrences and E count stored adjacency occurrences: the supplied graph constructor gives E = 2m, including for self-loops. The root satisfies 0 ≤ root < V, and the main result assumes the graph is connected.

The output is a parent sequence, a mutable mathematical function from all integer indices to integers. The root has parent −1; every other declared vertex names its predecessor toward the root. A minimum spanning tree is an acyclic selection of input edges connecting every declared vertex, with minimum total weight among all competing spanning forests. The formal SpanningParents predicate asserts this full property for the returned sequence.

A heap contains mutable sequences, objects, typed collections, and named natural-number counters. A Call contract supplies a finite returning execution in the generated semantics for every caller stack. Runtime T is the increase in clockWork: each of seven Fibonacci-heap event counters and six Prim bookkeeping counters is counted once. This measures explicit source ticks, not elapsed time or integer bit complexity.

Formalization targets

The main target combines termination, minimum spanning tree correctness, preservation of existing caller storage, fresh output allocation, and a bound on the same execution's work. Its statement quantifies a single positive constant before every graph, root, and initial heap:

The constant is independent of the input and its initial counter values. With E = 2m, this is the conventional $O(m+V\log V)$ bound. The logarithmic unit covers a graph containing only the root. The supporting reusable result retains the explicit estimate

FibonacciPrimAnalysis.correctness_and_running_time is the uniform-constant main result. FibonacciPrimAnalysis.summary provides the explicit bound and operation counts through prim_fibonacci.Call; runtimeBound and runtimeScale name the two expressions. The ordinary-output consequences are output_exists and output_with_cost_correct.

The component targets are the existing Fibonacci-heap correctness and amortized contract, the pure safe-edge and parent-tree results, the queue-independent Prim call contract, and their concrete composition. Invalid roots additionally return a fresh all-−1 sequence with zero ticks; no tree property is asserted for them.

What callers can reuse

The Fibonacci heap is reused from the Dijkstra formalization. This mission imports the same published implementation, shared definitions, correctness proofs, and amortized running-time contracts used by Dijkstra with a Fibonacci Heap. The existing heap contract keeps its original Prove2Me identity. Prim does not introduce a replacement heap or repeat its structural and amortized analysis; it proves the new algorithm-specific facts and composes them with that established contract. This reuse demonstrates how a verified data structure can support another algorithm without being formalized again.

The result lets a later algorithm invoke Prim on its current heap and receive a valid new parent sequence, an unchanged graph representation, unchanged preexisting sequences, objects, and typed collections, and a bound on the additional work. Initial counters need not be zero. The generic Prim theorem counts queue operations without depending on Fibonacci-heap internals; the concrete theorem discharges its queue assumptions using the existing published contract.

Prim's mathematical correctness and asymptotic complexity are established textbook results. The Algo2Lean development adds proofs about this actual mutable source program, including termination and storage preservation. Its complete Prim analysis has been checked locally under Lean 4.33.1. Prove2Me has accepted all four new Prim proofs, including the main correctness and running-time theorem, which reuses the already accepted Fibonacci-heap contract. The graph definitions are shared with the Kruskal analysis. Later clients can reuse these components without formalizing the data structure again. Alternative queue implementations and improvements to the explicit constants can retain the same mathematical specification.

Where the formalization is demanding

A minimum key alone does not establish that its parent pointer represents an input edge, that the chosen edges connect all vertices, or that their total weight is globally minimal. Those properties must remain connected to the mutable sequences that the source updates, including when weights tie or are negative.

A heap operation also changes shared mutable storage. Correct queue contents alone do not guarantee preservation of the graph or unrelated caller data. Moreover, some individual Fibonacci-heap operations are expensive despite small amortized budgets. The contract must account for the same evolving queue and counters across calls, rather than assume that every operation starts with an empty heap. These obligations distinguish the complete algorithm contract from a mathematical MST theorem or a count of queue calls.

Formalization scope and source

The .algo code closely follows the textbook pseudocode, with initialization, minimum extraction, and adjacency relaxation expressed as source operations and loops. It uses integer vertex handles and queues a vertex when first discovered. A parent of −1 denotes no discovered predecessor, so undiscovered keys require no artificial infinity. The root is selected before any edge is scanned. Relaxation compares an edge's weight directly; it does not add a path distance.

Inputs are finite linked adjacency lists with bounded endpoints and signed, unbounded integer weights. The theorem assumes a valid graph representation, symmetric adjacency, connectedness, and an in-range root. It assumes neither an existing successful transcript, a correct answer, nor an unverified queue-runtime estimate. The conclusion compares the result with every spanning forest. The whole-graph theorem does not apply to disconnected inputs.

The cost model counts the specified heap and Prim ticks. It does not count every arithmetic operation, sequence access, allocation, or generated transition. Constant-sequence and queue construction add no ticks; constructing the input graph is outside the call. The imported queue API covers the insert/decrease, minimum extraction, and emptiness operations used here; meld and arbitrary deletion are outside this contract.

The compiler is Algo2Lean v0.1.4, whose immutable release commit is 0f79d5e. The Prim example and its proofs are versioned separately from this unchanged compiler release. Compiler-output reproduction and Prove2Me import packaging are separate checks: platform-adapted files need not have the raw generated files' hashes. The compiler does not yet have a formal semantics-preservation proof. The Prim source and proof guide identifies the exact statements, definitions, and source files. The separate example source commit is d832a565.

The project import root is examples. These are its three new source files. The other imports are the existing fibonacci_heap.algo and dijkstra/priority_queue.algo; the heap's independent source and analysis belong to the linked published component.

prim/graph.algo

# An undirected graph with integer edge weights. Each edge is stored in both
# adjacency lists. Negative weights, parallel edges, and self-loops are allowed.

class Edge:
    target: Int
    weight: Int
    next: Edge | None

    def __init__(self, target: Int, weight: Int, next: Edge | None) -> None:
        self.target = target
        self.weight = weight
        self.next = next


class Graph:
    size: Int
    heads: Seq[Edge | None]

    def __init__(self, size: Int) -> None:
        self.size = size
        if size < 0:
            self.size = 0
        self.heads = const(None)

    def add_edge(self, source: Int, target: Int, weight: Int) -> Bool:
        if source < 0 or source >= self.size or target < 0 or target >= self.size:
            return False
        self.heads[source] = Edge(target, weight, self.heads[source])
        self.heads[target] = Edge(source, weight, self.heads[target])
        return True

prim/prim.algo

from prim.graph import Graph, Edge
from dijkstra.priority_queue import PriorityQueue

# Prim's key is the cheapest edge from the growing tree to each vertex.
# parent stores the predecessor; -1 means no predecessor has been assigned.
# Vertices enter the queue when first reached, so infinity need not be encoded.
# The caller supplies an empty queue, zero keys and selected flags, and parents
# filled with -1. The root retains parent -1. Queue and client storage are disjoint.

def scan_edges(queue: PriorityQueue, key: Seq, parent: Seq, selected: Seq,
               vertex: Int, edge: Edge | None) -> None:
    # @scan
    while edge is not None:
        tick("edges")
        target = edge.target
        if selected[target] == 0:
            weight = edge.weight
            if parent[target] < 0 or weight < key[target]:
                # @improve
                key[target] = weight
                parent[target] = vertex
                tick("queue_updates")
                queue.push_or_decrease(target, weight)
                tick("improvements")
        edge = edge.next


def prim(graph: Graph, root: Int, queue: PriorityQueue,
         key: Seq, parent: Seq, selected: Seq) -> Seq:
    key[root] = 0
    tick("queue_updates")
    queue.push_or_decrease(root, 0)
    tick("queue_empty_checks")
    # @extract
    while not queue.is_empty():
        tick("queue_pops")
        vertex = queue.pop_min()
        selected[vertex] = 1
        tick("settlements")
        scan_edges(queue, key, parent, selected, vertex, graph.heads[vertex])
        tick("queue_empty_checks")
    return parent

prim/prim_fibonacci.algo

from prim.graph import Graph
from fibonacci_heap import FibonacciHeap
from prim.prim import prim as grow_tree

# On a connected graph, the returned predecessors describe a minimum spanning
# tree rooted at root. The root has predecessor -1. An invalid root returns -1
# everywhere without constructing a queue.
def prim_fibonacci(graph: Graph, root: Int) -> Seq:
    parent = const(-1)
    if root < 0 or root >= graph.size:
        return parent
    key = const(0)
    selected = const(0)
    queue = FibonacciHeap()
    return grow_tree(graph, root, queue, key, parent, selected)

Selected references

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022, Chapter 21, §§21.1–21.2, Theorem 21.1. Publisher.
• The same authors, Fibonacci Heaps, official online supplement to the fourth edition, retained Chapter 19 of the third edition, MIT Press, 2009/2022, §§19.2–19.4, Corollary 19.5. Publisher's supplement.
• Algo2Lean, version 0.1.4, Lean-targeting compiler and source examples. Compiler and source repository.
• FibonacciQueueAnalysis.contracts, independently verified Fibonacci-heap queue behavior, preservation, and amortized work. Published Prove2Me theorem.

Prove2Me mission category: Textbook.

Reusable shortest-path algorithms

A shortest-path routine is often one component of a larger algorithm. Its useful contract must describe more than its returned numbers: it must also say that the routine terminates, preserves its caller's data, and incurs a bounded amount of work. Without these guarantees at a reusable boundary, each new caller must repeat parts of the implementation analysis.

This mission belongs to a series formalizing Introduction to Algorithms (CLRS), fourth edition. Its reference is Chapter 22, §22.3, Theorem 22.6, which establishes Dijkstra's correctness for nonnegative edge weights. The chosen queue is a Fibonacci heap, whose analysis is in the publisher's online supplement, retained Chapter 19, §§19.2–19.4, including Corollary 19.5 on degree. The fourth edition moved this material online; its printed Chapter 19 instead concerns disjoint sets. CLRS, fourth edition; official Fibonacci-heap supplement.

Graph, program, and measured work

A directed weighted graph consists of a finite set of vertices and a finite list of weighted outgoing edges for each vertex. Here vertices are integers 0, …, V−1, and every weight is a nonnegative integer. The number E counts adjacency-list entries, so parallel edges are counted separately. A source is in range when 0 ≤ source < V.

The program returns a distance sequence: a mathematical function from integer indices to integers, stored through a mutable reference. Its value is −1 at an unreachable vertex and otherwise is the minimum sum of edge weights over paths from the source. It uses a mutable Fibonacci heap to maintain unsettled vertices and their current distance estimates. A new vertex is inserted; a better estimate decreases its existing key.

A heap records the program's mutable arrays, objects, typed collections, and named natural-number counters. A Call contract relates the initial and final heap in the generated execution model: for every caller stack it supplies a finite execution returning the same final heap and result. The reusable theorem gives one such final state with all correctness, preservation, and cost properties together. The runtime T is the change in the sum of seven heap-event counters and six graph-algorithm counters. It measures the explicitly instrumented source operations, rather than elapsed time or integer bit complexity.

Formalization targets

The main correctness-and-running-time theorem has an accepted proof on Prove2Me under Lean 4.33.1.

The capstone target is one reusable contract giving termination, shortest distances, protected caller storage, a fresh result reference, and a total work bound for the same execution. Its main statement quantifies one positive constant before all graph, heap and source inputs:

Thus different proofs may provide different constants without changing the main proposition. The constant cannot depend on the graph or its initial heap. This states the familiar $O(E+V\log V)$ scale while covering small instances. The published Lean statement includes an additional constant $1$ in its runtimeScale. A valid source requires $V\ge1$, so this displayed form absorbs that term into the unspecified constant, at most doubling it. The reusable supporting result retains the explicit estimate

The explicit supporting declaration is FibonacciDijkstraAnalysis.summary; its ordinary-output consequence is output_with_cost_correct. Its named runtimeBound has fixed coefficients. The main proposition is a separate corollary that hides those coefficients and retains the same termination, correctness, allocation, preservation and actual-call guarantees.

The component milestones are the independently verified Fibonacci-heap contract, the generic priority-queue Dijkstra contract, and their concrete composition. The heap milestone includes correct insertion of an absent in-range handle or strict decrease of a present key, extraction from a nonempty represented queue, preservation, and constant/logarithmic amortized budgets. Clients maintain the heap representation and the required separation from protected storage. The generic milestone includes shortest distances and counts of queue and edge operations. The concrete milestone removes abstract queue assumptions by using the verified heap. Invalid sources additionally terminate with a fresh all-−1 result and no ticks.

What clients receive

A verified client can call this implementation and immediately use the resulting distance sequence in another algorithm. It receives the graph representation unchanged, all previously allocated sequences, objects, and typed collections unchanged, a valid newly allocated result, and a bound on the work added to arbitrary initial counters. The result is useful for nested calls: the surrounding computation need not restart its clocks or forget its existing heap.

The mathematical algorithm and its asymptotic bound are established textbook results, not new open problems. The Algo2Lean source development contains the correctness, termination, preservation, and runtime proofs. The complete source project and exact submission files have been checked locally under Lean 4.33.1. This mission presents those proofs as importable definition and theorem nodes, with the source program displayed alongside the generated execution semantics. Future contributions can reuse the heap independently, instantiate the generic queue boundary with another implementation, or improve explicit bounds without redoing the complete graph proof.

Where the formalization is demanding

A heap operation changes a shared mutable representation. Correct abstract queue contents alone do not establish that graph storage survived, that an array reference remains allocated, or that the cost argument describes the same execution as the correctness argument. The contract must connect all these facts rather than leave them as independent assumptions.

Fibonacci heaps also have expensive individual calls despite small amortized budgets. A worst-case bound applied separately to every decrease-key loses the intended running time. The reusable boundary must therefore describe the potential of the evolving queue, not a fresh empty queue for each operation. The generic Dijkstra result must remain independent of the internal tree and pointer representation of its chosen heap.

Formalization scope and source

The .algo code closely follows the textbook pseudocode: initialization, minimum extraction, and adjacency relaxation appear as explicit source loops and operations. Representation choices are made explicit: -1 denotes infinity, flags record settled vertices, and only discovered vertices enter the queue. The routine returns distances without a predecessor tree. Thus it preserves the textbook's shortest-distance algorithm for nonnegative weights, while differing from its all-vertices initial queue and literal notation.

The Lean representation includes finite adjacency lists stored as linked Edge objects, a Graph with typed heads, unbounded mathematical integers, and mutable sequences indexed by every integer. Zero-weight edges, self-loops, parallel edges, and shared adjacency suffixes are allowed. The theorem assumes a valid finite graph representation and an in-range source for its shortest-distance claim. It does not assume the desired distances, a pre-existing execution transcript, or an unverified queue-runtime bound.

The cost model sums the stated named ticks over unbounded mathematical integers and total sequences. It does not count every arithmetic operation, sequence access, allocation, or generated transition. Queue and constant-sequence construction add no ticks; input-graph construction is outside the call being analyzed. The independent queue API covers the operations used here, not heap meld or arbitrary deletion.

The compiler is Algo2Lean v0.1.4, at release commit 0f79d5e. The downloaded website compiler reproduces all 15 generated modules for this project exactly; the manifests identify the compiler and every source file. Byte-for-byte reproduction concerns unmodified compiler output. The Prove2Me transplant separately rewrites module imports/names, declaration packaging, and explicit options as required by the platform; its adapted files are not claimed to have the raw output's hashes. The edits and source mapping are recorded, the adapted dependency closure has been checked, and every theorem's elaborated type matches the original. The supplementary analysis archive contains the uniform-constant capstone, a reproducible source build, and an independent statement readback. The handwritten libraries include shortest-path mathematics, finite execution and call composition, heap representation, Fibonacci-heap operations, and reusable queue contracts. These boundaries are intended for later CLRS formalizations. The compiler itself is not yet equipped with a formal semantics-preservation proof.

The project import root is examples. The entry file is dijkstra/dijkstra_fibonacci.algo:

from graph import Graph
from fibonacci_heap import FibonacciHeap
from dijkstra.dijkstra import dijkstra as search

# Construct a Fibonacci heap and bind its operations to generic Dijkstra.
def dijkstra_fibonacci(graph: Graph, source: Int) -> Seq:
    distance = const(-1)
    if source < 0 or source >= graph.size:
        return distance
    settled = const(0)
    queue = FibonacciHeap()
    return search(graph, source, queue, distance, settled)

The companion algorithm description displays the complete five-file source: graph.algo, fibonacci_heap.algo, dijkstra/priority_queue.algo, dijkstra/dijkstra.algo, and this entry wrapper. The Fibonacci-heap component also displays its independent source. Improvements to exposed contracts, client examples, and source-level cost models are welcome when they preserve the stated semantics and remain separately checkable.

Selected references

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022, Chapter 22, §22.3, Theorem 22.6. Publisher.
• The same authors, Fibonacci Heaps, official online supplement to the fourth edition, retained Chapter 19 from the third edition, §§19.2–19.4, Corollary 19.5. Publisher's supplement.
• Algo2Lean, version 0.1.4, compiler and source semantics. Compiler and source repository.

Motivation

Sampling an entire finite-state execution is a different computational task from recognizing a supplied word. A membership circuit must answer correctly on its given input. A sampler instead chooses the input together with its associated output, while preserving their joint distribution. This distinction is relevant when finite-state models describe allowable executions and when parallel generation should avoid a sequential pass through every transition. The source paper establishes constant-depth sampling results for regular languages and finite Markov chains in Appendix E (Zhang et al., 2026).

The mission concerns that appendix's finite-state sampling results. It formalizes all six numbered results E.1–E.6, together with the seed bounds stated in the surrounding text. Each milestone points to a published theorem with a separately checked proof. The objects to sample are complete words, word–acceptance pairs, and complete state trajectories. Sampling only the final state would lose the joint temporal information required by the targets.

Finite-state models and fair-bit circuits

A binary deterministic finite automaton has finitely many states, a designated start state, a transition for each state and bit, and a set of accepting states. Starting from its initial state, a binary word of length $n$ determines a run. Let $L$ be the set of words whose final state is accepting. Put $L_n=L\cap\{0,1\}^n$. An arbitrary such automaton represents an arbitrary binary regular language, with no assumption that membership belongs to $\mathrm{AC}^0$.

A finite Markov chain consists of a nonempty finite state set $Q$, an initial probability vector $\mu$, and a row-stochastic transition matrix $P$. Entries are nonnegative real numbers, not restricted to rational numbers. For $\gamma=(x_0,\ldots,x_n)$, its probability is $p_M(\gamma)=\mu(x_0)\prod_{i=1}^{n}P(x_{i-1},x_i)$. The distribution of all $n+1$ states is denoted $\mathrm{Path}_n(M)$. For $F\subseteq Q$, conditioning is allowed when the probability that $X_n\in F$ is positive.

A randomized $\mathrm{AC}^0$ sampler is a deterministic Boolean circuit supplied with independent, unbiased random bits. AND and OR gates have unbounded fan-in; NOT gates and Boolean constants are permitted. Its size is polynomial and its depth has a constant bound independent of trajectory length. Approximate families are nonuniform in both $n$ and their real error tolerance $\epsilon$: existence does not require efficiently computing circuit descriptions or numerical tables from a supplied transition matrix.

Formalization targets

The main goal is the conjunction of all results E.1–E.6, including the linear seed guarantee for E.5. This organizational theorem is not an additional numbered result attributed to the paper. All six milestones must be proved for the goal to hold. The exact Markov sampling criterion in Theorem E.5 is one component. A nonnegative real number is dyadic if it equals $a/2^k$ for natural numbers $a,k$, including zero. A chain is path-dyadic when every finite trajectory, including a trajectory of length zero, has a dyadic probability. The target is

On the left, the family has polynomial size in $n+1$ and depth bounded independently of $n$. A supporting target records the linear fair-bit budget $O_M(n+1)$ when path-dyadicity holds. Lemma E.4 supplies another target: every path-dyadic chain is the coordinatewise projection of a finite chain whose initial and transition probabilities are all dyadic. Path-dyadicity must not be replaced by the stronger requirement that the original transition matrix itself be dyadic (Appendix E.3).

Theorem E.1 concerns exact sampling of a uniformly random word together with its acceptance indicator:

The sampler uses exactly $n$ fair bits, polynomial size, and depth depending only on the fixed automaton. This is a sampling assertion and does not assert that membership can be computed in constant depth on an arbitrary externally supplied word.

Theorem E.2 concerns the uniform law on nonempty $L_n$. For every $0<\epsilon\leq1/2$, the target is

Every possible output is accepted. Size is polynomial in $n+1$ and $1/\epsilon$, and depth depends only on the fixed language or its automaton. In particular, the leading coefficient of the $n$ term in the random-bit bound is one (Appendix E.2).

Theorem E.6 is the corresponding approximate target for trajectories conditioned on $X_n\in F$. It requires total variation error at most $\epsilon$, only positive-probability outputs ending in $F$, $O_M(n+\log(1/\epsilon))$ fair bits, polynomial size in $n+1$ and $1/\epsilon$, and depth depending only on the chain. There is no lower bound on the conditioning probability beyond strict positivity (Appendix E.4).

Lemma E.3 supplies the exact representation used in the Markov construction. A transition-dyadic chain is represented by one binary DFA and a fixed state projection. On a uniform input of length $v+ns$, with positive constants $v,s$, the states observed after $v,v+s,\ldots,v+ns$ bits project to exactly the complete trajectory law of the chain. The same DFA and projection work for every length, including zero.

Significance of the targets

These results separate sampling an input together with its finite-state behavior from computing that behavior on a prescribed input. They also identify a precise obstruction to exact sampling with a finite fair-bit seed: each output probability must be dyadic. Approximate sampling allows arbitrary real transition probabilities while retaining the valid trajectory support. The complete trajectory requirement preserves correlations among all time coordinates.

The formalization makes the circuit model, seed accounting, support guarantees and asymptotic quantifiers explicit and reusable. The theorem statements and their separately submitted proofs have passed the platform verifier. The goal proof imports all six milestones; its E.5 milestone in turn imports both the equivalence and the linear seed theorem. Thus the platform dependency graph covers the entire appendix. Platform verification establishes the formal statements; semantic correspondence is documented in the statement descriptions and source references.

Difficulty

A literal step-by-step implementation of a run makes circuit depth grow with $n$, so it does not meet the constant-depth target. Recognition results alone do not furnish the required joint sampler. For approximate word sampling, an error estimate alone is insufficient: the output must remain in the accepted support, and the coefficient-one seed bound must also hold. For exact Markov sampling, unreachable states and non-dyadic individual transitions prevent identifying the desired criterion with entrywise dyadicity. Conditioning on a rare terminal event must not introduce an unstated dependence on its probability.

Formalization scope

States are indexed by finite types $\mathrm{Fin}(q)$. Binary words have type $\mathrm{Fin}(n)\to\mathrm{Bool}$; trajectories have $n+1$ coordinates. Markov vectors and matrices are real-valued and carry normalization and nonnegativity proofs. Sampling probabilities are defined by counting all seeds that give a particular encoded outcome and dividing by $2^r$. Total variation is half the finite sum of absolute probability differences.

The circuit representation is an explicit topologically ordered gate list with checked wire references. Size counts input bits, gates, gate-input wires and output wires; this yields the usual polynomial-size class. State trajectories use a fixed one-hot encoding at each time coordinate. The invalid-output predicate is checked over every seed, so neither arbitrary decoders nor unrepresented outcomes can satisfy an exact or support-preserving claim. The encodings used by the targets are injective. The circuit family is existentially quantified after the fixed finite-state model; the depth and polynomial constants precede $n$ and $\epsilon$.

Zero-length words and zero-transition Markov paths are included. The word target excludes empty accepted slices. The conditioned target excludes zero-probability conditioning events. Definitions of division by zero still exist as total Lean functions, but the hypotheses exclude those cases from approximate claims. Extensions of these results, reusable finite-state probability lemmas, and further circuit constructions are welcome. No sampler-existence axiom, vacuous model or final-state-only replacement is part of the interface.

Selected references

• Jiarui Zhang, Chengwei Liang, Haozhe Jiang, Binhang Yuan and Jingzhao Zhang. Revision Provably Reduces Sequential Computation in Diffusion Language Models. Zenodo preprint, 2026. DOI 10.5281/zenodo.23105365, Appendix E, Theorems E.1, E.2, E.5, E.6 and Lemmas E.3, E.4, printed pages 33–36.

Matrix multiplication and arithmetic cost

Multiplying matrices is a basic operation whose asymptotic cost is measured by the number of scalar arithmetic operations needed as the matrix dimensions increase. The familiar entry-by-entry algorithm has cubic cost. The question addressed here is how small an exponent can describe exact multiplication of square matrices when algorithms may use more elaborate finite computations. OpenAI's October 2, 2026 paper establishes the bound $9/4$ for matrices over the complex numbers. Its Theorem 1.1 concerns asymptotic arithmetic complexity, with arbitrarily small positive slack in the exponent.

Finite programs and admissible exponents

An arithmetic program is a finite sequence of register computations. A step can load a field constant, read an input entry, or add, subtract, or multiply two values from preceding registers. Constant loads and input reads have zero cost. Each addition, subtraction, and multiplication has cost one. There is no division operation in this program model. Outputs are selected registers, and a program is correct only when these outputs equal the matrix product for every pair of input matrices.

For a field $F$, a real number $\tau$ is an admissible exponent if, for every real $\varepsilon>0$, there exists a real constant $C>0$ such that every integer size $n\geq1$ admits a correct program with cost at most $C n^{\tau+\varepsilon}$. The constant must work uniformly for all sizes and all input entries. The chosen program may depend on $n$ and $\varepsilon$. The definition does not charge for a separate procedure that constructs these programs. The arithmetic matrix multiplication exponent $\omega_F$ is the real infimum of the set of admissible exponents.

Formalization target

The goal is exactly the complex-field exponent conclusion of OpenAI's Theorem 1.1:

In the Lean source, the quantity on the left is OAI.MatrixMultiplication.Arithmetic.omega ℂ. The bound on the right is the exact real rational (9 : ℝ) / 4, equal to $2.25$. The inequality is non-strict. The theorem does not assert a strict inequality below $9/4$, and it is not quantified over arbitrary fields.

The paper also states the corresponding algorithmic conclusion with every positive exponent slack. The goal here retains the exact infimum formulation used by its released comparator challenge. In particular, the bound should not be read as asserting that one fixed family has cost $C n^{9/4}$ without any slack, or that an algorithm is efficient at a specified finite matrix size.

What the formal result provides

The result places $9/4$ above the asymptotic arithmetic exponent in a model with explicitly defined programs, outputs, correctness, and operation counts. It gives a statement that other formal developments can use without leaving those conventions implicit. The dependence on the complex field is part of that statement, so results using another field or another computational model require their own justified connection.

This is a port and verification of an existing proof, not a claim that the source theorem remains unproved. The released Lean development contains the proof entry point. Keeping the original definitions and conclusion allows compatibility changes to be reviewed independently of the mathematical claim.

Why the supporting development matters

An asymptotic exponent bound requires one uniform cost constant for every positive matrix size, while correctness quantifies over all pairs of matrices at each size. A computation for selected dimensions or selected inputs cannot satisfy those requirements. Arguments about tensors must also support the stated arithmetic program cost, including the operations needed for the relevant linear combinations. The infimum formulation makes its defining set and the interpretation of its bounds part of the supporting mathematics, rather than assumptions to insert into the target theorem.

Formalization scope and conventions

The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Matrices are functions on finite index sets. Program evaluation and output selection give exact field values. The main theorem fixes the field to $\mathbb C$, excludes size zero from admissibility, and uses real powers for its cost estimates. Constants may be arbitrary complex numbers; no bit-cost interpretation is asserted.

The definition item preserves the original source block, including its rectangular matrix multiplication definitions and complex dual exponent. Those additional definitions support the shared source development but are not additional mission goals. A complete proof must establish the displayed bound without an admitted lemma, a new axiom, or an assumption equivalent to that bound. Reusable components include the arithmetic program model, finite tensor constructions, asymptotic bounds, and the bridge from tensor rank to arithmetic operations.

Selected references

• OpenAI, An Upper Bound of 9/4 for the Matrix Multiplication Exponent, preprint, October 2, 2026. Paper, Theorem 1.1.
• OpenAI, MatrixMultiplication comparator challenge and Lean development, 2026, source revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Exact challenge statement.

Status: complete. This mission records a finished formalization rather than an open call for work. Every statement below, including the goal, was uploaded together with a proof that the platform has verified, so there is nothing left to prove.

Motivation

The Lovász Local Lemma (LLL) is a basic tool of the probabilistic method. It shows that a collection of rare "bad" events can all be avoided simultaneously, even when the events are not independent, provided each event depends on only a few others. Its best-known application is to satisfiability: a $k$-CNF formula in which every variable appears in few clauses has a satisfying assignment.

Quantum satisfiability ($k$-QSAT) is the quantum analogue of $k$-SAT. Clauses are replaced by projectors acting on $k$ qubits, and the question is whether some nonzero state is annihilated by all of them, equivalently whether the corresponding local Hamiltonian is frustration-free. Bravyi showed that $k$-QSAT is $\mathsf{QMA}_1$-complete for $k \ge 4$, so sufficient conditions for satisfiability are of interest in quantum complexity theory and in many-body physics. Ambainis, Kempe and Sattath (arXiv:0911.1696, J. ACM 2012) proved a quantum version of the LLL in which probability is replaced by relative dimension, and derived a sufficient condition for $k$-QSAT instances to be satisfiable.

Timeline

• 1975. Erdős and Lovász introduce the local lemma, in the symmetric form, to colour hypergraphs (Infinite and Finite Sets, 1975).
• 1977. Spencer publishes the general (asymmetric) form, credited to Lovász, and applies it to Ramsey numbers (Discrete Math. 20, 1977).
• 1985. Shearer determines the optimal dependency condition, in terms of the independence polynomial of the dependency graph (Combinatorica 5, 1985).
• 2009 to 2010. Moser gives a constructive proof for $k$-SAT (arXiv:0810.4812, STOC 2009); Moser and Tardos make the general lemma constructive (arXiv:0903.0544, J. ACM 2010).
• 2011. Kolipaka and Szegedy show that the Moser and Tardos algorithm works throughout Shearer's region, giving an algorithmic proof of Shearer's bound (Moser and Tardos meet Lovász, STOC 2011, 235 to 244).
• 2009 to 2012. Ambainis, Kempe and Sattath prove the quantum local lemma and its $k$-QSAT corollaries (arXiv:0911.1696, J. ACM 59(5):24, 2012).
• 2013. Arad and Sattath (arXiv:1310.7766) and, independently, Schwarz, Cubitt and Verstraete (arXiv:1311.6474) give constructive versions for commuting projectors.
• 2016. Sattath, Morampudi, Laumann and Moessner extend Shearer's criterion to the quantum setting and conjecture that it is tight (arXiv:1509.07766, PNAS 2016).
• 2017. He, Li, Liu, Wang and Xia show that the abstract and variable versions of the local lemma differ: Shearer's bound, tight for the abstract version, is not tight for the variable version (the setting of $k$-SAT, where events are determined by independent variables) for instance when the base graph of the event-variable graph has an induced cycle of length at least 4, while there is no gap when it is a tree (arXiv:1709.05143, FOCS 2017).
• 2017. Gilyén and Sattath give an efficient quantum algorithm for the non-commuting case under a spectral gap condition (arXiv:1611.08571, FOCS 2017).
• 2018 to 2019. He, Li, Sun and Zhang prove this conjecture: Shearer's bound is tight for the quantum local lemma, so in this respect the quantum lemma behaves like the abstract version rather than the variable one; they also show that the tight regions of the quantum lemma and of its commuting variant differ in general (arXiv:1804.07055, STOC 2019).

Setting

Let $V$ be a nonzero finite-dimensional vector space. For a subspace $X \subseteq V$, the relative dimension is

It plays the role of probability: subspaces replace events, intersection replaces conjunction, and $R(X \mid Y) = \dim(X \cap Y)/\dim Y$ replaces conditional probability.

Subspaces $X_1, \dots, X_n$ have dependency sets $\Gamma(1), \dots, \Gamma(n) \subseteq \{1, \dots, n\}$ when, for every $i$ and every set $S$ of indices with $i \notin S$ and $S \cap \Gamma(i) = \emptyset$,

In words, $X_i$ is independent, for relative dimension, of every intersection of subspaces outside its dependency set.

A $k$-QSAT instance on $n$ qubits is a family of projectors $\Pi_1, \dots, \Pi_m$, each acting on a set of $k$ qubits and extended by the identity on the others. It is satisfiable if a nonzero state lies in the kernel of every $\Pi_i$.

The formalization proves the local lemma once, for an abstract valuation: a real function $R$ on a bounded lattice that is nonnegative, monotone and modular, $R(x) + R(y) = R(x \vee y) + R(x \wedge y)$, with $R(\top) = 1$ and $R(\bot) = 0$. Relative dimension on subspaces and the uniform probability on subsets of a finite set are the two instances used.

Formalization targets

Goal: the quantum local lemma (Theorem 14)

Let $X_1, \dots, X_n$ be subspaces with dependency sets $\Gamma(i)$, and let $0 \le y_i < 1$ satisfy $R(X_i) \ge 1 - y_i \prod_{j \in \Gamma(i)} (1 - y_j)$ for every $i$. Then

Other formalized results

All of these are proved on Prove2Me and can be found by name (tag quantum-lll):

1. The same statement for any valuation on a bounded lattice (Theorem 14, abstract form): QLLL.Valuation.lll.
2. The symmetric quantum local lemma: if $R(X_i) \ge 1 - p$, each $X_i$ has at most $d$ dependencies and $p \cdot e \cdot (d + 1) \le 1$, then $R(\bigcap_i X_i) > 0$ (Theorem 4): QLLL.quantum_lll_symmetric.
3. The classical Erdős and Lovász local lemma, asymmetric and symmetric (Theorems 13 and 1), for the uniform probability on a finite set: QLLL.SAT.classical_lll, QLLL.SAT.classical_lll_symmetric.
4. $k$-SAT: a $k$-CNF formula in which every variable appears in at most $2^k/(e k)$ clauses is satisfiable (Corollary 2): QLLL.SAT.sat_of_degree_le.
5. $k$-QSAT: an instance of rank-$\le r$ constraints in which every qubit appears in at most $2^k/(e r k)$ constraints is satisfiable (Corollary 16): QLLL.PiQSAT.inf_ker_extendOp_ne_bot on Mathlib's tensor product, and QLLL.QSAT.satisfiable_of_degree_le for orthogonal projectors.
6. Two results beyond the paper: infinite $k$-SAT (QLLL.SAT.exists_assignment_forall), and the local lemma for infinite index sets under a continuity hypothesis (QLLL.lll_iInf).

Significance

The quantum local lemma gives a sufficient condition for $k$-QSAT satisfiability that depends only on the local structure of the instance: the rank of the projectors and the number of projectors per qubit. It shows that the classical criterion survives the passage from events to subspaces, even though subspaces do not form a distributive lattice. Later work on constructive and tight versions, listed in the timeline, builds on this statement.

All results of this mission are proved and machine-checked. The Lean development was written as a complete formalization of the paper, and every statement here was uploaded together with a proof verified by the platform. What the mission adds is a reusable, Mathlib-based library: the local lemma for abstract valuations, its classical and quantum instances, $k$-QSAT stated on Mathlib's tensor product of qubits, and linear algebra on intersections of tensor products of subspaces that Mathlib does not yet contain. Mathlib currently has no form of the Lovász Local Lemma.

Difficulty

The classical proof uses complements of events and the identity $\Pr(A) + \Pr(A^c) = 1$, together with the distributive law for events. Subspaces satisfy neither in general: the lattice of subspaces is modular but not distributive, and the orthogonal complement does not distribute over intersections. The argument has to be rebuilt from the properties of relative dimension that do hold. For $k$-QSAT, the further difficulty is to show that constraints acting on disjoint sets of qubits are independent for relative dimension, which requires computing intersections and dimensions of tensor products of subspaces.

Formalization scope

Conventions committed to in the Lean statements:

1. The local lemma is stated for $n$ indexed subspaces (or lattice elements) and real weights $0 \le y_i < 1$. An index is never in its own dependency set's complement: independence is required from intersections over sets $S$ that avoid both $\Gamma(i)$ and $i$ itself.
2. Independence is stated in product form, $R(X \cap Y) = R(X) R(Y)$, which agrees with the conditional form of the paper whenever the conditional relative dimension is defined.
3. The quantum lemma holds over any field and requires $V$ to be nonzero and finite-dimensional.
4. The classical lemmas are stated for good events (complements of bad events) under the uniform probability on a finite nonempty set.
5. Qubits: the main $k$-QSAT statement uses Mathlib's tensor product $\bigotimes_{j} \mathbb{C}^2$ and allows arbitrary local operators of rank at most $r$, since only the dimension of their kernels enters. A second form, on functions from bit strings to $\mathbb{C}$, requires the constraints to be orthogonal projectors (idempotent and self-adjoint). Self-adjointness cannot yet be stated on Mathlib's $n$-fold tensor product, which has no inner product in the pinned Mathlib version.
6. Degree conditions are integers: "at most $2^k/(e r k)$ projectors per qubit" is written as at most $D' + 1$ with $\frac{r}{2^k} \cdot e \cdot (k D' + 1) \le 1$, which the paper's hypothesis implies.

An infinite version of $k$-QSAT is deliberately not included. Nonzero subspaces can have all finite intersections nonzero and zero total intersection, so the infinite statement has to be phrased with compatible families of density matrices, and the current Lean formulation does not yet restrict the constraints to positive operators.

The blueprint of the formalization, linking every paper statement to its Lean declaration, is at sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint. Natural extensions, outside the scope of this mission: the orthogonal-projector form of Corollary 16 on Mathlib's tensor product once inner products on $n$-fold tensor products are available, Shearer-type conditions, and a measure-theoretic classical local lemma on general probability spaces.

A note from the contributor

This is my first contribution to Prove2Me, so the definitions, statements, proofs and descriptions may fall short of what an experienced contributor would produce. Some choices may be unidiomatic, some lemmas may duplicate Mathlib, and the split into entries could be better. Every proof is checked by Lean, so the theorems are correct as stated; the question is whether they are stated in the most useful way.

Selected references

• P. Erdős and L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, Infinite and Finite Sets, Colloq. Math. Soc. János Bolyai 10, 1975, 609 to 627.
• J. Spencer, Asymptotic lower bounds for Ramsey functions, Discrete Math. 20, 1977, 69 to 76.
• J. B. Shearer, On a problem of Spencer, Combinatorica 5, 1985, 241 to 245.
• R. A. Moser, A constructive proof of the Lovász local lemma, STOC 2009. arXiv:0810.4812
• R. A. Moser and G. Tardos, A constructive proof of the general Lovász local lemma, J. ACM 57(2), 2010. arXiv:0903.0544
• A. Ambainis, J. Kempe and O. Sattath, A quantum Lovász local lemma, J. ACM 59(5):24, 2012. arXiv:0911.1696
• I. Arad and O. Sattath, A constructive quantum Lovász local lemma for commuting projectors, 2013. arXiv:1310.7766
• M. Schwarz, T. S. Cubitt and F. Verstraete, An information-theoretic proof of the constructive commutative quantum Lovász local lemma, 2013. arXiv:1311.6474
• O. Sattath, S. C. Morampudi, C. R. Laumann and R. Moessner, When a local Hamiltonian must be frustration-free, PNAS 113(23), 2016. arXiv:1509.07766
• A. Gilyén and O. Sattath, On preparing ground states of gapped Hamiltonians: an efficient quantum Lovász local lemma, FOCS 2017. arXiv:1611.08571
• K. He, Q. Li, X. Sun and J. Zhang, Quantum Lovász local lemma: Shearer's bound is tight, STOC 2019. arXiv:1804.07055

All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph.

We strengthen the previously formalized $O(n^{2.99942})$ bound to $O(n^{2.9983})$ for deterministic APSP on directed graphs with polynomially bounded integer weights and no negative cycles, using the same word-RAM model. It formalizes the improvement outlined by Alman and Vassilevska Williams in their conclusion.

References:

1. Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026, Theorems 17 and 19 and conclusion footnote 10.
2. Virginia Vassilevska Williams and Ryan Williams, Finding, Minimizing, and Counting Weighted Subgraphs, 2013, Theorem 3.3 and Proposition 3.4.
3. Virginia Vassilevska Williams and Ryan Williams, Subcubic Equivalences Between Path, Matrix, and Triangle Problems, 2018, Theorem 4.2.

Motivation

Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by $H_n$. The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most $f$, giving an $f$-approximation.

Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.

Setting

An instance consists of a finite type $E$ of elements, a finite type $S$ indexing available sets, an assignment $s \mapsto A_s \subseteq E$, and a nonnegative cost $c : S \to \mathbb{R}$. Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are

The frequency of an element is the number of sets containing it, and $f$ denotes the maximum frequency over all elements.

The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given $C$ covers is strictly stronger than coverability of the family.

Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when $E$ is empty, $f = 0$ and the $f$-approximation bound reads $\mathrm{cost}(C) \le 0$, which the certificate's tightness clause forces to be $0 \le 0$ rather than anything false.

Formalization targets

The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.

A primal-dual certificate is a pair $(C, y)$ where $C \subseteq S$ covers $E$, $y$ is dual-feasible, and every $s \in C$ has a tight dual constraint, $\sum_{e \in A_s} y_e = c_s$.

Goal — the primal-dual $f$-approximation

For any primal-dual certificate $(C,y)$ and any fractional cover $x$,

Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover $C$ costs at most $f$ times the fractional optimum and a fortiori at most $f$ times the integral optimum.

The double-counting step

The one substantive step of the goal is split out as its own target: for a primal-dual certificate,

Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most $f$ times. With this and weak duality, the goal is two lines.

The greedy bound

A greedy certificate at ratio $\rho$ is a cover $C$ and a nonnegative $y$ with $\sum_{s \in C} c_s = \sum_{e} y_e$ and $\sum_{e \in A_s} y_e \le \rho\, c_s$ for every $s$. For such a certificate and any fractional cover $x$,

Instantiating $\rho = H_n$ is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.

Set-cover weak duality and LP attainment

Every dual packing is bounded by every fractional cover, $\sum_e y_e \le \sum_s c_s x_s$; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.

Significance

This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no $f$-approximation result to build on.

Difficulty

The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.

Formalization scope

Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.

Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.2, pp. 10–14. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Vijay V. Vazirani, Approximation Algorithms, Springer, 2001, Chapters 2 and 15 — the standard treatment of the greedy and primal-dual set-cover analyses.

Motivation

An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.

This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs $1$ per day and buying costs $B$ once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic $2$-competitive algorithm, and a randomized algorithm whose competitive ratio tends to $e/(e-1)$, due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.

Setting

An instance is a pair $(B, k)$: the purchase price $B$, a positive integer, and the number $k \ge 0$ of ski days, which the online algorithm does not know. An offline solution either buys at once, paying $B$, or rents on every day, paying $k$; so the offline optimum is

Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable $x$ and one rent variable $z_j$ per day $j$:

Its dual is a packing program with one variable $y_j$ per day:

The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.

The fractional primal-dual algorithm maintains $x$, initially $0$. On each new day, while $x < 1$ it sets $z_j \leftarrow 1 - x$, then raises

and sets $y_j \leftarrow 1$; once $x$ has reached $1$ it does nothing further. The free parameter $c$ is then pinned to the value that makes $x$ reach exactly $1$ after $B$ days,

Formalization targets

Goal — the fractional algorithm's competitive ratio at finite $B$

The coefficient is the exact finite-$B$ ratio $1 + 1/c$, left in closed form rather than replaced by a constant. This is deliberate: $\left(1+\frac1B\right)^B$ increases to $e$, so $c < e - 1$ and therefore $1 + 1/c > e/(e-1)$ for every finite $B$. A goal asserting $e/(e-1)$-competitiveness at finite $B$ would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.

Asymptotic companion — where $e/(e-1)$ actually lives

The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.

Parallel target — the deterministic algorithm

Chapter 3's other result, independent of the fractional development.

Significance

The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.

On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.

Difficulty

The offline problem is trivial, and a newcomer's first move — prove $\min(B,k)$ is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:

The optimum is never observed. The algorithm's cost must be compared against $\min(B,k)$ without $k$ being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.

The growth law is piecewise. The update fires only while $x < 1$. Summing the per-day increments therefore does not telescope uniformly: days before $x$ reaches $1$ contribute $1 + 1/c$ each and later days contribute nothing, and the index at which the switch happens is exactly $B$ — which is a theorem about the recurrence, not an assumption.

The constant is forced, not chosen. $c = (1+1/B)^B - 1$ is not a free tuning parameter; it is the unique value for which the geometric sequence $x_j = \bigl((1+1/B)^j - 1\bigr)/c$ hits $1$ at $j = B$, which is in turn what makes the dual solution feasible ($\sum_j y_j \le B$). Dual feasibility and the choice of $c$ are the same fact.

Formalization scope

Conventions this development commits to. The purchase price is a natural number $B$ with $0 < B$, because Chapter 3 uses $B$ simultaneously as a price, as a day index ("buy skis on the $B$th day"), and as the exponent in $(1+1/B)^B$; costs are real numbers, with $B$ and $k$ coerced. Days are indexed from $0$, so day $j+1$ of the prose is index $j$, and Fin k indexes the $k$ days. Real division is total, so $1/0 = 0$; the hypothesis $0 < B$ is what keeps every reciprocal in the development genuine, and without it $c$ would evaluate to $0$ and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day $B$.

A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting $x$ and each $z_j$ range over $[0,1]$; Figure 3.1 on p. 18 prints only $x \ge 0$, $z_j \ge 0$. This mission takes the prose version, $0 \le x \le 1$ and $0 \le z_j \le 1$, as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value $\min(B,k)$, so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.

Ruling out a trivializing formalization. The offline optimum is defined independently, as $\min(B,k)$, and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to $(1+1/c)$ times the number of days on which $x < 1$ — so it cannot be weakened into vacuity without becoming false.

Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.

Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold $\alpha \in [0,1]$ uniformly and buying on the day whose increment of $x$ contains $\alpha$. That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008. Chapter 3, pp. 17–19. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024
• Anna R. Karlin, Mark S. Manasse, Lyle A. McGeoch and Susan Owicki, Competitive randomized algorithms for nonuniform problems, Algorithmica 11(6), 1994, 542–571. https://doi.org/10.1007/BF01294260
• Allan Borodin and Ran El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

Comparing undecidable problems

Computability theory studies which questions admit algorithms and how the unsolvable questions compare with one another. A decision problem can be represented by a set of natural numbers: the question on input $n$ is whether $n$ belongs to the set. Even when there is no algorithm that always answers this question, there may be an algorithm that eventually recognizes every positive instance. Understanding the relative difficulty of such problems is the setting of the Friedberg–Muchnik theorem.

The original paper by Richard M. Friedberg appeared in 1957 under the title Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944). It supplies the historical paper source for this formalization. A. A. Muchnik's independent contribution appeared in Russian in 1956. Friedberg, PNAS 43(2), 236–238; Muchnik, Math-Net bibliography, 1956 entry.

Sets, enumeration, and oracle access

A set $A\subseteq\mathbb N$ is computably enumerable, abbreviated c.e., if membership has a semidecision procedure: on input $n$, the procedure halts exactly when $n\in A$. The older terminology is recursively enumerable, abbreviated r.e. The Lean predicate CEnumerable A uses Mathlib's REPred for this property. A computable set has a decision procedure that terminates on every input and answers membership correctly; this is expressed separately by ComputableSet A using ComputablePred.

For each set $A$, define its characteristic function by

An oracle for $A$ answers requests for this function's values. It always supplies an answer, even if membership in $A$ cannot be computed without an oracle. The declaration setOracle A represents this total function inside Mathlib's type of partial functions from natural numbers to natural numbers.

Write $A\le_T B$ when an algorithm with access to the membership oracle for $B$ computes $\chi_A$ on every input. This is Turing reducibility, expressed by SetTuringReducible A B. The algorithm may make several queries, with later queries depending on earlier answers. Incomparability requires both $A\not\le_T B$ and $B\not\le_T A$; it is stronger than saying the two sets merely have different degrees. These conventions specify the mathematical reading of the supplied Lean definitions.

Formalization target

The goal is the following unconditional existence statement:

Its Lean name is Computability.friedberg_muchnik. No enumeration, pair of sets, or oracle program is supplied as a hypothesis. Both sets must be obtained as witnesses to the conclusion. The statement matches Theorem 26.2 in Arnold W. Miller's Lecture notes in Recursion Theory, Section 26, with the theorem on page 51 and its proof on pages 51–54. Miller, December 3, 2008 version.

Mathematical and formal significance

The target establishes that the c.e. problems have incomparable levels of computational difficulty. Its witnesses cannot be computable: a computable membership procedure would also work in the presence of any other oracle simply by making no queries, contradicting the required nonreducibility. The stronger historical consequence is a positive solution of Post's problem: a c.e. degree can lie strictly between the computable degree and the halting degree. Miller records this consequence separately as Corollary 26.3 on page 54. Miller, Section 26.

The mathematical theorem is established; the work requested here is its Lean 4 formalization. A completed development must construct witnesses, prove their computable enumerability, and exclude oracle computations in each direction using Mathlib's actual reducibility relation. The provided goal currently ends in sorry. Successful compilation of this statement checks its formulation and imports; it does not constitute a proof of the existence result.

Difficulty of simultaneous requirements

The main obstacle is preserving decisions about oracle computations while both sets are still being enumerated. An additional element in one set can change an oracle answer used by an earlier computation, undermining the attempt to separate the other set from it. There are infinitely many candidate programs in both directions. Thus a formal treatment has to justify the eventual stability of the relevant computations as well as the effectiveness of the enumeration. This is the setting of the finite injury argument developed in Miller's proof of Theorem 26.2. Miller, pages 51–54.

Formalization scope

The sets are arbitrary Set ℕ, including the natural number zero in their ambient domain. The oracle answers use natural numbers, with one for membership and zero for nonmembership. Classical reasoning is used to define the oracle for an arbitrary set; it supplies no assertion that this function is computable. Each oracle is nevertheless total. Replacing it with a partial membership recognizer would change the meaning of the target.

The foundation consists of Mathlib.Computability.RE and Mathlib.Computability.TuringDegree, together with the supplied definitions in namespace Computability. SetTuringEquivalent records reducibility in both directions. degreeOfSet maps a characteristic-function oracle to its Turing degree, and CEnumerableDegree says that a degree has a c.e. representative. These additional definitions are retained as useful interfaces, while the root theorem itself is expressed directly with sets and TuringIncomparable.

A complete proof will need representations of effective finite stages and oracle computations, and lemmas relating those representations to the imported predicates. Such infrastructure can support later formalizations involving oracle use, computable enumerations, and priority constructions. Contributions should establish these connections with Mathlib's definitions and finish the unconditional target. The theorem must not be replaced by mere degree inequality, weakened reducibility, or a conditional assertion that assumes the required incomparable sets already exist.

Selected references

• Richard M. Friedberg, Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944), Proceedings of the National Academy of Sciences of the USA 43(2), 236–238, 1957. DOI; free archived paper.
• A. A. Muchnik, On the unsolvability of the problem of reducibility in the theory of algorithms (Russian: Неразрешимость проблемы сводимости теории алгоритмов), Doklady Akademii Nauk SSSR 108(2), 194–197, 1956. Math-Net bibliography, 1956 entry.
• Arnold W. Miller, Lecture notes in Recursion Theory, University of Wisconsin–Madison, version dated December 3, 2008, Section 26, Theorem 26.2, pages 51–54. Author-hosted PDF.

Motivation

Classical Eilenberg correspondence theorems connect algebraic descriptions of finite-state behavior with language-theoretic closure principles. The version developed by Juan Climent Vidal and Enric Cosme Llópez replaces one-sorted monoids by many-sorted algebras, so that operations may accept arguments of several prescribed sorts and return a value of another sort. This is the natural algebraic setting for typed term languages: a signature records the permitted input and output sorts of each operation, and a language is a family of sets indexed by sorts. The paper proves that two ways of organizing finite-state behavior—through finite-index congruences and through regular languages—determine the same ordered structure. The source is the final section of Climent Vidal and Cosme Llópez, Eilenberg theorems for many-sorted formations, published in the Houston Journal of Mathematics 45(2), 2019.

The companion manuscript A Kleene theorem for free many-sorted algebras develops the free-term and recognizability infrastructure used by this formalization. It supplies a concrete Lean representation of sorted signatures, free algebras, homomorphisms, terms, and finite many-sorted carriers. The present mission begins from that reusable core and formalizes the formation-level theorem of the HJM paper, rather than repeating the already completed Kleene development.

Setting

Fix a finite type of sorts $S$ and an $S$-sorted signature $\Sigma$. For an $S$-sorted set $X$, write $T_\Sigma(X)$ for the free $\Sigma$-algebra on $X$. A congruence $\Phi$ on a many-sorted algebra is a family of equivalence relations $\Phi_s$, one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family

is finite. A sorted language $L$ is $\Phi$-saturated when membership in $L_s$ is constant on every $\Phi_s$-class. The syntactic congruence $\Omega(L)$ is the greatest algebra congruence that saturates $L$, and $L$ is regular when $\Omega(L)$ has finite index.

A finite-index congruence formation $\mathfrak F$ selects, for every variable family $X$, a nonempty filter $\mathfrak F(X)$ of finite-index congruences on $T_\Sigma(X)$. The selection is closed under intersections, upward inclusion, and pullback along homomorphisms whose composite with the relevant quotient projection is surjective at every sort.

A regular-language formation $\mathcal L$ selects regular languages in each $T_\Sigma(X)$. It contains every language saturated by the universal congruence; whenever $L,K\in\mathcal L(X)$ it contains every language saturated by $\Omega(L)\cap\Omega(K)$; and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.

The two constructions are

and

Formalization targets

The capstone is the paper's final formation theorem: the ordered sets of finite-index congruence formations and regular-language formations are order-isomorphic, with the isomorphism fixed to be exactly the two displayed constructions.

The milestones establish the universal property of the syntactic congruence, closure of finite-index congruences under the filter operations, the well-definedness of each construction, and the two recovery identities

These identities determine the inverse maps and prevent the goal from being satisfied by an unrelated abstract order equivalence.

Significance

The theorem packages a family of finite quotients and a family of regular languages as interchangeable data. On the algebraic side, closure is expressed by filters of congruences and quotient-surjective pullbacks. On the language side, the same information is expressed through saturation by syntactic congruences. The result therefore gives a systematic translation between quotient-based and language-based classifications in a typed, many-sorted setting.

Formalizing the theorem adds congruence, quotient-index, saturation, syntactic-congruence, and formation interfaces to the existing free many-sorted algebra library. These components are reusable for future formalizations of recognizability, Myhill–Nerode principles, finite algebra formations, and varieties or pseudovarieties of typed algebras. The mathematical theorem is already proved in the cited 2019 paper; the remaining task is to produce machine-checked Lean proofs of the source-faithful statements.

Difficulty

The two maps are simple to write down but their inverse laws are not pointwise tautologies. A finite-index congruence must be reconstructed from the family of all languages it saturates, and a language formation must be reconstructed from all selected finite-index congruences. In the many-sorted case, finiteness applies to the entire quotient family, including its support across sorts, and intersections and pullbacks must preserve this global condition. The quotient-surjectivity premise is also essential: replacing it by ordinary surjectivity of the original homomorphism would change the formation axiom.

The syntactic congruence creates a second layer of care. It must be characterized as the greatest compatible sorted equivalence saturating a language, not merely as the kernel of the language's characteristic function, which need not itself respect the algebra operations. Thus an argument that treats saturation as an arbitrary set-theoretic equivalence misses the algebraic compatibility required by the theorem.

Formalization scope

The Lean development uses the existing MSKleene representation of sorted sets, signatures, argument tuples, algebras, homomorphisms, terms, and free algebras. Congruences are sort-indexed setoids with explicit compatibility for every signature operation. Their order is inclusion of relations. Intersection and the universal congruence are concrete constructions, while pullback is defined along an algebra homomorphism.

Finite index is represented by finiteness of the sigma-type of all quotient carriers, matching the paper's finite sorted-set convention; it is not weakened to separate finiteness of each inhabited component. The sort type is assumed finite in the finite-index filter and formation correspondence theorems, as required in the final section of the source. Languages are arbitrary sorted subsets of free term algebras, including empty components. No nonemptiness assumption on variable carriers or algebra sorts is added.

The syntactic congruence is defined internally as the supremum-style least upper bound of all congruences saturating a language, rather than postulated together with its universal property. The formation structures contain only the source closure axioms. In particular, neither correspondence map nor either inverse identity is stored as a structure field; doing so would trivialize the capstone. Contributions are welcome on the foundational universal-property and finite-index lemmas, the two formation constructors, and the recovery identities that assemble into the final order isomorphism.

Selected references

• Juan Climent Vidal and Enric Cosme Llópez, Eilenberg theorems for many-sorted formations, Houston Journal of Mathematics 45(2), 2019, pp. 351–416. arXiv:1604.04792
• Samuel Eilenberg, Automata, Languages, and Machines, Volume B, Academic Press, 1976.
• Adolfo Ballester-Bolinches, Jean-Éric Pin, and Xaro Soler-Escrivà, Formations of finite monoids and formal languages: Eilenberg's variety theorem revisited, Forum Mathematicum 26, 2014, pp. 1737–1761.

Motivation

Kleene's theorem (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the regular ones — those built from finite languages by union, concatenation, and the Kleene star. Mezei and Wright (1967) lifted recognizability off strings, calling a subset of an arbitrary algebra recognizable when it is the preimage of a subset of a finite algebra under a homomorphism. Replacing strings by terms — finite trees labelled by operation symbols — gives the theory of recognizable tree languages and finite tree automata of Gécseg and Steinby (1984), where the Kleene correspondence reappears with a tree concatenation and an iteration operation in the role of the star.

Many computational structures are inherently many-sorted: typed lambda calculi, structured programming languages, process calculi, XML schemas — data and operations organized into distinct sorts. In the many-sorted setting a signature assigns to each operation symbol the sorts of its arguments and of its value, variables carry sorts, and a language is a sort-indexed family of term sets. The predecessor of this mission, Climent Vidal–Cosme Llópez 2020 (CVCL20), established that recognizability over free many-sorted algebras is preserved — and, where applicable, reflected — by substitution, iteration, quotient, inverse tree-homomorphic image, and direct linear image, via finite-index congruences. What CVCL20 left open is the regular side: whether a natural class of many-sorted regular expressions captures exactly the recognizable languages. This mission closes that gap.

Setting

Fix a finite set of sorts $S$. An $S$-sorted set $A = (A_s)_{s\in S}$ is a family of sets; it is finite when $\coprod_{s\in S} A_s$ is finite. An $S$-sorted signature $\Sigma$ assigns to each pair $(\mathbf{s}, s) \in S^\star \times S$ a set $\Sigma_{\mathbf{s},s}$ of operation symbols of arity $\mathbf{s}$ and coarity $s$. A $\Sigma$-algebra $\mathbf{A}$ is an $S$-sorted set $A$ together with, for each $\sigma \in \Sigma_{\mathbf{s},s}$, an operation $\sigma^{\mathbf A}\colon A_{\mathbf s} \to A_s$, where $A_{\mathbf s} = \prod_{j} A_{s_j}$. A homomorphism commutes with all operations sortwise.

The free $\Sigma$-algebra $\mathbf T_\Sigma(X)$ on an $S$-sorted set $X$ of variables has as its sort-$s$ carrier $\mathrm T_\Sigma(X)_s$ the set of $(X,s)$-terms; every $S$-sorted map $X \to A$ extends uniquely to a homomorphism $\mathbf T_\Sigma(X) \to \mathbf A$. Following automata-theoretic tradition, subsets of $\mathrm T_\Sigma(X)$ are called languages. For a sort $s$, a language $L \subseteq \mathrm T_\Sigma(X)_s$ is $s$-recognizable when there are a finite $\Sigma$-algebra $\mathbf N$, a homomorphism $f\colon \mathbf T_\Sigma(X) \to \mathbf N$, and a subset $M \subseteq N_s$ with $L = f_s^{-1}[M]$. Write $\mathrm{Rec}_s(\mathbf T_\Sigma(X))$ for the set of all such $L$.

Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable $z \in X_u$ and a language $L \subseteq \mathrm T_\Sigma(X)_u$, $z$-substitution $\left(\!\begin{smallmatrix}z\\ L\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s$ replaces, in every term of an input language of sort $s$, each occurrence of $z$ independently by a term of $L$. The $z$-iteration is $L^{\star z} = \bigcup_{i\in\mathbb N} L^{i\,z}$, where $L^{0\,z} = \{z\}$ and $L^{i+1\,z} = L^{i\,z} \cup \left(\!\begin{smallmatrix}z\\ L^{i\,z}\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s(L)$. For a finite $S$-sorted set $Z$, the regular signature $\mathrm{Reg}(S,\Sigma,Z)$ expands $\Sigma$ by an empty constant $\varnothing_s$, a binary sum $+_s$, a unary $z$-iteration $(\cdot)^{\star z}$ for each $z\in Z_s$, and a $z$-substitution operation for each $z\in Z_t$. Its terms are the regular expressions over $(S,\Sigma,Z)$; the power algebra $\mathbf T_\Sigma(Z)^\wp$ carries a canonical $\mathrm{Reg}(S,\Sigma,Z)$-algebra structure, and interpreting a regular expression there yields a language $\{R\}^{Z\sharp}_s$. A language $L\subseteq \mathrm T_\Sigma(X)_s$ is $s$-regular when $L = \{R\}^{Z\sharp}_s$ for some finite $Z\supseteq X$ and some regular expression $R$ of type $s$; write $\mathrm{Reg}_s(\mathbf T_\Sigma(X))$.

Formalization targets

Goal — the many-sorted Kleene theorem

The statement fixes no automaton model and no normal form for regular expressions: it asserts only that the two classes of languages coincide, at every sort, for every finite $S$, every finite $S$-sorted signature $\Sigma$, and every finite $S$-sorted set $X$. It splits into $\mathrm{Reg}_s \subseteq \mathrm{Rec}_s$ (Corollary 4.8) and $\mathrm{Rec}_s \subseteq \mathrm{Reg}_s$ (Proposition 4.10).

Significance

The result completes the Kleene–Myhill–Nerode correspondence on the side of universal algebra, uniformly over an arbitrary finite many-sorted signature: it names the exact operations — those of $\Sigma$, plus empty language, union, sortwise substitution, and sortwise iteration — that generate precisely the finite-state behaviours. Over non-free structures the correspondence is known to fail (recognizable but non-rational subsets of a monoid, Eilenberg 1974), which is what makes the free many-sorted algebra the natural home for an exact statement. The forward direction organizes the regular languages into a $\mathrm{Reg}$-algebra and instantiates the closure properties of CVCL20; the converse gives a constructive, syntactic procedure — from a recognizing homomorphism it builds a regular expression denoting the language — generalizing Lemma 2.5.7 of Gécseg–Steinby, itself descended from McNaughton–Yamada.

The paper is new (June 2026) and has no machine-checked proof. This mission produces the first formalization: a reusable Lean development of finite many-sorted universal algebra — signatures, algebras, free term algebras and their universal property, the Artinian subterm order, power algebras, recognizability, and the substitution/iteration calculus — together with the two inclusions and the state-elimination argument. Everything below the §4 headline results is infrastructure of independent value for many-sorted formal language theory.

Difficulty

The converse inclusion is the substance. The single-sorted proof eliminates automaton states one at a time along a single axis; the naive port to the many-sorted case — fix a linear order on all states and eliminate — loses track of the sort at which each elimination happens and does not terminate cleanly. The argument instead carries a sortwise budget: an $S$-sorted family $K \le N$ recording, for each sort $t$, the set $K_t$ of state values still admissible at internal subterms. The induction is on $\lVert\lVert K\rVert\rVert = \sum_{s\in S} k_s$, and each step removes the top state of one chosen sort, so the recursion branches over the sorts whose budget is nonzero and the key identity (Equation (E)) is a union over those sorts. The inductive invariant — the family of auxiliary languages $L_u(C,K,l)$ with its budget bookkeeping — is what separates the many-sorted argument from its ancestor; it is also the part Gécseg–Steinby declare "obvious from the construction" and this proof spells out in full (Claims C1–C6).

Formalization scope

Proposed Lean representation: $S$ a type with [Fintype S]; an $S$-sorted set as S → Type; a signature as a family List S → S → Type with finiteness where the theorems need it; the free algebra as an inductive term type; the power algebra with sort-$s$ carrier Set (T_Σ Z s); $s$-recognizability as the existence of a finite $\Sigma$-algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: $S$ finite throughout; $\Sigma$ finite and $X$ finite for the §4 results (so that only finitely many basic terms exist and the budget induction is well-founded); the regular operations are exactly $\{\varnothing, +, (\cdot)^{\star z}, z\text{-subst}\}$ together with the operations of $\Sigma$ — not an unrestricted Boolean or closure algebra, which would trivialize the statement.

A complete development needs: the many-sorted UA core (sorted sets and maps, signature, algebra, homomorphism, subalgebra, congruence); the free algebra with unique readability (Proposition 3.4) and universal property (Proposition 3.5); the Artinian subterm order (Proposition 3.6); the power algebra; recognizability and $s$-recognizability with the CVCL20 closure results (Propositions 3.29, 3.30, 3.33); the substitution and iteration calculus (Lemmas 3.23, 3.25, 3.28, Corollary 3.17, Lemma 3.18); and the §4 regular-expression layer (Definition 4.1, Proposition 4.3, Corollary 4.4, Definition 4.6). The UA core and the substitution calculus are reusable beyond this mission. Contributions are welcome at every level — the definitions, the closure results, the auxiliary claims C1–C6, and either inclusion.

Selected references

• L. Gong, R. Ruiz Mora, N. Sanmartín Vich, E. Cosme Llópez, A Kleene theorem for free many-sorted algebras, 2026.
• J. Climent Vidal, E. Cosme Llópez, Congruence-based proofs of the recognizability theorems for free many-sorted algebras, Journal of Logic and Computation 30(2) (2020), 561–633. https://arxiv.org/abs/1808.08217
• F. Gécseg, M. Steinby, Tree Automata, Akadémiai Kiadó, Budapest, 1984.
• R. McNaughton, H. Yamada, Regular expressions and state graphs for automata, IRE Transactions on Electronic Computers EC-9 (1960), 39–47.
• S. C. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, Princeton University Press, 1956, 3–42.
• J. Mezei, J. Wright, Algebraic automata and context-free sets, Information and Control 11 (1967), 3–29.
• S. Eilenberg, Automata, Languages, and Machines, Vol. A, Academic Press, New York, 1974.

Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every $n\ge 3$, an eventual quantitative upper bound, the conclusion $f(n)=n^{1/2+o(1)}$, and the exact affirmative answer to the original upper-bound question.

Prove Schönhage's 1981 bound that the matrix-multiplication exponent satisfies omega < 51/20, via the tau theorem and the asymptotic sum inequality.