The TCS Formalization Drive

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…

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…

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…

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…

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…

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…

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