Theoretical Computer Science

Motivation

Mean-payoff games ask which starting positions allow a player to guarantee a nonnegative long-run average reward. Binary-encoded weights make the bit cost of solving the complete winning set a central part of the question. The source manuscript presents the surrounding research claim.

Setting

A game is a finite nonempty directed multigraph with integer edge weights, an owner for each vertex and an outgoing edge everywhere. Winning means that a history-dependent maximizer strategy guarantees liminf average payoff at least zero against every opponent strategy.

Formalization target

Construct one randomized three-tape machine and C>0 such that every encoded game of length L has a time bound

$$T\le2^{C(\log_2(L+2))^2},$$

all T-bit random tapes halt by T, and at least 7/8 of them output the exact winning-set indicator, with all other output cells blank.

The selected formal target is OAI.randomized_quasipolynomial_mean_payoff.

Significance and status

The target makes the input encoding, computation model, success fraction and complete output explicit. It is an existence theorem for a uniform machine, not a separate solver for each game. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The running time must hold on every random tape, while correctness holds on the specified fraction. Signed weights and the full binary input length cannot be replaced by unary magnitude bounds.

Formalization scope

The published definitions specify games, strategies, plays, liminf payoffs, serialization and tape transitions. The independent finite Truffet elimination counterexample is retained as contextual reference; it is not a prerequisite or an asserted proof of the randomized algorithm. The manuscript’s certification/always-correct consequence is not an additional attached goal.

Selected references

• OpenAI, Randomized quasipolynomial-time mean-payoff games, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Embedding edit distance into ℓ₁ would permit algorithms and geometric tools for that normed space. Distortion lower bounds quantify the loss any such representation must incur. The source manuscript presents the surrounding research claim.

Setting

Edit distance is the least number of unit insertions, deletions and substitutions, with unrestricted intermediate word lengths. For a finite equal-length binary set W, c₁(W) is the infimum over all injective maps into the full real sequence space ℓ₁ of the product of the two worst distance ratios.

Formalization target

Find an absolute c>0 and d₀ such that for every d≥d₀ there are 1≤n≤d and at least two binary words of length n with

$$c_1(W)\ge\exp\!\left(c\sqrt{\log d\,\log\log d}\right).$$

The selected formal target is OAI.TreeEdit.binary_lower_bound.

Significance and status

The witness exists for every sufficiently large length cap. The target bounds distortion against every injective ℓ₁ embedding, not only a particular algorithm. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A bad map is not a lower bound for the infimum over all maps. The finite family must force distortion uniformly while preserving its common binary word length.

Formalization scope

The chosen target uses Word Bool n and Finset witnesses. A companion binary_torus formulation is retained as a reference to the same lower-bound endpoint. Its independent source group repeats edit-distance declarations and is not combined into one import. No companion upper embedding theorem is attached.

Selected references

• OpenAI, Tree Constructions for the l1 Distortion of Binary Edit Distance, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Automatic verification of programs that manipulate pointers needs procedure specifications: preconditions saying which part of the heap a procedure touches and postconditions saying what it leaves behind. Writing them by hand does not scale to millions of lines of code. Calcagno, Distefano, O'Hearn and Yang (J. ACM 58(6), 2011) infer them compositionally with bi-abduction: when symbolic execution reaches a call whose precondition is not implied by the current state, it asks for the missing memory $M$ that would make it hold. This abduction question in separation logic,

$$\Delta * M \models H,$$

is the engine behind the Abductor tool and, later, Facebook Infer.

The question has many solutions ($M = \mathsf{false}$ is always one), so its quality matters. The paper defines an order $\precsim$ on solutions that prefers less memory and then logical strength, shows that a best solution always exists as a semantic object, and then asks whether it can be written down and computed in the language that the analysis actually manipulates: symbolic heaps. For the fragment whose only spatial predicate is points-to, it answers yes. That answer, Theorem 3.25, is the goal of this mission.

Setting

Values are natural numbers; $0$ is nil and the nonzero naturals are the locations. A heap $h$ is a finite partial map from locations to values; a stack $s$ assigns a value to every variable; a state is a pair $(s,h)$. Write $h = h_0 \uplus h_1$ when $h_0,h_1$ have disjoint domains and $h$ is their union. A predicate is an arbitrary set of states. On predicates:

• $s,h \models F * G$ iff $h = h_0 \uplus h_1$ with $s,h_0 \models F$ and $s,h_1 \models G$;
• $s,h \models F \mathbin{-\!\!*} G$ iff for every $h'$ disjoint from $h$ with $s,h' \models F$, we have $s,h \uplus h' \models G$;
• $\mathsf{emp}$ holds in the empty heap, $\mathsf{true}$ everywhere, and $\neg$, $\vee$, $\wedge$, $\exists X$, $\forall X$ are the Boolean and quantifier operations; $F \models G$ is inclusion.

Symbolic heaps of the Points-to Instantiation. Expressions $E$ are variables or natural-number constants. A pure formula $\Pi$ is a conjunction of $E = E'$ and $E \neq E'$. A spatial formula $\Sigma$ is a $*$-conjunction of points-to facts $E \mapsto E'$, possibly with $*\,\mathsf{true}$; here $s,h \models E \mapsto E'$ iff $[\![E]\!]s \neq 0$ and $h$ is the one-cell heap $[\,[\![E]\!]s \mapsto [\![E']\!]s\,]$. A symbolic heap is $H = \exists \vec X.\, \Pi \wedge \Sigma$, and a disjunction $D = H_1 \vee \dots \vee H_n$. In the abduction question (5), $\Delta * D \models H$, the left-hand side $\Delta = \Pi \wedge L_1 \mapsto R_1 * \dots * L_n \mapsto R_n$ is quantifier-free.

Orders. $M \le M'$ iff $M' \models M * \mathsf{true}$ (spatially smaller), and

$$M \precsim M' \iff (M \le M' \wedge M' \not\le M) \vee (M \le M' \wedge M' \le M \wedge M \models M').$$

$\min(F)$ keeps the states of $F$ no proper subheap of which (with the same stack) is in $F$. $\mathrm{Elsewhere}(F) = \neg(F \mathbin{-\!\!*} \mathsf{false})$ says that some separate heap satisfies $F$, and the compatible preorder is $D \le_c D' \iff (D \wedge \mathrm{Elsewhere}(\Delta)) \le (D' \wedge \mathrm{Elsewhere}(\Delta))$. Subtraction is $F - G = F \wedge \neg((\neg\mathsf{emp}) * G)$.

Formalization targets

Goal: Theorem 3.25

There is a single algorithm $f$ such that for every quantifier-free $\Delta$ and symbolic heap $H$ of the Points-to Instantiation, the disjunction $D = f(\Delta, H)$ satisfies

$$\Delta * D \models H \quad\text{and}\quad D \precsim M \ \text{ for every predicate } M \text{ with } \Delta * M \models H.$$

Both halves are part of the goal: the best solution is expressible as a disjunction of symbolic heaps, and it is computable.

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

1. Lemma 3.16. If $D$ is a minimal solution w.r.t. $\le_c$, then $\min(D \vee \neg\mathrm{Elsewhere}(\Delta))$ is the minimal solution w.r.t. $\precsim$.
2. Figure 2 derives solutions (§3.4.2). If $\Delta * [D] \triangleright H$ is derivable, then $\Delta * D \models H$.
3. Lemma 3.18. For all $\Delta, H$ some $D$ with $\Delta * [D] \triangleright H$ is derivable, and the proof search terminates.
4. Lemma 3.19. If $\Delta * [D] \triangleright H$ is derivable and $\Delta * F \models H$, then $D \le_c F$.
5. Lemma 3.20. $\mathrm{Incompat}(\Delta)$ and $\neg\mathrm{Elsewhere}(\Delta)$ are semantically equivalent.
6. Lemma 3.23. Six algebraic properties of subtraction, including $\min(F_1 \vee \dots \vee F_n) = G_1 \vee \dots \vee G_n$ with $G_i = ((F_i - F_1)\cdots - F_n)$.
7. Quantifier removal for pure formulae (§3.4.4). $\exists X.\Pi$ is equivalent to a computable pure formula without $X$.
8. Subtraction with quantifiers (§3.4.4). $(\exists\vec X.\Delta) - (\exists\vec Y.\Delta')$ is a computable disjunction of symbolic heaps.

Significance

The result. Semantically the best solution is $\min(\Delta \mathbin{-\!\!*} H)$ (Theorem 3.13 of the paper), a formula that nests $-\!\!*$ and negation around $*$, which no automatic separation-logic prover handles and which says nothing directly about the shape of the missing memory. Theorem 3.25 shows that in the points-to fragment this object collapses to a finite disjunction of symbolic heaps, the format in which an analysis draws "pictures of memory", and that it can be computed. It gives an optimal abduction procedure against which the paper's heuristic procedure can be measured.

Formalizing it. The theorem is proved in the paper, but several steps are given as sketches ("the proof of each of these properties is straightforward", "a straightforward exercise"), Lemma 3.18 has only a proof sketch, and the quantifier-free subtraction display on p. 33 is incomplete as printed (it inspects only the points-to facts and not the pure part of the subtracted heap). A machine-checked development would supply the missing arguments, fix the subtraction step, and give a verified reference implementation of optimal abduction for points-to symbolic heaps. No part of it is known to have been formalized.

Difficulty

The obvious route is to compute $\min(\Delta \mathbin{-\!\!*} H)$ directly, but $-\!\!*$ quantifies over all heaps, and symbolic heaps have no syntax for it. The paper splits the problem into three phases (a $\le_c$-minimal solution from a proof system, the incompatible solutions, and $\min$), and each phase carries its own difficulty. The proof system's minimality (Lemma 3.19) must hold against arbitrary semantic predicates, not only symbolic heaps, and it fails as soon as $\Delta$ may denote more than one heap for a given stack (the paper notes that adding list segments breaks it). Computing $\min$ needs subtraction of symbolic heaps with quantifiers, which in turn needs quantifier elimination for Boolean combinations of equalities over an infinite domain, and the paper's quantifier-free subtraction step has to be repaired. Showing that the final disjunction is $\precsim$-least, not merely a solution, needs all three phases.

Formalization scope

All statements live in the namespace BiAbduction.Systematic. Values are ℕ with nil 0, locations are the nonzero naturals, variables are ℕ (program and logical variables form one sort), and heaps are maps ℕ → Option ℕ with 0 unallocated and finite domain. Finiteness of heaps is essential, since $\min$ relies on well-foundedness of the subheap order. Predicates are arbitrary Set (Stack × Heap). The syntax is built from ℕ, Bool, Sum, Prod and List by abbreviations, so "computed by an algorithm" is Mathlib's Computable₂ with the standard Primcodable encodings. The left-hand side $\Delta$ has no true conjunct, as in the paper's proofs; the right-hand side may have one. Figure 2 is an inductive relation in which psto may match any right-hand points-to fact. The soundness and $\le_c$-minimality statements assume the paper's bound-variable convention (no variable bound in $H$ occurs in $\Delta$); the goal does not need it.

The goal cannot be met by a degenerate reading. The competitors $M$ range over all predicates, not only over disjunctions, and computability refers to fixed standard encodings. The points-to semantics excludes nil addresses, and heaps are finite.

A complete development needs the separation-logic algebra of predicates (associativity and commutativity of $*$, the adjunction between $*$ and $-\!\!*$), properties of $\min$ under finite heaps, the soundness and minimality of the proof system, quantifier elimination for equality logic, and a computability argument for list-manipulating procedures. The semantic layer and the quantifier-elimination result are reusable beyond this mission. Contributions to any milestone, and to the supporting lemmas of §3.3 (Lemmas 3.10–3.11, Theorem 3.13), are welcome.

Theorem numbers and page references are those of the accepted manuscript of the J. ACM article (72 pages), not of the typeset journal version.

Selected references

• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, Journal of the ACM 58(6), Article 26, 2011. https://doi.org/10.1145/2049697.2049700
• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, POPL 2009. https://doi.org/10.1145/1480881.1480917
• J. Berdine, C. Calcagno, P. W. O'Hearn, Symbolic Execution with Separation Logic, APLAS 2005. https://doi.org/10.1007/11575467_5
• J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002. https://doi.org/10.1109/LICS.2002.1029817
• D. Pym, P. W. O'Hearn, H. Yang, Possible Worlds and Resources: The Semantics of BI, Theoretical Computer Science 315(1), 2004. https://doi.org/10.1016/j.tcs.2003.11.020

Motivation

Automatic program analyses for heap-manipulating code have to infer, for each procedure, a precondition describing the memory the procedure needs. Calcagno, Distefano, O'Hearn and Yang (J. ACM 2011) do this with bi-abduction: at a call site the analysis asks for an anti-frame $M$, the missing memory, and a frame, the memory left untouched, so that the current state together with $M$ meets the callee's precondition. Their tool, Abductor, and its successor Infer, derive specifications compositionally, procedure by procedure, without a whole program.

A natural question is what the inferred preconditions mean. The paper's informal answer is that the analysis aims at footprints: descriptions of the cells a program actually uses. §4.2.4 makes this precise for straight-line sequences of actions: if each precondition is precise and the prover always returns the best anti-frame, the inferred precondition is exactly the footprint. That result rests on the semantic theory of best abductive solutions developed in §3.3: with respect to a natural order, the abduction question $F * M \models G$ has a unique best solution, $\min(F \mathbin{-\!\!*} G)$.

Setting

A heap is a finite partial map from locations to values; a stack maps variables to values; a state is a stack–heap pair $(s,h)$. A predicate is an arbitrary set of states. Write $h = h_0 \uplus h_1$ when $h_0, h_1$ have disjoint domains and $h$ is their union, and $h' \subseteq h$ for a subheap. The separating conjunction $F * G$ holds of $(s,h)$ when $h = h_0 \uplus h_1$ with $(s,h_0) \in F$ and $(s,h_1) \in G$; $\mathsf{true}$ is the set of all states; the separating implication $F \mathbin{-\!\!*} G$ holds of $(s,h)$ when every disjoint $h'$ with $(s,h') \in F$ gives $(s, h \uplus h') \in G$. Entailment $F \models G$ is inclusion.

A solution of the abduction question $F * M \models G$ is any predicate $M$ with $F * M \models G$. Solutions are compared by the spatial preorder and the betterness order

$$M \le M' \iff M' \models M * \mathsf{true}, \qquad M \precsim M' \iff (M \le M' \wedge M' \not\le M) \vee (M \le M' \wedge M' \le M \wedge M \models M').$$

The minimal states of $F$ are $\min(F)$: the states $(s,h) \in F$ such that no proper subheap $h' \subsetneq h$ has $(s,h') \in F$.

An action $\alpha$ is given by its specification $\{P_\alpha\}\,\alpha\,\{Q_\alpha\}$, a pair of predicates. A predicate $P$ is precise if every $(s,h)$ has at most one subheap $h_f \subseteq h$ with $(s,h_f) \in P$. For a nonempty sequence of actions, the safe states and the footprint are

$$\mathrm{safe}(\alpha) = P_\alpha * \mathsf{true},\quad \mathrm{safe}(\alpha;C) = P_\alpha * \big(Q_\alpha \mathbin{-\!\!*} \mathrm{safe}(C)\big),\quad \mathrm{foot}(C) = \min(\mathrm{safe}(C)).$$

The canonical precondition $P_C$ of a sequence, as computed by an ideal bi-abductive prover, is $P_\alpha$ for a single action and $P_\alpha * M$ for $\alpha; C$, where $M$ is the best solution of $Q_\alpha * M \models P_C * \mathsf{true}$.

Formalization targets

Goal: Theorem 4.11 (Deriving Footprint)

If every precondition $P_\beta$ of the sequence is precise and every anti-frame is a $\precsim$-best solution, then

$$\mathrm{foot}(C) = P_C .$$

Milestones

1. Lemma 3.10. $\le$ is a preorder; $M \le \min(M)$ and $\min(M) \le M$; and $M, M'$ are $\le$-equivalent iff $\min(M) = \min(M')$.
2. Lemma 3.11. $\precsim$ is a partial order, and $M' \le M$ implies $\min(M') \precsim M$.
3. Lemma 3.12. $F \mathbin{-\!\!*} G$ is a $\le$-least solution of $F * M \models G$; equivalently $F * M \models G \iff M \models F \mathbin{-\!\!*} G$.
4. Theorem 3.13. The $\precsim$-least solution exists, is unique, and equals $\min(F \mathbin{-\!\!*} G)$.
5. Proof of Theorem 4.11, safe states. $\mathrm{safe}(C) = \mathrm{foot}(C) * \mathsf{true}$ for every sequence.
6. Proof of Theorem 4.11, precision. If $P$ is precise, $\min(P * X) = \min(P) * \min(X)$ for every $X$, and $\min(P) = P$.

Significance

Theorem 3.13 gives the abduction question a canonical semantic answer, and it is the yardstick for every algorithm in the paper: the heuristic procedure of §3.2 is shown not to reach it, and the systematic procedure of §3.4 is proved to compute it on a restricted fragment. Theorem 4.11 connects this semantic optimum to program analysis: on straight-line paths, bi-abduction with an ideal prover infers neither more nor less memory than the program touches. It is the paper's theoretical justification for aiming the analysis at footprints.

Neither result has a machine-checked proof that this mission knows of; the platform has no separation-logic layer at all. The mission produces a self-contained semantic layer for separation logic over a concrete heap model (finite heaps, $*$, $\mathbin{-\!\!*}$, $\min$, the orders $\le$ and $\precsim$, precise predicates) that the companion mission on the systematic abduction algorithm, and later work on frame inference or footprint analysis, can share. The paper proves both results; the work here is to formalize those proofs.

Difficulty

Most steps are short once the definitions are fixed, and the paper states several of them as "immediate". Two points are not. First, $\min(M) \le M$ and the "if" direction of Lemma 3.10(3) need every state of $M$ to lie above a minimal one; this holds because heaps are finite, so the subheap order is well founded, and fails for infinite heaps. Second, the inductive step of Theorem 4.11 passes through $\mathrm{safe}(C) = P_C * \mathsf{true}$ and through distributing $\min$ over a precise $*$-factor. Precision of $P_\alpha$ is what forces the split of a minimal heap of $P_\alpha * X$ to be unique; without it, the two sides of the displayed chain on p. 50 differ. The induction must carry precision for every action of the tail.

Formalization scope

Lean represents values and variables as natural numbers, with $0$ as nil and the nonzero naturals as locations; a heap is a cell map ℕ → Option ℕ with cell 0 = none and finite domain; disjoint union is a relation. Predicates are Set (Stack × Heap), entailment is ⊆, and $\mathsf{true}$ is Set.univ. Program and logical variables are not distinguished, and actions carry no parameters, as in §4.2.4; the stack is the same on both sides of every connective. "The minimal solution w.r.t. $\precsim$" is the $\precsim$-least solution, competing against every predicate, not only symbolic heaps. A sequence of actions is a head action plus a tail list, so the empty sequence never occurs. Theorem numbers and pages are those of the accepted manuscript of the J. ACM article (pp. 1–72, footer "Journal of the ACM, Vol. V, No. N, May 2011"), not of the typeset Article 26.

The paper does not define "the canonical spec" in §4.2.4. The formalization reads it from the proof of Theorem 4.11, as an inductive relation whose anti-frames are arbitrary $\precsim$-least solutions. Defining the anti-frame as $\min(Q_\alpha \mathbin{-\!\!*} (P_C * \mathsf{true}))$ would build Theorem 3.13 into the definition, and dropping precision, allowing infinite heaps or restricting the competitors in the definition of a best solution would change the theorem; all of these are ruled out.

Needed infrastructure: the heap model with union and subheap lemmas, well-foundedness of strict subheap inclusion on finite heaps, the adjunction between $*$ and $\mathbin{-\!\!*}$, and upward closure of $\mathrm{safe}(C)$. Reusable pieces, such as the heap model, the adjunction and the properties of $\min$, are welcome as separate lemmas.

Selected references

• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, Journal of the ACM 58(6), 2011. https://doi.org/10.1145/2049697.2049700
• C. Calcagno, D. Distefano, P. W. O'Hearn, H. Yang, Compositional Shape Analysis by means of Bi-Abduction, POPL 2009. https://doi.org/10.1145/1480881.1480917
• C. Calcagno, P. W. O'Hearn, H. Yang, Local Action and Abstract Separation Logic, LICS 2007. https://doi.org/10.1109/LICS.2007.30
• D. Pym, P. W. O'Hearn, H. Yang, Possible Worlds and Resources: The Semantics of BI, Theoretical Computer Science 315(1), 2004. https://doi.org/10.1016/j.tcs.2003.11.020
• J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002. https://doi.org/10.1109/LICS.2002.1029817

Motivation

The learning with errors (LWE) problem underlies most of post-quantum public-key cryptography. Its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). The reduction is iterative: it repeatedly turns samples of a discrete Gaussian on a lattice into samples of a narrower one. Its classical step, Lemma 3.11, needs the following fact. Adding continuous Gaussian noise to a discrete Gaussian sample gives, up to a small statistical distance, a continuous Gaussian. That fact is Claim 3.9 of the paper. Through Corollary 3.10 it turns a lattice point plus noise into an LWE-type sample with a periodic Gaussian error.

The tool behind it is the smoothing parameter of Micciancio and Regev (SIAM J. Comput. 2007). Above this width a discrete Gaussian on a lattice behaves like a continuous one. Claims of this type have since become standard in lattice-based cryptography: discrete Gaussian sampling, trapdoors, and the convolution theorems of Peikert (CRYPTO 2010).

This mission formalizes Claim 3.9 from the published J. ACM article (Article 34, 2009). The paper's main theorem, Theorem 3.1, is a quantum reduction about efficient algorithms. It is outside this series of missions.

Setting

Work in $\mathbb{R}^n$ with the Euclidean norm and Lebesgue measure. For $s > 0$ the Gaussian function is $\rho_s(x) = \exp(-\pi\|x/s\|^2)$, its shift is $\rho_{s,c}(x) = \rho_s(x - c)$, and $\nu_s = \rho_s/s^n$ is a probability density (Eqs. (4)–(5)). For a countable set $A$, $\rho_s(A) = \sum_{x \in A}\rho_s(x)$.

A lattice $L \subset \mathbb{R}^n$ is the set of integer combinations of $n$ linearly independent vectors. Its dual is $L^* = \{y : \langle x, y\rangle \in \mathbb{Z}\ \forall x \in L\}$, and $\det(L^*) = 1/\det(L)$, where $\det(L)$ is the volume of a fundamental parallelepiped. For $u \in \mathbb{R}^n$ and $r > 0$, the discrete Gaussian $D_{L+u,r}$ is the distribution on the coset $L + u$ with mass $\rho_r(y)/\rho_r(L+u)$ at $y$ (Eq. (6)).

For $\epsilon > 0$ the smoothing parameter $\eta_\epsilon(L)$ is the smallest $s$ with $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$ (Definition 2.10).

The statistical distance of two densities is $\Delta(\varphi_1,\varphi_2) = \int_{\mathbb{R}^n}|\varphi_1 - \varphi_2|$, with no factor $\tfrac12$, so it ranges in $[0,2]$.

Let $r, s > 0$ and $t = \sqrt{r^2+s^2}$. The distribution $Y$ is obtained by sampling $y \sim D_{L+u,r}$ and adding independent noise with density $\nu_s$. Its density is

$$Y(x) = \sum_{y \in L+u} D_{L+u,r}(y)\,\nu_s(x - y).$$

Formalization targets

Goal: Claim 3.9 (p. 34:25)

If $rs/t \ge \eta_\epsilon(L)$ for some $0 < \epsilon < \tfrac12$, then

$$\Delta(Y, \nu_t) \le 4\epsilon .$$

Milestones, in attack order

1. Lemma 2.14 (Poisson summation), already proved on the platform and used here as a reference: $f(L) = \det(L^*)\hat f(L^*)$.
2. The remark after Definition 2.10 (p. 34:19). The map $s \mapsto \rho_{1/s}(L^*\setminus\{0\})$ is continuous and strictly decreasing on $(0,\infty)$, with limits $\infty$ at $0$ and $0$ at $\infty$, and $\eta_\epsilon(L)$ is its inverse.
3. The Fourier transform of a shifted Gaussian (p. 34:25), $\widehat{\rho_{\sigma,c}}(w) = e^{-2\pi i\langle c,w\rangle}\sigma^n\rho_{1/\sigma}(w)$.
4. Claim 3.8 (p. 34:24). If $r \ge \eta_\epsilon(L)$, then $\rho_r(L+c) \in r^n\det(L^*)(1\pm\epsilon)$.
5. Eq. (11) (p. 34:25), $Y(x) = s^{-n}\rho_t(x)\,\rho_{rs/t,(r/t)^2x-u}(L)/\rho_{r,-u}(L)$.
6. The pointwise bound (p. 34:26), $|Y(x) - \rho_t(x)/t^n| \le \rho_t(x)/t^n\cdot 4\epsilon$.

A supporting item states the bridge used in both proofs: if $s \ge \eta_\epsilon(L)$, then $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$.

Significance

Claim 3.9 is what makes Regev's iterative step classical. A discrete Gaussian sample, blurred by continuous noise, cannot be told apart from a continuous Gaussian of the combined width, except with probability $2\epsilon$. Corollary 3.10 projects this onto a direction $z$ and reduces it modulo 1 to obtain LWE samples with periodic Gaussian error $\Psi_\beta$. Without it, the reduction from lattice problems to LWE has no way to produce its error distribution. Claim 3.8, a milestone here, says that above the smoothing parameter the discrete Gaussian measure is almost invariant under shifts. It is the basic estimate of the theory.

The results are proved in the paper; none of them is formalized. Lean's Mathlib has lattices, their covolume, dual submodules and the Gaussian Fourier transform. The platform has the Poisson summation formula for lattices. This mission adds the smoothing parameter, discrete Gaussians on cosets, and the first machine-checked convolution theorem for discrete and continuous Gaussians. Later work, such as Corollary 3.10 or Peikert's general convolution theorem, can build on it.

Difficulty

Neither density is a finite object. $Y$ is an infinite sum over a coset of a lattice, normalized by another infinite sum. A direct term-by-term comparison of $Y(x)$ with $\nu_t(x)$ fails: the sum defining $Y(x)$ is a Gaussian sum over a shifted lattice, and its value genuinely varies with the position of $(r/t)^2x - u$ relative to $L$; for narrow Gaussians the variation is of order one. The claim is that this oscillation is uniformly small, with a relative error that depends only on $\epsilon$, not on $n$, $x$ or $u$. Two ratios of lattice sums must be bounded at once, uniformly in $x$. The constant $4\epsilon$ uses $\epsilon < \tfrac12$ in an essential way, because $(1+\epsilon)/(1-\epsilon)$ must stay below $1+4\epsilon$.

The smoothing parameter is defined as a least element. That the least element exists, i.e. that the infimum is attained, is itself a statement about continuity and strict monotonicity of an infinite sum in its width.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n).
• A lattice is a Submodule ℤ with [DiscreteTopology L] [IsZLattice ℝ L].
• $L^*$ is LinearMap.BilinForm.dualSubmodule (innerₗ _) L.
• $\det(L^*)$ is written $\det(L)^{-1}$ with $\det(L)$ = ZLattice.covolume L.
• Lattice sums are real tsums. They are genuinely summable, so no summability hypothesis is added.
• $\eta_\epsilon(L)$ is the real infimum of $\{s > 0 : \rho_{1/s}(L^*\setminus\{0\}) \le \epsilon\}$. Its attainment is milestone 2, not part of the definition.
• $Y$ is defined by its density, the formula on the first line of the proof.
• $\Delta$ is a lower Lebesgue integral with values in $[0,\infty]$ and no $\tfrac12$. A Bochner integral of a non-integrable difference would be $0$ and make the bound free; this form rules that trivialization out.

Added hypotheses, each disclosed in the item.

• $\epsilon > 0$ in Claim 3.9 and the pointwise bound (Claim 3.8 prints it). Definition 2.10 defines $\eta_\epsilon$ only for $\epsilon > 0$, and for $\epsilon \le 0$ the defining set is empty, so the hypothesis $\eta_\epsilon(L) \le rs/t$ would be vacuous.
• $r > 0$ in Claim 3.8, where $\rho_r$ requires it, and likewise $s > 0$ in the supporting item "$s \ge \eta_\epsilon(L) \Rightarrow \rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$".
• $n \ge 1$ in the smoothing remark, which fails for $n = 0$, where $L^*\setminus\{0\}$ is empty.

Other conventions.

• Lemma 2.14 is printed "for any function", with technical conditions omitted (p. 34:20). The referenced platform theorem is the version for Schwartz functions in translated form; every Gaussian used here is Schwartz.
• Eq. (11) is formalized as the equality of its first and fifth lines, the real-valued completing-the-square identity. The Fourier-side lines are not stated.
• The Fourier transform is Mathlib's 𝓕, $\int h(x)e^{-2\pi i\langle x,w\rangle}dx$, as on p. 34:20.

Reusable beyond this mission: the Gaussian, coset-sum and smoothing-parameter definitions, Claim 3.8, and the shifted Fourier transform. Proofs of any milestone are welcome, and so are proofs of the summability and Schwartz facts for Gaussians on lattices that every milestone needs.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• D. Micciancio and O. Regev, Worst-Case to Average-Case Reductions Based on Gaussian Measures, SIAM Journal on Computing 37(1), 2007. https://doi.org/10.1137/S0097539705447360
• C. Peikert, An Efficient and Parallel Gaussian Sampler for Lattices, CRYPTO 2010, LNCS 6223. https://doi.org/10.1007/978-3-642-14623-7_5

Motivation

The Learning with Errors (LWE) problem, introduced by Regev in On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324), asks to recover a secret vector $s \in \mathbb{Z}_p^n$ from noisy inner products $\langle a, s\rangle/p + e \bmod 1$. The noise $e$ is drawn from a periodic normal distribution $\Psi_\beta$ on the circle $\mathbb{T} = \mathbb{R}/\mathbb{Z}$: a centred normal variable reduced modulo $1$. LWE has since become the main hardness assumption of lattice-based cryptography, including the post-quantum standards built on it.

Regev's reductions repeatedly need to compare $\Psi_\alpha$ and $\Psi_\beta$ for nearby parameters, for instance when the noise parameter is known only up to a small relative error. Claim 2.2 of the paper (p. 34:16) quantifies this: the two periodic normal distributions are close in statistical distance, linearly in the relative change $\beta/\alpha - 1$. This mission formalizes Claim 2.2 and the steps of its proof. The source is the published J. ACM article; the paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series.

Setting

Identify $\mathbb{T} = \mathbb{R}/\mathbb{Z}$ with the segment $[0,1)$ with addition modulo $1$. For $\beta > 0$ the normal density with mean $0$ and standard deviation $\beta/\sqrt{2\pi}$ is

$$\nu_\beta(x) = \frac{1}{\beta}\exp\Bigl(-\pi\Bigl(\frac{x}{\beta}\Bigr)^2\Bigr), \qquad x \in \mathbb{R},$$

(Eq. (5) in dimension one), and the periodic normal density (Eq. (7)) is its periodization

$$\Psi_\beta(r) = \sum_{k=-\infty}^{\infty} \frac{1}{\beta}\exp\Bigl(-\pi\Bigl(\frac{r-k}{\beta}\Bigr)^2\Bigr), \qquad r \in [0,1),$$

the density of a $\nu_\beta$-distributed variable reduced modulo $1$.

The statistical distance of two densities $\varphi_1, \varphi_2$ (p. 34:14) is

$$\Delta(\varphi_1, \varphi_2) = \int |\varphi_1 - \varphi_2|,$$

the integral taken over $\mathbb{R}$ for densities on the line and over $[0,1)$ for densities on $\mathbb{T}$. The paper uses this normalization without a factor $\tfrac12$, so that $\Delta$ ranges in $[0,2]$ on probability densities. In Lean these objects are RegevLWE.PeriodicGauss.nu, Psi, statDist and statDistT.

Formalization targets

Goal: Claim 2.2

For any $0 < \alpha < \beta \le 2\alpha$,

$$\Delta(\Psi_\alpha, \Psi_\beta) \le 9\Bigl(\frac{\beta}{\alpha} - 1\Bigr).$$

The hypotheses and the constant $9$ are exactly as printed.

Milestones

1. The bound on the line (proof of Claim 2.2, first sentence). For $0 < \alpha < \beta \le 2\alpha$,

$$\Delta(\nu_\alpha, \nu_\beta) \le 9\Bigl(\frac{\beta}{\alpha} - 1\Bigr).$$

2. Reduction modulo 1 does not increase $\Delta$ (p. 34:15, used on p. 34:16): for integrable $\varphi_1, \varphi_2$ on $\mathbb{R}$, the periodizations $\tilde\varphi_i(r) = \sum_k \varphi_i(r-k)$ satisfy $\Delta(\tilde\varphi_1, \tilde\varphi_2) \le \Delta(\varphi_1, \varphi_2)$.
3. The three displayed steps of the proof after normalizing to $\alpha = 1$, $\beta = 1 + \epsilon$, $0 < \epsilon \le 1$: the first display (a triangle-inequality split and an exact evaluation), the pointwise bound

$$\bigl|e^{-\pi(1-1/(1+\epsilon)^2)x^2} - 1\bigr| \le \pi\bigl(1 - 1/(1+\epsilon)^2\bigr)x^2 \le 2\pi\epsilon x^2,$$

and the final evaluation

$$\epsilon + 2\pi\epsilon\int_{\mathbb{R}} x^2 e^{-\pi x^2/(1+\epsilon)^2}\,dx = \epsilon + \epsilon(1+\epsilon)^3 \le 9\epsilon.$$

Significance

Claim 2.2 is a stability statement for the LWE error distribution. It lets an algorithm that works for one noise parameter be applied to a nearby one at a controlled cost in statistical distance, which is how Regev's reductions tolerate an approximately known parameter. It also states a quantitative fact about wrapped normal distributions, which appear outside cryptography, for example in directional statistics.

The result is proved in the paper; no machine-checked proof is known to this mission. Formalizing it produces a reusable one-dimensional toolkit: the $L^1$ distance between two centred normal densities, the second moment of a Gaussian in Regev's normalization, and the contraction of $L^1$ distance under periodization. Each of these is a building block for formalizing the rest of the paper's analysis of Gaussian noise.

Difficulty

The arithmetic is elementary; the work is in the analysis. The statement on $\mathbb{T}$ involves infinite series inside an integral, and the passage from the line to the circle requires exchanging a sum over $\mathbb{Z}$ with an integral and controlling the series almost everywhere. A direct attack on $\Psi_\alpha - \Psi_\beta$ termwise on $[0,1)$ does not by itself produce a bound in terms of $\beta/\alpha - 1$; the comparison has to be made on the line first. On the line, the scaling to $\alpha = 1$ is a change of variables in a Lebesgue integral, and the evaluation of $\int x^2 e^{-\pi x^2/\sigma^2}dx = \sigma^3/(2\pi)$ requires Gaussian moment identities in the paper's normalization rather than Mathlib's.

Formalization scope

• Reals and densities. Everything is one-dimensional over $\mathbb{R}$; distributions are represented by their densities, not by measures. $\mathbb{T}$ is the interval Set.Ico 0 1 with Lebesgue measure; $\Psi_\beta$ is a real tsum over $k \in \mathbb{Z}$, which converges absolutely for $\beta \ne 0$.
• Statistical distance. $\Delta$ is a lower Lebesgue integral ∫⁻ ENNReal.ofReal |φ₁ - φ₂| valued in $[0,\infty]$, with no factor $\tfrac12$, as on p. 34:14. Bounds are compared through ENNReal.ofReal. A Bochner integral would be $0$ on a non-integrable difference and would make any upper bound trivially true; the extended-valued integral rules this out.
• Added hypotheses. None on the goal or on the line bound. The modulo-1 milestone assumes $\varphi_1, \varphi_2$ integrable (the paper states the data-processing fact for random variables, whose densities are integrable); only the "modulo 1" instance used in the proof is stated, not the general inequality for arbitrary randomized functions. The pointwise bound is stated for every $\epsilon \ge 0$, a harmless generalization of the proof's range $0 < \epsilon \le 1$. The first display is stated as its three component facts (inequality, evaluation $= \epsilon$, and the rewriting of the integrand), which together give the printed chain.
• No trivialization. The goal is Claim 2.2 on $\mathbb{T}$, not the bound on the line, and neither side can collapse to a junk value: the left side is an extended nonnegative integral and the right side is positive under the hypotheses.
• Welcome contributions. Gaussian moment lemmas in the normalization $e^{-\pi x^2/s^2}$, the periodization contraction for general integrable functions, and a measure-level statement identifying $\Psi_\beta$ with the pushforward of $\nu_\beta$ under reduction modulo $1$.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• D. Micciancio and S. Goldwasser, Complexity of Lattice Problems: A Cryptographic Perspective, Kluwer, 2002 (cited on p. 34:15 for the data-processing property of statistical distance). https://doi.org/10.1007/978-1-4615-0897-7

Motivation

Learning with errors (LWE) asks to recover a secret vector $s \in \mathbb Z_p^n$ from noisy inner products $(a_i, \langle a_i, s\rangle + e_i)$, where the $a_i$ are uniform and the errors $e_i$ are drawn from a narrow distribution $\chi$ on $\mathbb Z_p$. Regev introduced the problem and showed that solving it is at least as hard as solving worst-case lattice problems by a quantum algorithm (Regev 2009). The same paper uses LWE to build a public-key cryptosystem, the ancestor of most lattice-based encryption schemes in use today, including the schemes standardized by NIST in 2024 (ML-KEM, derived from Kyber).

A cryptosystem has two halves: security (an eavesdropper learns nothing about the plaintext) and correctness (the legitimate receiver recovers the plaintext). This mission is the correctness half of Regev's scheme: Lemma 5.1 of the paper, which converts a tail bound on the noise into a bound on the probability that decryption fails. The source is the published article, Journal of the ACM 56(6), Article 34 (2009). The paper's main theorem, a quantum reduction from lattice problems to LWE, is outside this series.

Setting

Fix an integer $p \ge 2$ and let $\mathbb Z_p = \{0, 1, \dots, p-1\}$ with addition modulo $p$. Fix integers $n, m \ge 0$ and a probability distribution $\chi$ on $\mathbb Z_p$. All additions are in $\mathbb Z_p$, and $\langle a, s\rangle = \sum_j a_j s_j$ for $a, s \in \mathbb Z_p^n$.

• Distance from zero. For $a \in \mathbb Z_p$, $|a|$ (absZ) is the integer $a$ if $a \in \{0, \dots, \lfloor p/2\rfloor\}$ and $p - a$ otherwise.
• Convolution powers. $\chi^{\star k}$ (convPow χ k) is the law of the sum of $k$ independent samples from $\chi$; $\chi^{\star 0}$ is the point mass at $0$.
• Private key. $s \in \mathbb Z_p^n$, chosen uniformly.
• Public key. $a_1, \dots, a_m \in \mathbb Z_p^n$ independent and uniform, $e_1, \dots, e_m \in \mathbb Z_p$ independent with law $\chi$, and $(a_i, b_i)_{i=1}^m$ with $b_i = \langle a_i, s\rangle + e_i$ (publicKey).
• Encryption. A subset $S \subseteq [m]$ is chosen uniformly among all $2^m$ subsets. The bit $0$ is encrypted as $\bigl(\sum_{i\in S} a_i, \sum_{i\in S} b_i\bigr)$ and the bit $1$ as $\bigl(\sum_{i\in S} a_i, \lfloor p/2\rfloor + \sum_{i\in S} b_i\bigr)$ (encrypt).
• Decryption. A pair $(a, b)$ decrypts to $0$ if $b - \langle a, s\rangle$ is closer to $0$ than to $\lfloor p/2\rfloor$ modulo $p$, i.e. $|b - \langle a, s\rangle| < |b - \langle a, s\rangle - \lfloor p/2\rfloor|$, and to $1$ otherwise (decrypt, decodeResidue).

The outcome distribution outcome n m χ c of a bit $c$ is the law of the decrypted bit when all of $s$, $a_1,\dots,a_m$, $e_1,\dots,e_m$ and $S$ are drawn as above.

Formalization targets

Goal: Lemma 5.1 (Correctness), p. 34:35

Let $\delta > 0$ and assume that for every $k \in \{0, 1, \dots, m\}$,

$$\Pr_{e \sim \chi^{\star k}}\Bigl[\,|e| < \Bigl\lfloor \frac p2\Bigr\rfloor\Big/2\,\Bigr] > 1 - \delta .$$

Then for each bit $c \in \{0,1\}$,

$$\Pr[\text{decryption of an encryption of } c \text{ equals } c] \ge 1 - \delta ,$$

the probability being over all the randomness of the protocol. The lemma has no hard-coded parameters: $p$, $m$, $n$, $\chi$ and $\delta$ are arbitrary, and the paper's concrete choice ($p$ prime in $[n^2, 2n^2]$, $\chi = \bar\Psi_{\alpha(n)}$) is supplied separately by Claim 5.2.

Milestones (proof of Lemma 5.1, p. 34:36)

1. Residue identity. For an encryption $(a, b)$ of $0$, $b - \langle a, s\rangle = \sum_{i\in S} e_i$; for an encryption of $1$, $b - \langle a, s\rangle = \lfloor p/2\rfloor + \sum_{i\in S} e_i$.
2. Residue law. For a fixed $S$, $\sum_{i\in S} e_i \sim \chi^{\star |S|}$.
3. Rounding. If $|x| < \lfloor p/2\rfloor/2$ then $x$ is closer to $0$ than to $\lfloor p/2\rfloor$, so the residue $x$ decrypts to $0$ and the residue $\lfloor p/2\rfloor + x$ decrypts to $1$.

Significance

The result. Lemma 5.1 is the interface between the noise distribution and the scheme: any bound on the tails of the convolution powers $\chi^{\star k}$, $k \le m$, gives a bound on the decryption error, independently of the security analysis. With Claim 5.2 it shows that the paper's parameters decrypt correctly except with negligible probability. The same template (residue equals accumulated noise; small noise rounds correctly) underlies the correctness proofs of essentially every later LWE-based encryption scheme.

Formalizing it. The result is proved in the paper and is elementary; it is not open. As far as is known, no machine-checked statement of Regev's scheme as a probability experiment exists on Prove2Me; related platform items concern a different scheme (a dual-Regev variant with deterministic noise bounds over an even modulus). The mission's contribution is a faithful, reusable definition of the cryptosystem as a probability experiment over all of its randomness, together with a proof of its correctness lemma. The definitions (the distance $|\cdot|$ on $\mathbb Z_p$, convolution powers of a distribution on $\mathbb Z_p$, i.i.d. product distributions) are reusable by later missions on the security proof (Claim 5.3, Lemma 5.4) or on other LWE schemes.

Difficulty

The arithmetic is short; the work lies in the probability bookkeeping. The hypothesis controls the law of the noise for each fixed subset size, while the conclusion is about a single experiment in which $S$ is random and independent of the errors, and the keys $s$ and $a_i$ are random too. The step that needs care is identifying the law of $\sum_{i\in S} e_i$ for a fixed $S$ with $\chi^{\star|S|}$ from a product distribution, and then averaging over $S$; the uniform choices of $s$ and $a_i$ must be shown not to affect the residue. A second point is the rounding step: $|\cdot|$ is a cyclic distance on $\mathbb Z_p$, and the strict inequality $|x| < \lfloor p/2\rfloor/2$ is sharp (at $|x| = \lfloor p/2\rfloor/2$ the residue is equidistant and decrypts to $1$), so odd and even $p$ and ties must be handled exactly as printed.

Formalization scope

• $p : \mathbb N$ with [NeZero p] and the hypothesis $2 \le p$ (the paper defines $\mathbb Z_p$ for $p \ge 2$, p. 34:14). Primality, part of the paper's parameter choice, is not assumed: Lemma 5.1 does not use it.
• $\mathbb Z_p$ is ZMod p, vectors are Fin n → ZMod p, $\langle a, s\rangle$ is a ⬝ᵥ s, bits are Fin 2, and subsets of $[m]$ are Finset (Fin m).
• Distributions are PMFs. $\chi^{\star k}$ is defined recursively by binds; the i.i.d. errors use the product PMF with mass $\prod_i \chi(e_i)$; uniform choices are PMF.uniformOfFintype. The experiment outcome n m χ c draws $s$, then $a$, then $e$, then $S$, all independently.
• $|a|$ is computed from the representative a.val; $\lfloor p/2\rfloor$ is natural-number division p / 2; $\lfloor p/2\rfloor/2$ is compared in $\mathbb R$, since it can be a half-integer.
• Decryption ties ($|x| = |x - \lfloor p/2\rfloor|$) decrypt to $1$, as printed ("Otherwise, the decryption is 1").
• Probabilities in the goal are real numbers (toReal of PMF masses, exact because they are at most $1$). The form ENNReal.ofReal (1 − δ) < Pr was rejected: for $\delta \ge 1$ it would add the hypothesis $\Pr > 0$, which the page does not make.
• The goal is not a statement about a fixed key, a fixed subset $S$ or a fixed error vector: the probability is over all of $s$, $a_i$, $e_i$ and $S$, and the hypothesis quantifies over every $k \in \{0, \dots, m\}$. A formalization conditioning on any of these would be a different (weaker) theorem. For $k = 0$ the hypothesis reads $1 > 1 - \delta$, true for $\delta > 0$, so it imposes no hidden restriction.
• No printed slip was found in Lemma 5.1 or its proof.

Contributions welcome: proofs of the three milestones and the goal; general lemmas on convolution powers and product distributions of PMFs on finite groups.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• O. Regev, The Learning with Errors Problem, IEEE Conference on Computational Complexity (invited survey), 2010. https://doi.org/10.1109/CCC.2010.26
• NIST, Module-Lattice-Based Key-Encapsulation Mechanism Standard, FIPS 203, 2024. https://doi.org/10.6028/NIST.FIPS.203

Motivation

Many linear programs that arise in combinatorial optimization have a few "complicating" constraints $Ax \le b$ on top of a set $P$ over which linear optimization is easy: multicommodity flow, where $P$ is a product of single-commodity flow polytopes; scheduling and the Held–Karp bound, where $P$ is a polytope of assignments or trees. Plotkin, Shmoys and Tardos showed that for such problems an approximate solution can be found with a number of calls to the linear optimizer over $P$ that depends on the required accuracy and on a structural quantity, the width, but only logarithmically on the number of constraints. Their packing and covering algorithms (§§2–3 of the paper) assume nonnegative data. Section 4 removes that assumption and treats an arbitrary system of linear inequalities over a convex set. This framework, later known as the multiplicative-weights method for linear programs, is among the standard tools of approximation algorithms (Arora, Hazan and Kale's 2012 survey gives the modern account).

Timeline. Shahrokhi and Matula (1990) gave an exponential-potential algorithm for the maximum concurrent flow problem. Plotkin, Shmoys and Tardos (FOCS 1991; Cornell ORIE Technical Report 999, 1992; Mathematics of Operations Research 1995) generalized it to fractional packing, covering and the general problem of this mission. Grigoriadis and Khachiyan (1994–1996) obtained related bounds for block-angular and convex resource-sharing problems. Garg and Könemann (1998) and Arora, Hazan and Kale (2012) gave width-free or simplified variants.

Setting

An instance of the GENERAL problem consists of an arbitrary real $m\times n$ matrix $A$ with rows $a_1,\dots,a_m$, an arbitrary vector $b\in\mathbb R^m$, a convex set $P\subseteq\mathbb R^n$, and a positive vector $d\in\mathbb R^m$ that sets the scale of the allowed error. The question is whether some $x\in P$ satisfies $Ax\le b$. Such a point is an exact solution; a point $x\in P$ with $Ax\le b+\varepsilon d$ is an $\varepsilon$-approximate solution.

For $x\in P$ write

$$\lambda(x)=\max_{1\le i\le m}\frac{a_ix-b_i}{d_i},$$

the least $\lambda$ with $Ax\le b+\lambda d$; it may be negative. The width is $\rho=\max_i\max_{x\in P}|a_ix-b_i|/d_i$. Access to $P$ is through subroutine (10): given $y\ge 0$ in $\mathbb R^m$, return $\tilde x\in P$ minimizing $y^tAx$ over $P$. For a dual vector $y\ge0$ let $C_{\mathcal G}(y)=\min\{y^t(Ax-b):x\in P\}$. The relaxed optimality conditions for a point $x$ with $\lambda=\lambda(x)$ and a dual vector $y$ are

$$(\mathcal G1)\ \ \lambda\,y^td\le 4\,y^t(Ax-b),\qquad(\mathcal G2)\ \ y^t(Ax-b)-C_{\mathcal G}(y)\le\tfrac{\lambda}{5}\,y^td.$$

The dual solution corresponding to $x$ with parameter $\alpha$ is $y_i=d_i^{-1}e^{\alpha(a_ix-b_i)/d_i}$, and its potential is $\Phi=y^td$. Procedure IMPROVE-GENERAL (Figure 4) starts from $x_0\in P$ with $\lambda_0=\lambda(x_0)$, fixes $\alpha$ and a step size $\sigma$, and, while $\lambda(x)\ge\lambda_0/2$ and $(\mathcal G2)$ fails, replaces $x$ by $(1-\sigma)x+\sigma\tilde x$, where $\tilde x$ is the oracle's answer for the current dual solution. The driver calls IMPROVE-GENERAL repeatedly, stopping with an $\varepsilon$-approximate solution or with a report that none exists.

Formalization targets

Goal: Theorem 4.5

For every $\varepsilon\in(0,1)$, every start $x_0\in P$ and every exact minimizing oracle, the driver stops; an output point is an $\varepsilon$-approximate solution; an infeasibility report is correct ($\nexists x\in P$ with $Ax\le b$); and the number of oracle calls is at most

$$N=2\big(\lfloor\log_2(\rho/\varepsilon)\rfloor+1\big)+11520\,\frac{\rho^2}{\varepsilon^2}\ln\frac{12\,m\,\max(\rho,\varepsilon)}{\varepsilon}=O\!\Big(\rho^2\varepsilon^{-2}\log\frac{m\rho}{\varepsilon}\Big).$$

Milestones

1. Lemma 4.1. If $x\in P$, $y\ge0$, $y\ne0$ satisfy $(\mathcal G1)$ and $(\mathcal G2)$ with $\lambda(x)>0$, no exact solution exists.
2. Lemma 4.2. If $\alpha\ge2\lambda^{-1}\ln(6m\rho\lambda^{-1})$, then $x$ and its dual solution satisfy $(\mathcal G1)$.
3. Lemma 4.3. If $(\mathcal G2)$ fails and $0\le\sigma\le\lambda/(24\alpha\rho^2)$, the step to $(1-\sigma)x+\sigma\tilde x$ lowers the potential: $\Phi-\hat\Phi\ge\alpha\sigma\lambda\Phi/30$.
4. Theorem 4.4. IMPROVE-GENERAL started with $\lambda_0>0$ stops after at most $2+8640\rho^2\lambda_0^{-2}\ln(12m\rho\lambda_0^{-1})$ oracle calls.

Significance

The result gives an $\varepsilon$-relaxed decision procedure for any system of linear inequalities over a convex set with a linear-optimization oracle, with no sign conditions on the data. Its oracle-call count is independent of $n$ and logarithmic in $m$, which is what makes it useful when $m$ is large and $P$ has a fast combinatorial optimizer. The simultaneous packing-and-covering problem is the special case where every row is either nonnegative or nonpositive; the paper's width-reduction techniques (§5) and applications (§6) build on this procedure and on its packing and covering counterparts.

The paper's statements use $O(\cdot)$ and $\Omega(\cdot)$; this mission states the explicit constants that the paper's own proofs give. The result is proved in the literature; no machine-checked proof of it is known on Prove2Me or in Mathlib. It also records a gap in Figure 4 (below) and states the theorem for the smallest correction that makes the paper's proof go through. Formalizing the analysis yields reusable potential-function arguments (second-order bounds on $e^{x+\delta}$, geometric decrease of a potential between two levels) of the kind used throughout multiplicative-weights analyses.

Difficulty

The correctness half is short; the complexity half carries the weight. Lemma 4.3 needs a second-order bound on the exponential that is valid only when the step changes each exponent by at most $1/2$, so the step size must be tied to $\lambda$ and $\rho$. Theorem 4.4 then has to control the potential between a ceiling $me^{\alpha\lambda_0}$ and a floor $e^{\alpha\lambda_0/2}$ while $\lambda$ moves, and Theorem 4.5 has to sum the per-call bounds over a sequence of calls whose $\lambda_0$ halves each time, so that the last call dominates.

The first reading of Figure 4 fails here: Figure 4 fixes $\alpha=4\lambda_0^{-1}\ln(6m\rho\lambda_0^{-1})$ and $\sigma=\lambda_0/(24\alpha\rho^2)$ from $\lambda_0$, but the loop runs for every $\lambda\ge\lambda_0/2$. For $\lambda<\lambda_0$ the hypothesis $\sigma\le\lambda/(24\alpha\rho^2)$ of Lemma 4.3 fails, and the decrease bound from its proof becomes negative for $\lambda<5\lambda_0/6$. At $\lambda=\lambda_0/2$, the hypothesis of Lemma 4.2 requires $\alpha\ge4\lambda_0^{-1}\ln(12m\rho\lambda_0^{-1})$, which the printed $\alpha$ does not meet, so $(\mathcal G1)$ and the infeasibility certificate are not guaranteed. With the printed parameters, the iteration bound is not established by the paper's argument.

Formalization scope

• Representation. Constraints are indexed by Fin m with $m\ge1$ ([NeZero m]), coordinates by Fin n; $A$ is a real matrix and $b$, $d$ real vectors with $d>0$; $P$ is a convex set. No sign hypothesis is put on $A$, $b$ or $P$.
• Width. $\rho>0$ is an upper bound on the width ($|a_ix-b_i|\le\rho d_i$ on $P$), not a supremum; the algorithm uses $\rho$ in its parameters, and the theorems hold for every such bound, the exact width included.
• Oracle. Subroutine (10) is an arbitrary function from dual vectors to points; theorems assume that for every $y\ge0$ it returns a point of $P$ minimizing $y^tAx$ over $P$, and quantify over every such oracle.
• Corrected parameters. IMPROVE-GENERAL uses $\alpha=4\lambda_0^{-1}\ln(12m\rho\lambda_0^{-1})$ and $\sigma=\lambda_0/(48\alpha\rho^2)$, i.e. Figure 4's formulas with $\lambda_0/2$ for $\lambda_0$. Lemmas 4.1–4.3 are stated as printed; they do not mention Figure 4.
• Runs and cost. Procedure and driver are defined with a fuel bound; the theorems assert that the loop test fails before the fuel is exhausted. One oracle call is charged per evaluation of the loop test that reaches $(\mathcal G2)$; the loop body reuses its answer. The driver checks $\lambda(x)\le\varepsilon$ before every call, so no call is made with $\lambda_0\le\varepsilon$, and it reports infeasibility only when a call stopped on its $(\mathcal G2)$ test with $\lambda>\varepsilon$.
• Explicit constants replacing $O(\cdot)$ and $\Omega(\cdot)$. Lemma 4.3: $\Omega(\alpha\sigma\lambda\Phi)$ becomes $\alpha\sigma\lambda\Phi/30$. Theorem 4.4: $O(\rho^2\lambda_0^{-2}\log(m\rho\lambda_0^{-1}))$ becomes $2+8640\rho^2\lambda_0^{-2}\ln(12m\rho\lambda_0^{-1})$ oracle calls. Theorem 4.5: $O(\rho^2\varepsilon^{-2}\log(m\rho\varepsilon^{-1}))$ becomes $N$ above; $\max(\rho,\varepsilon)$ equals $\rho$ whenever a call is made. The "time to compute $Ax$" clause of Theorem 4.5 is not formalized.
• Ruled out. A formalization that assumes termination, takes the oracle's optimality only at the points visited, lets the constant depend on the instance, or allows a call with $\lambda_0\le0$ (where $\ln$ and division return junk values) is not the paper's theorem.
• Needed. Finite sums and maxima over Fin m, second-order bounds on Real.exp and monotonicity of Real.log, convex combinations, induction over fuelled recursions. The potential-decrease lemmas are reusable for the packing and covering missions of the same paper. Proofs of any milestone are welcome independently.

Selected references

• S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Cornell University School of ORIE, Technical Report No. 999, 1992 (§4, pp. 23–27). Journal version: Mathematics of Operations Research 20(2):257–301, 1995. https://doi.org/10.1287/moor.20.2.257
• F. Shahrokhi, D. W. Matula, The maximum concurrent flow problem, Journal of the ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620
• M. D. Grigoriadis, L. G. Khachiyan, Fast approximation schemes for convex programs with many blocks and coupling constraints, SIAM Journal on Optimization 4(1):86–107, 1994. https://doi.org/10.1137/0804004
• N. Garg, J. Könemann, Faster and simpler algorithms for multicommodity flow and other fractional packing problems, SIAM Journal on Computing 37(2):630–652, 2007. https://doi.org/10.1137/S0097539704446232
• S. Arora, E. Hazan, S. Kale, The multiplicative weights update method: a meta-algorithm and applications, Theory of Computing 8:121–164, 2012. https://doi.org/10.4086/toc.2012.v008a006