Theoretical Computer Science

Motivation

The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).

The proof is a reduction from the clique number $\omega(G)$ of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses $\omega(G)$ as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding $\omega(G)\ge l$ is one of Karp's (1972) NP-complete problems.

Setting

A real 3-tensor is an array $\mathcal A=[\![a_{ijk}]\!]\in\mathbb R^{l\times m\times n}$ with trilinear form $\mathcal A(\mathbf x,\mathbf y,\mathbf z)=\sum_{i,j,k}a_{ijk}x_iy_jz_k$. With the Euclidean norm $\|\cdot\|_2$, its spectral norm is

$$\|\mathcal A\|_{2,2,2}=\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal A(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}.$$

A real $\sigma$ is a unit $\ell^2$-singular value of $\mathcal A$ if there are unit vectors $\mathbf u,\mathbf v,\mathbf w$ with

$$\textstyle\sum_{j,k}a_{ijk}v_jw_k=\sigma u_i,\quad \sum_{i,k}a_{ijk}u_iw_k=\sigma v_j,\quad \sum_{i,j}a_{ijk}u_iv_j=\sigma w_k$$

for all $i,j,k$: the stationarity conditions of $\mathcal A(\mathbf u,\mathbf v,\mathbf w)$ on a product of unit spheres.

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$, with $e$ edges $\{i_k,j_k\}$, $k=1,\dots,e$, and clique number $\omega$. Let $\Delta_v$ be the standard simplex, $A_G$ the adjacency matrix and $J$ the all-ones matrix. For a positive integer $l$ set $Q_l=A_G+\frac1lJ$ and $M_l=\max_{\mathbf x\in\Delta_v}\mathbf x^\top Q_l\mathbf x$. Let $E_k=\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$, and let $T_l$ be the maximum over unit $\mathbf u,\mathbf v\in\mathbb R^v$, $\mathbf w\in\mathbb R^{l+2e}$ of the multilinear form

$$\sum_{i=1}^l\Big(\mathbf u^\top\tfrac1lI\mathbf v\Big)w_i+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{l+k}+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{e+l+k}. \tag{26}$$

The graph tensor $\mathcal A_l\in\mathbb Q^{v\times v\times(l+2e)}$ has as entry $a_{ijk}$ the coefficient of $u_iv_jw_k$ in (26).

Formalization targets

Goal: Theorems 6.5 and 1.10, encoding-free core

For every graph $G$ on $v\ge1$ vertices and every enumeration of its edges:

$$\forall l\ge1:\ \|\mathcal A_l\|_{2,2,2}=1\iff l=\omega;\qquad 1\text{ is a unit singular value of }\mathcal A_\omega;\qquad \forall l>\omega:\ 1\text{ is not one of }\mathcal A_l,$$

so $\omega$ is the largest $l\in\{1,\dots,v\}$ for which $1$ is a unit singular value of $\mathcal A_l$. The paper's $v$-query Turing reductions rest on exactly this.

Milestones (in attack order)

1. Theorem 6.7 (Motzkin–Straus): $1-1/\omega=2\max_{\mathbf x\in\Delta_v}\sum_{\{i,j\}\in E}x_ix_j$.
2. (22): $M_l=1+\frac{\omega-l}{l\omega}$; so $M_\omega=1$, $M_l>1$ for $l<\omega$, $M_l<1$ for $l>\omega$.
3. Lemma 6.8: $M_l=N_l$, where $N_l=\max_{\|\mathbf u\|_2=1}\{\sum_{i=1}^l(\mathbf u^\top\frac1lI\mathbf u)^2+2\sum_k(\mathbf u^\top E_k\mathbf u)^2\}$.
4. Theorem 6.9 (Banach), (24): for a symmetric 4-tensor, $\|\mathcal S\|_{2,2,2,2}=\sup_{\mathbf x\neq\mathbf 0}|\mathcal S(\mathbf x,\mathbf x,\mathbf x,\mathbf x)|/\|\mathbf x\|_2^4$.
5. Proposition 6.10 (He–Li–Zhang): for symmetric $A_k$, $\max_{\|\mathbf u\|=\|\mathbf v\|=1}\sum_k(\mathbf u^\top A_k\mathbf v)^2=\max_{\|\mathbf v\|=1}\sum_k(\mathbf v^\top A_k\mathbf v)^2$.
6. Lemma 6.11: $T_l=M_l^{1/2}$, hence $T_l=1$ iff $l=\omega$, $T_l>1$ iff $l<\omega$, $T_l<1$ iff $l>\omega$.
7. Proof of Theorem 6.5: $\|\mathcal A_l\|_{2,2,2}=T_l$, $T_l$ is a unit singular value of $\mathcal A_l$, and every unit singular value has absolute value at most $T_l$.
8. §7 (content of Theorem 1.13): $\min_{\sigma\ge0,\ \text{unit }\mathbf u,\mathbf v,\mathbf w}\|\mathcal A-\sigma\,\mathbf u\otimes\mathbf v\otimes\mathbf w\|_F^2=\|\mathcal A\|_F^2-\|\mathcal A\|_{2,2,2}^2$, attained only with $\sigma=\|\mathcal A\|_{2,2,2}$.

Significance

The result. The goal shows that a single comparison with $1$ of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size $v\times v\times(l+2e)$ encodes whether $l=\omega(G)$. It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.

Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.

Difficulty

The construction of $\mathcal A_l$ is explicit, and the comparison with $1$ is arithmetic once $T_l=M_l^{1/2}$ is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.

Formalization scope

Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with $v\ge1$, clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. $\mathcal A_l$ is a rational tensor, read over $\mathbb R$ by casting.

Explicit readings of the paper:

• Definition 6.1 has no norm constraint. Since $(\sigma,\mathbf u,\mathbf v,\mathbf w)\mapsto(t\sigma,t\mathbf u,t\mathbf v,t\mathbf w)$ preserves (20), unnormalized singular values make every nonzero real a singular value of $\mathcal A_l$, so the clause "not for $l>\omega$" would be false. Singular vectors are therefore unit vectors, as in the paper's derivation on p. 0:21.
• The statement of Lemma 6.11 prints $w_{m+l+k}$. There is no $m$ in §6, and the proof uses $w_{e+l+k}$, which is formalized.
• $E_k$ is written entrywise as $\frac12[\{i,j\}=\{i_k,j_k\}]$, which equals $\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$ for a loopless edge.
• "$T_l$ is just the maximum $\ell^2$-singular value of $\mathcal A_l$" is made explicit as milestone 7.
• The goal does not claim that $1$ fails to be a singular value of $\mathcal A_l$ for $l<\omega$; the paper neither claims nor uses this.

This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of $\mathcal A_l$, the $v$-query procedure, the scaling to a general fixed $0\ne\sigma\in\mathbb Q$, and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.

Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.

Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (final version arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393v5)
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian J. Math. 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in (L²), Studia Math. 7, 36–44, 1938. https://doi.org/10.4064/sm-7-1-36-44
• S. He, Z. Li, S. Zhang, Approximation algorithms for homogeneous polynomial optimization with quadratic constraints, Math. Program. Ser. B 125(2), 353–383, 2010. https://doi.org/10.1007/s10107-010-0409-z
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

A snark is an uncolourable, cyclically 4-edge-connected cubic graph of girth at least 5: a cubic graph whose edges cannot be properly coloured with three colours, and which is not reducible to a smaller such graph by an elementary operation. Snarks are the critical cases for several of the central conjectures of graph theory, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture: a minimal counterexample to any of them, if one exists, is a snark. Lists of all small snarks are therefore used to test such conjectures by computer.

Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, 2013) generated all snarks on up to 36 vertices. Testing 3-edge-colourability is NP-complete, and only a vanishing fraction of cubic graphs are snarks (0.00044% of the cubic graphs of girth at least 5 on 28 vertices, p. 4), so the generation algorithm needs cheap criteria that recognise, before a graph is built, that it will be colourable and can be skipped. Section 3.1 of the paper supplies such a criterion for the last construction step, and this mission formalizes it.

Setting

All graphs are finite and simple. A graph is cubic if every vertex has degree 3. A 3-colouring of a graph $G=(V,E)$ is a map $C:E\to\{0,1,2\}$ that gives different colours to any two distinct edges sharing an end-vertex; $G$ is colourable if it has one, i.e. its chromatic index satisfies $\chi'(G)\le 3$ (p. 2, Isaacs' terminology).

A 2-factor of $G$ is a spanning 2-regular subgraph $F$ (p. 4); each connected component of $F$ is a cycle. $F$ is an even 2-factor if all its cycles have even length (p. 5). For a 3-colouring $C$ and colours $i\ne j$, write $G_{ij}$ for the spanning subgraph whose edges are those coloured $i$ or $j$.

The edge insertion operation (Figure 1(d), p. 5) takes two distinct edges $e=ab$ and $e'=cd$ of $G$, which may share an end-vertex, subdivides $e$ by a new vertex $x$ and $e'$ by a new vertex $y$, and adds the edge $xy$. The resulting graph $G'$ has vertex set $V\cup\{x,y\}$ and edge set

$$E(G')=\bigl(E\setminus\{e,e'\}\bigr)\cup\{ax,xb,cy,yd,xy\}.$$

If $G$ is cubic, so is $G'$. In the generation algorithm every graph of girth at least 4 is produced from a graph with two fewer vertices by this operation.

Formalization targets

Goal: Theorem 3.3 (p. 5)

Let $G$ be a cubic graph with a 3-colouring $C$, let $i\ne j$ be colours, and let $e=ab$, $e'=cd$ be distinct edges of $G_{ij}$ lying on the same cycle of $G_{ij}$. Then

$$\chi'(G')\le 3,\qquad G' = G \text{ with an edge inserted between } e \text{ and } e'.$$

Milestones

1. Lemma 3.1 (p. 5). For a cubic graph $G$,

$$\chi'(G)\le 3 \iff G \text{ has an even 2-factor.}$$

2. The two-colour observation (§3.1, p. 5). If $G$ is cubic, $C$ is a 3-colouring and $i\ne j$, then $G_{ij}$ is an even 2-factor of $G$.
3. Lemma 3.2 (p. 5). If $F$ is an even 2-factor of a cubic graph $G$ and $e\ne e'$ are edges of $F$ on the same cycle of $F$, then the graph obtained by inserting an edge between $e$ and $e'$ is colourable.

Supporting statement (not on the goal's path)

Theorem 3.4 (p. 6, stated as folklore without proof). If $G$ is a colourable cubic graph and the inserted edge $xy$ lies on a 4-cycle of $G'$, then $G'$ is colourable.

Significance

The result. Theorem 3.3 is the look-ahead of the snark generator: one 3-colouring of a graph on $n-2$ vertices excludes, at once, every pair of edges lying on a common cycle of one of its three bicoloured 2-factors. For 28 vertices the first colouring alone discards on average 85% of the candidate edge pairs (p. 6), and the overall ratio of weak snarks among generated graphs on the last level improves by a factor of 85 (p. 4). The enumeration of all snarks up to 36 vertices, on which the paper's counterexamples and statistics rest, depends on this pruning being sound: a wrong pruning rule would silently delete snarks from the lists. Theorem 3.4 is a second pruning rule of the same kind.

Formalizing it. The results are proved (Lemma 3.1 is classical; the paper gives the argument for Lemma 3.2 in one sentence and for Theorem 3.3 by combination). None of them, and no statement about 3-edge-colourings of cubic graphs and their 2-factors, is formalized on the platform. The mission produces a machine-checked soundness proof of the pruning criterion and, along the way, a reusable development of the equivalence between 3-edge-colourings and even 2-factors in Lean's SimpleGraph library. Theorem 3.4 has no proof in the paper.

Difficulty

The combinatorial content is short; the difficulty lies in graph-theoretic infrastructure that Mathlib does not have. Lemma 3.1 relates a global object (a proper colouring of all edges) to the cycle structure of a spanning 2-regular subgraph, and either direction needs the description of a finite 2-regular graph as a disjoint union of cycles together with parity information along each cycle. Mathlib has walks, cycles and connected components, but no decomposition of a 2-regular graph into cycles and no notion of the length of a component as a cycle.

Lemma 3.2 and Theorem 3.3 change the vertex type: $G'$ lives on $V\sqcup\{x,y\}$, so 2-factors, connected components and cycle lengths must be transported from $G$ to $G'$, and the case where $e$ and $e'$ share an end-vertex (allowed by Figure 1(d)) has to be handled alongside the generic one. A first idea, to extend a given 3-colouring of $G$ directly to $G'$, does not work in general: the colours forced on the edges at $x$ and $y$ by the old colours of $e$ and $e'$ can conflict, and the hypothesis "same cycle" is what has to be used to avoid the conflict.

Formalization scope

Vertices form a type V with [Fintype V] [DecidableEq V]; graphs are SimpleGraph V with decidable adjacency, and "cubic" is Mathlib's G.IsRegularOfDegree 3. Colourability is G.lineGraph.Colorable 3 (an edge colouring, not a vertex colouring), and a 3-colouring is G.lineGraph.Coloring (Fin 3). A 2-factor is a graph F on the same vertex type with F ≤ G and F.IsRegularOfDegree 2; it is even if every connected component has an even number of vertices (Nat.card). The edge insertion operation produces a graph on V ⊕ Fin 2, with Sum.inr 0 subdividing $e$ and Sum.inr 1 subdividing $e'$; edges are unordered pairs Sym2 V. "On the same cycle" is encoded as membership of both edges in the 2-factor plus reachability of their end-vertices inside the 2-factor. Oddness is not defined as a number; Lemma 3.1 is stated in its second form.

Dropping "on the same cycle" would make Theorem 3.3 and Lemma 3.2 false (inserting edges between different cycles of a bicoloured 2-factor is exactly how snarks are produced), and both statements require the two edges to be distinct; a formalization without either hypothesis is ruled out. Every statement assumes cubicity, without which Lemma 3.1 fails.

Out of scope: the algorithmic content of §3 (isomorphism rejection, the look-ahead implementation, recolouring along non-hamiltonian cycles, the 85% / 11% / 3.4% statistics), the generation counts, and every exhaustive-search claim of the paper. The remaining results of the paper are covered by three sibling missions of this series.

Reusable beyond this mission: the 2-factor and even-2-factor definitions, the two-colour 2-factor of an edge colouring, and Lemma 3.1 itself. Contributions welcome: the cycle decomposition of finite 2-regular graphs, alternating colourings of even cycles, and a proof of Theorem 3.4.

Selected references

• G. Brinkmann, J. Goedgebeur, J. Hägglund, K. Markström, Generation and properties of snarks, J. Combin. Theory Ser. B 103 (2013); arXiv:1206.6690v3. https://arxiv.org/abs/1206.6690
• R. Isaacs, Infinite families of nontrivial trivalent graphs which are not Tait colorable, Amer. Math. Monthly 82 (1975) 221–239. https://doi.org/10.2307/2319844

Motivation

A data curator holds a database of $n$ individual records and wants to publish something from which many statistics can be computed, while guaranteeing differential privacy: no single record should noticeably change what is published (Dwork, McSherry, Nissim, Smith 2006). Interactive mechanisms answer queries one at a time and add noise to each answer, so their accuracy degrades as more queries are asked; Dinur and Nissim showed that answering too many arbitrary queries accurately reveals the database (Dinur, Nissim 2003).

Blum, Ligett and Roth asked a different question: can a curator release, once and non-interactively, a synthetic database that is accurate simultaneously for every query of a large, structured class, while remaining differentially private? Their answer (arXiv:1109.2229; JACM 60(2), 2013; conference version STOC 2008) is yes for every class of counting queries over a discretized universe, with accuracy governed by the class's VC-dimension rather than its cardinality. The mechanism it introduces, the Net mechanism, became the starting point of the literature on private query release (SmallDB, private multiplicative weights, and the lower bounds that followed).

Setting

Fix a finite data universe $X$ (for instance $X=\{0,1\}^k$). The curator's input is an $n$-tuple $z=(z_1,\dots,z_n)\in X^n$, read as a multiset of records. Two inputs are neighbouring if they differ in exactly one entry.

A database of arbitrary size $D\in X^*$ is a finite nonempty multiset of elements of $X$. For a predicate $\varphi:X\to\{0,1\}$ the counting query is

$$Q_\varphi(D)=\frac{1}{|D|}\sum_{x\in D}\varphi(x),$$

the fraction of records satisfying $\varphi$. A class $C$ of predicates is identified with its class of counting queries, and its VC-dimension $\mathrm{VCDIM}(C)$ is the size of the largest set of points that $C$ shatters.

A randomized mechanism $A$, whose output on input $z$ is a random database $\hat D\in X^*$, is $\varepsilon$-differentially private if $\Pr[A(z)\in S]\le e^{\varepsilon}\Pr[A(z')\in S]$ for all neighbouring $z,z'$ and all sets $S$ of outputs. It is $(\alpha,\delta)$-useful for $C$ if for every input $z$, with probability at least $1-\delta$, $|Q_\varphi(\hat D)-Q_\varphi(z)|\le\alpha$ for every $\varphi\in C$.

The global sensitivity of $f:X^n\to\mathbb R$ is $GS_f=\max|f(z)-f(z')|$ over neighbouring pairs. An $\alpha$-net for $C$ is a finite set $N\subseteq X^*$ such that every $D\in X^*$ has some $D'\in N$ with $|Q_\varphi(D)-Q_\varphi(D')|\le\alpha$ for all $\varphi\in C$; $N_\alpha(C)$ denotes a net of minimum size.

The exponential mechanism with quality score $q:X^n\times R\to\mathbb R$ over a finite range $R$ outputs $r$ with probability proportional to $\exp(\varepsilon q(z,r)/(2GS_q))$. The Net mechanism is the exponential mechanism over $R=N_\alpha(C)$ with score $q(z,D')=-\max_{\varphi\in C}|Q_\varphi(z)-Q_\varphi(D')|$.

Formalization targets

Goal: Theorem 3.10

There is an absolute constant $c>0$ such that, for every finite $X$, $d=\mathrm{VCDIM}(C)\ge1$, $n\ge1$, $\varepsilon>0$, $0<\delta\le1$, $0<\alpha\le\tfrac12$, whenever

$$\alpha\ \ge\ \frac{c}{\varepsilon\alpha^2 n}\Big(d\log|X|\log\frac1\alpha+\log\frac1\delta\Big),$$

a minimum $\tfrac\alpha2$-net exists and the Net mechanism run on any minimum $\tfrac\alpha2$-net is $(\alpha,\delta)$-useful for $C$. The constant is left unspecified, as in the paper; the goal asserts the shape of the bound, not a value of $c$.

Milestones

1. Observation 2.4: $GS_{Q_\varphi}\le 1/n$.
2. Theorem 3.2 and Property 3.3: the exponential mechanism, hence the Net mechanism, is $\varepsilon$-differentially private.
3. Property 3.4: for any query class with sensitivities at most $\Delta$, the Net mechanism is $(2\alpha,\delta)$-useful once $\alpha\ge\frac{2\Delta}{\varepsilon}\log\frac{|N_\alpha(C)|}{\delta}$.
4. Corollary 3.5: for counting queries, $(2\alpha,\delta)$-useful once $\alpha\ge\frac{2}{\varepsilon n}\log\frac{|N_\alpha(C)|}{\delta}$.
5. Lemma 3.7 and Theorem 3.6 (finite classes): $|N_\alpha(C)|\le|X|^{\lceil\log|C|/\alpha^2\rceil}$.
6. Lemma 3.8 and Theorem 3.9 (finite VC-dimension): $|N_\alpha(C)|\le|X|^{c_0\,d\log(1/\alpha)/\alpha^2}$.

Significance

The result. Theorem 3.10 shows that a database of size roughly $\tilde O(\mathrm{VCDIM}(C)\log|X|/(\alpha^3\varepsilon))$ suffices to release, privately, a synthetic database answering every query of $C$ to within $\alpha$. This is only a polynomial factor above what sampling needs without privacy, and it covers classes with exponentially many queries in $n$, which interactive noise addition cannot. Together with Property 3.3 it is the first general feasibility result for non-interactive private release, and it identified VC-dimension as the governing parameter.

Formalizing it. The result is proved in the paper, modulo the cited uniform-convergence lemma (Lemma 3.8). No part of it is machine-checked on the platform. A complete development would give a formal exponential mechanism with a general score and its privacy proof, a formal utility analysis of a mechanism with a finite range, and a formal ε-approximation theorem for VC classes, which is the deepest dependency and reusable across learning theory.

Difficulty

The privacy and utility of the exponential mechanism (Theorem 3.2, Property 3.4) are short ratio arguments. The difficulty is concentrated in bounding the size of the net. For finite classes a random-sampling and union-bound argument suffices (Lemma 3.7). For infinite classes the union bound over $C$ is unavailable, and Lemma 3.8 needs uniform convergence over a class of finite VC-dimension, uniformly over every finite multiset $D$: a symmetrization or chaining argument together with the Sauer–Shelah lemma, none of which is in Mathlib in this form. The obvious route of applying the finite-class bound to the restriction of $C$ to the support of $D$ gives a size depending on $|D|$ and fails.

Formalization scope

• Inputs are Fin n → X with X : Type finite; neighbouring means "replace one entry", the platform's PrivLearn.Generic.Neighbors. The paper's "$|D\Delta D'|\le1$" read literally for equal-size multisets forces $D=D'$ and would make every mechanism private.
• Databases of arbitrary size are nonempty multisets (Database X), with every set measurable. Queries are real functions on multisets, so the same query reads inputs and outputs. Predicates are X → Bool; VC-dimension is the platform's HighDimProb.Chaining.vcDim (valued in ℕ∞; the theorems take it finite, equal to $d\ge1$).
• Usefulness and α-nets use "for all $Q\in C$", not a real supremum. $N_\alpha(C)$ is never an infimum of cardinalities: statements quantify over minimum nets and assert that one exists.
• The exponential mechanism is a finite mixture of point masses. Where the paper divides by $GS_q$, Theorem 3.2 and Properties 3.3–3.4 assume $GS_q>0$; Corollary 3.5 and Theorem 3.10 need no such hypothesis, because for counting queries $GS_q=0$ forces a regime in which every output is accurate.
• $O(\cdot)$ instantiations. Lemma 3.8: $|D'|\le c_0\,d\log(1/\alpha)/\alpha^2$. Theorem 3.9: $|N_\alpha(C)|\le|X|^{c_0 d\log(1/\alpha)/\alpha^2}$ (real power). Theorem 3.10: the condition $\alpha\ge\frac{c}{\varepsilon\alpha^2n}(d\log|X|\log\frac1\alpha+\log\frac1\delta)$. Each constant is absolute and quantified before the universe and the class. Theorem 3.10's $(\alpha,\delta)$ is Corollary 3.5's $(2\alpha',\delta)$ at $\alpha'=\alpha/2$, so the mechanism runs on a minimum $\alpha/2$-net. Lemma 3.7 and Theorem 3.6 round $\log|C|/\alpha^2$ up and assume $|C|\ge3$, as the paper's proof does.
• Excluded corners, disclosed in each statement: $d=0$, $\alpha>\tfrac12$. Logarithms are natural. The "solving for α" display $\tilde O(\cdot)^{1/3}$ of Theorem 3.10 is out of scope.
• A trivializing formalization is ruled out: usefulness is required of the Net mechanism as defined, whose output law is a genuine probability distribution over a nonempty net of nonempty databases (Property 3.3 records this), not of a zero measure, an empty net, or a net containing the empty database.

Welcome contributions: a general ε-approximation theorem for VC classes (Lemma 3.8), reusable well beyond this mission; a reusable exponential-mechanism privacy proof; the finite-range utility analysis of Property 3.4.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1, 2011; J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229
• F. McSherry, K. Talwar, Mechanism Design via Differential Privacy, FOCS 2007. https://doi.org/10.1109/FOCS.2007.66
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• I. Dinur, K. Nissim, Revealing Information while Preserving Privacy, PODS 2003. https://doi.org/10.1145/773153.773173
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. https://doi.org/10.1017/CBO9780511624216
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.
• Y. Li, P. M. Long, A. Srinivasan, Improved Bounds on the Sample Complexity of Learning, J. Comput. Syst. Sci. 62(3), 2001. https://doi.org/10.1006/jcss.2000.1741

Motivation

Differential privacy (Dwork, McSherry, Nissim, Smith 2006) asks that a randomized algorithm run on a database behave almost identically whether or not any single record is changed. A central question for data curators is non-interactive release: publish, once, a sanitized object (ideally a synthetic database) from which analysts can answer many statistical queries accurately. Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that over a discrete data universe this is possible for every class of counting queries of bounded VC-dimension, with accuracy governed by the VC-dimension and the logarithm of the universe size.

That dependence on the universe size raises an obvious question: can the discretization be removed? For real-valued data the class of interval queries ("what fraction of the records lies in $[a,b]$?") has VC-dimension 2, so a learning-theoretic intuition suggests that releasing a database accurate for all intervals should be easy. Section 5 of the paper shows that it is impossible under differential privacy. This mission formalizes that impossibility.

The phenomenon was later quantified: Bun, Nissim, Stemmer and Vadhan (FOCS 2015) showed that for approximate differential privacy, releasing threshold queries over a finite ordered domain of size $N$ requires sample size growing with $\log^* N$, so that the infinite case is impossible for approximate privacy as well. The present result is the pure-privacy statement for the real line.

Setting

A real-valued database of size $n \ge 1$ is a tuple $z = (z_1,\dots,z_n) \in \mathbb R^n$. Two databases are neighbours if they differ in exactly one coordinate. A mechanism maps each database $z$ to a probability distribution $A(z)$ on a measurable output space $O$. It is $\varepsilon$-differentially private if for all neighbours $z, z'$ and all measurable $S \subseteq O$,

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

For real $a \le b$ the interval query is $Q_{[a,b]}(z) = \#\{i : a \le z_i \le b\}/n$. A mechanism with a readout $\mathrm{ans}(o,a,b)$ (the answer that output $o$ gives to $Q_{[a,b]}$; for synthetic data $\hat D$, $\mathrm{ans}(\hat D,a,b) = Q_{[a,b]}(\hat D)$) is $(\alpha,\delta)$-useful for interval queries if for every database $z$,

$$\Pr_{o\sim A(z)}\big[\forall a \le b:\ |\mathrm{ans}(o,a,b) - Q_{[a,b]}(z)| \le \alpha\big] \ge 1-\delta .$$

A real number $r$ is a $\theta$-percentile point of $z$ (the paper's "$50-\delta, 50+\delta$ percentile" with $\theta = \delta/100$) if at least $(1/2-\theta)n$ entries satisfy $z_i \le r$ and at least $(1/2-\theta)n$ entries satisfy $z_i \ge r$. A mechanism with real outputs answers median queries usefully with positive probability if on every database its output is a $\theta$-percentile point with positive probability.

In Lean, databases are Fin n → ℝ; neighbours and differential privacy are the published PrivLearn.Generic.Neighbors and PrivLearn.Generic.IsDP; the new objects are intervalQuery, IsPercentile, AnswersMedianUsefully and UsefulIntervals in PrivateRelease.Continuous.

Formalization targets

Goal: Corollary 5.2 (p. 15)

For every $n \ge 1$, $\varepsilon \ge 0$ and $\alpha, \delta < 1/2$, no $\varepsilon$-differentially private mechanism with a measurable readout is $(\alpha,\delta)$-useful for interval queries on $\mathbb R^n$:

$$\mathrm{IsDP}(A,\varepsilon) \;\Longrightarrow\; \neg\,\mathrm{UsefulIntervals}(A,\mathrm{ans},\alpha,\delta).$$

No constant is hard-coded; the thresholds $1/2$ are the paper's.

Milestone: Theorem 5.1 (p. 14)

For every $n \ge 1$, $0 \le \theta < 1/2$ and real $\varepsilon$, no $\varepsilon$-differentially private mechanism $A : \mathbb R^n \to \mathcal P(\mathbb R)$ answers median queries usefully with positive probability on every database:

$$\mathrm{IsDP}(A,\varepsilon) \;\Longrightarrow\; \exists z,\ \Pr_{r\sim A(z)}[r \text{ is a } \theta\text{-percentile point of } z] = 0 .$$

Significance

The result. Corollary 5.2 is the reason the paper's general release mechanism needs a discretized data universe and why its halfspace mechanism (§6) relaxes usefulness to large-margin queries. More broadly it separates private release from non-private learning: the class of intervals is learnable from $O(1/\alpha^2)$ samples without privacy, yet no pure-private mechanism can release it at all over $\mathbb R$. It anticipates the line of work on private learning of thresholds and the role of the domain size in private query release.

Formalizing it. Both statements are proved in the paper; neither is, to our knowledge, machine-checked. A formal proof needs the countability of the atoms of a finite measure on $\mathbb R$, the stability of differential privacy under measurable post-processing, and a measurable selection of a percentile point from approximate interval answers. These pieces (especially post-processing for general measurable outputs) are reusable across formalized differential privacy.

Difficulty

The obvious argument for Theorem 5.1, a direct comparison of two neighbouring databases, gives nothing: changing one record moves the percentile set only slightly, and differential privacy allows each probability to change by a factor $e^{\varepsilon}$, so no single pair of neighbours yields a contradiction. A naive appeal to "the median reveals a record" also fails, since the statement must exclude even mechanisms that are correct with tiny positive probability.

For Corollary 5.2 the difficulty is measure-theoretic: the usefulness event intersects uncountably many conditions, the release must be converted into a single real output measurably, and the converted output must be a percentile point on the useful event for every real database, not only those in $[0,1]$.

Formalization scope

Conventions committed to in Lean:

• Databases are ordered tuples Fin n → ℝ with $n \ge 1$; the paper's neighbour relation "$|D\Delta D'| \le 1$" is read as replace-one-entry.
• Mechanisms are families of probability measures (IsProbabilityMeasure (A z) is a hypothesis). Theorem 5.1's outputs live in $\mathbb R$ with its Borel σ-algebra.
• Interval queries use closed intervals $[a,b]$ with $a \le b$, as in the paper's indicator $I_{a_1,a_2}$ (p. 12).
• Usefulness is required on every database in $\mathbb R^n$ (Definition 2.10 with $X = \mathbb R$). The usefulness event need not be measurable; its probability is the outer measure.
• The goal is stated for an arbitrary measurable output space with a readout $\mathrm{ans}$ measurable in the output for each fixed query. Synthetic data is a special case, so the formal goal is at least as strong as the paper's. The readout's measurability is necessary for the statement to be true with outer measures.
• The percentile set counts entries equal to $r$ on both sides. A one-sided reading ($\#\{z_i \le r\}/n \in [1/2-\theta, 1/2+\theta]$) makes the set empty for constant databases, so that Theorem 5.1 would hold vacuously; the chosen definition always contains a sample median and equals $\{c\}$ on a constant database $(c,\dots,c)$ (both facts were checked locally in Lean).
• Trivializing readings are ruled out: the percentile set is never empty, the mechanism is a probability measure (the zero measure is differentially private), and $n = 0$ (no neighbours, $Q = 0/0 = 0$ in Lean) is excluded.
• There is no O(·)/Ω(·) in this section, so no constant was instantiated.
• Not formalized: the clause of Corollary 5.2 "nor for any class $C$ that generalizes interval queries to higher dimensions (for example, halfspaces, axis-aligned rectangles, or spheres)", because the paper does not define "generalizes".

Contributions welcome: a proof of Theorem 5.1; a general post-processing lemma for IsDP; the reduction from interval usefulness to median answers.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1, 2011; J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229, https://doi.org/10.1145/2450142.2450148
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• M. Bun, K. Nissim, U. Stemmer, S. Vadhan, Differentially Private Release and Learning of Threshold Functions, FOCS 2015. https://arxiv.org/abs/1504.07553

Motivation

Differential privacy (Dwork, McSherry, Nissim and Smith 2006) is the standard guarantee for releasing statistics about a sensitive database: replacing one record changes the probability of any outcome by at most a factor $e^{\varepsilon}$. In their paper on non-interactive database privacy, Blum, Ligett and Roth propose an alternative motivated by learning theory, distributional privacy. When a database is a sample from a population, a release should reveal no more about the sample than is inherent in the population itself. Their example is a group of hospitals, each treating a random sample of the patients with a disease in a region: a hospital can publish information that describes the regional population without revealing which hospital's patients produced it.

The two notions look incomparable at first. Differential privacy protects only databases that differ in one record, but protects every such pair; distributional privacy can protect databases that differ in all their records, but only for typical pairs, and it tolerates a small failure probability $\beta$. §7 of the paper (p. 19) shows that distributional privacy is the stronger notion once $\beta$ is small compared with $1/n^2$. This mission formalizes that implication, Theorem 7.3.

Setting

Fix a data universe $X$ and a measurable space $R$ of outputs. In §7 a database of size $n$ is a set $D\subseteq X$ with $|D|=n$; databases are drawn without replacement, so they have no repeated elements. A mechanism $A$ assigns to each database $D$ of size $n$ the probability law $A(D)$ of its random output, a measure on $R$, and $\Pr[A(D)\in E]$ denotes $A(D)(E)$.

• Two databases $D,D'$ of size $n$ are neighbours if $D'$ is obtained from $D$ by replacing one element: $|D\setminus D'|=1$.
• $A$ is $\varepsilon$-differentially private (Definition 2.1, p. 5) if $\Pr[A(D)\in E]\le e^{\varepsilon}\Pr[A(D')\in E]$ for all neighbours $D,D'$ and all measurable events $E\subseteq R$.
• For a finite population $S\subseteq X$ with $|S|\ge n$, two $S$-neighbours $D_1,D_2$ (Definition 7.1) are drawn independently, each uniformly among the $n$-element subsets of $S$.
• A pair $(D_1,D_2)$ is good if $\Pr[A(D_1)\in E]\le e^{\varepsilon}\Pr[A(D_2)\in E]$ for all measurable $E$ simultaneously.
• $A$ is $(\varepsilon,\beta)$-distributionally private (Definition 7.2) if, for every such $S$, the $S$-neighbours form a good pair with probability at least $1-\beta$; equivalently, at most $\beta\binom{|S|}{n}^2$ ordered pairs of $n$-subsets of $S$ are bad.

The Lean development uses the same names: SetNeighbors, IsDPSet, GoodPair, badPairCount and IsDistPrivate in the namespace PrivateRelease.Distributional.

Formalization targets

Goal: Theorem 7.3

For a family of mechanisms $(A_n)_n$, one per database size, and failure probabilities $\beta_n=o(1/n^2)$:

$$n^2\beta_n\to0\ \text{ and }\ A_n\text{ is }(\varepsilon,\beta_n)\text{-distributionally private for all }n\ \Longrightarrow\ A_n\text{ is }\varepsilon\text{-differentially private for all sufficiently large }n.$$

The goal keeps the paper's asymptotic hypothesis and leaves the rate of $\beta_n$ unfixed beyond $o(1/n^2)$.

Milestone: the fixed-size statement

For a single size $n$, the threshold the paper's argument actually uses:

$$\beta<\frac{1}{(n+1)^2}\ \text{ and }\ A\text{ is }(\varepsilon,\beta)\text{-distributionally private}\ \Longrightarrow\ A\text{ is }\varepsilon\text{-differentially private on databases of size }n.$$

The goal follows from it, since $n^2\beta_n\to0$ forces $\beta_n<1/(n+1)^2$ eventually.

Significance

The result. Theorem 7.3 places distributional privacy above differential privacy: a mechanism designed for the distributional guarantee automatically inherits every consequence of differential privacy, including its composition properties and its robustness to auxiliary information about individuals. The paper complements it with a separation (Theorem 7.5), so the inclusion is strict. A footnote extends the conclusion to $t\varepsilon$-privacy for databases that differ in $t$ elements.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The value of the formalization lies in fixing the definitions. Definition 7.2 is informal about the sampling model ("drawn at random without replacement"), about whether the guarantee holds for all events at once or event by event, and about what $\beta=o(1/n^2)$ means for a mechanism defined on one database size. The proof's count "with probability $2/n^2$" is also loose: the exact probability of a given unordered pair is $2/(n+1)^2$. The mission records one precise reading of each and the theorem under it, and the definitions are reusable for further work on distributional privacy and on the paper's separation result.

Difficulty

The mathematics is short; the difficulty is in the encoding. The step that fails under a careless reading is the passage from "with probability $1-\beta$" to "with certainty": it requires the population $S$ to be finite and small (the proof takes $|S|=n+1$), so that a single pair has probability bounded below. If the guarantee is read event by event (for each $E$, most pairs satisfy the inequality for that $E$), the counting argument still applies to each event separately, but the definition is weaker than the paper's. If databases are allowed to repeat elements, the theorem is false, because distributional privacy never examines a database with repetitions while differential privacy does.

Formalization scope

• Databases are Finset X of cardinality $n$; a mechanism is A : Finset X → Measure R, and only its values on $n$-element sets matter. [DecidableEq X] is assumed for set difference.
• Neighbours replace one element ((D \ D').card = 1). The paper's literal "$|D\Delta D'|\le1$" holds for equal-size sets only when $D=D'$; the replace-one reading is the intended one.
• Events are measurable subsets of $R$; with the σ-algebra $\top$ on $R$ these are all sets.
• Only finite populations $S$ are quantified. This weakens the hypothesis of Theorem 7.3 and so makes the theorem stronger. The two draws are independent, and pairs are counted as ordered pairs.
• The asymptotic hypothesis is Tendsto (fun n => n^2 * β n) atTop (𝓝 0) and the conclusion is ∀ᶠ n in atTop; the claim for every $n$ would be false at small $n$.
• No probability-measure hypothesis is imposed: the theorem is an implication between two families of inequalities. The hypotheses are satisfiable, for instance by any constant mechanism.
• A trivializing formalization is ruled out: $\beta$ is constrained by $n^2\beta_n\to0$, since for $\beta\ge1$ distributional privacy holds for every mechanism and the implication would be false; and the bad event is "some measurable $E$ violates the inequality", not a per-event condition.
• Explicit thresholds: the paper's "$\beta=o(1/n^2)$" with its count "$2/n^2$" becomes $\beta<1/(n+1)^2$ in the fixed-size milestone; no other $O(\cdot)$ appears.
• Out of scope: Theorem 7.5 (the separation) with Definition 7.4, because its query $Q_{2/\varepsilon}$ needs $2/\varepsilon\in\mathbb N$, its databases are bit-vectors rather than sets, and "with constant probability" is never quantified.

Contributions welcome: proofs of the milestone and the goal, and the footnote's $t\varepsilon$ extension for databases differing in $t$ elements, stated as a new theorem.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1, 2011; J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229 , https://doi.org/10.1145/2450142.2450148
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14

Motivation

A data curator holds a database of $n$ records and wants to publish answers to a large family of statistical questions about it without revealing any individual record. Differential privacy (Dwork, McSherry, Nissim, Smith 2006) makes the requirement precise, and the most basic questions are counting queries: what fraction of the records satisfy a given predicate? Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that a single private release can answer every query of a class $C$ to error $\alpha$ once the database has size roughly $\log|X| \cdot \mathrm{VCDIM}(C)/(\alpha^3\epsilon)$, so that the sample size depends on the class only through its VC-dimension, a quantity from learning theory.

This mission formalizes the converse in §3.1 of that paper: the dependence on the VC-dimension cannot be removed. On databases of fewer than $\mathrm{VCDIM}(C)/2$ records, every differentially private mechanism has constant error on some query of $C$. The argument is an early instance of the reconstruction attack idea of Dinur and Nissim (2003): accurate answers to many counting queries determine the database, and a mechanism that determines its input cannot be private.

Setting

Let $X$ be a set (the data universe). An input database of size $n$ is a tuple $z = (z_1,\dots,z_n) \in X^n$. A predicate is a map $\varphi : X \to \{0,1\}$, and its counting query is

$$Q_\varphi(z) = \frac{1}{n}\,\#\{i : \varphi(z_i) = 1\}.$$

A class $C$ of predicates is identified with its class of counting queries. A finite set $S \subseteq X$ is shattered by $C$ if every function $S \to \{0,1\}$ is the restriction of some $\varphi \in C$; the VC-dimension $\mathrm{VCDIM}(C) \in \mathbb N \cup \{\infty\}$ is the supremum of the sizes of shattered sets.

A mechanism $M$ maps each input $z \in X^n$ to a probability distribution $M(z)$ on an output space $O$; an output $o$ is read through an answer map $\mathrm{ans}(o, \varphi) \in \mathbb R$. Two inputs are neighbours if they differ in exactly one entry. The mechanism is $\epsilon$-differentially private if $M(z)(E) \le e^{\epsilon} M(z')(E)$ for all neighbours $z, z'$ and all measurable events $E$. It is $(\alpha,\delta)$-useful for $C$ if for every input $z$, with probability at least $1-\delta$ over $o \sim M(z)$, every query is answered to within $\alpha$:

$$\forall \varphi \in C:\quad |\mathrm{ans}(o,\varphi) - Q_\varphi(z)| \le \alpha .$$

In the paper the output is a synthetic database $\hat D$ and $\mathrm{ans}(\hat D,\varphi) = Q_\varphi(\hat D)$.

Formalization targets

Goal: Theorem 3.11 (p. 11)

There is an absolute constant $c > 0$ such that for every universe $X$, class $C$, size $n \ge 1$ with $n \le \mathrm{VCDIM}(C)/2$, $0 \le \epsilon \le 1$ and $0 < \delta \le 1/4$: every $\epsilon$-differentially private mechanism that is $(\alpha,\delta)$-useful for $C$ on databases of size $n$ satisfies

$$\alpha \ \ge\ \frac{c}{4 + 16\epsilon}.$$

Milestones

1. Lemma 3.12. For a set $S$ of size $d$ and the family $\mathcal D_S$ of its subsets of size $d/2$, and $Q_T$ the counting query of a predicate equal to the indicator of $T$ on $S$: $Q_T(T) - Q_T(T') = |T\Delta T'|/d$ for $T, T' \in \mathcal D_S$.
2. Lemma 3.13. For an $(\alpha,\delta)$-useful mechanism, a fixed procedure recovers from $M(T)$ a set $T' \in \mathcal D_S$ with $|T'\Delta T| \le 2d\alpha$, with probability at least $1-\delta$.
3. The final inequality of the proof (p. 12), with $\delta$ kept. Under the goal's hypotheses with $0 < \delta < 1$ and any $\epsilon$:

$$(1-\delta)(1-2\alpha) \ \le\ e^{\epsilon}(\delta + 2\alpha).$$

Significance

Theorem 3.11 shows that the VC-dimension term in the paper's upper bound is necessary: for a class of VC-dimension $d$, no private mechanism is accurate on databases of size below $d/2$, whatever its running time. It thereby locates the sample complexity of private query release between $\mathrm{VCDIM}(C)$ and $\mathrm{VCDIM}(C)\cdot\log|X|$ up to accuracy and privacy factors, a gap that later work on private learning and on fingerprinting codes studied in detail (Bun, Ullman, Vadhan 2014).

The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a checked reconstruction-attack lower bound for differential privacy, together with the corrected statement disclosed below: the printed proof drops the failure probability $\delta$ of the two reconstructions, and keeping it shows that the conclusion requires $\delta$ below $1/(1+e^{\epsilon})$, not merely "bounded away from 1". Milestone 3 records the inequality the argument actually yields.

Difficulty

The combinatorial core (Lemmas 3.12 and 3.13) is elementary. The difficulty lies in the last step, which compares the output distributions on two different inputs. The paper argues about a uniformly random $T \in \mathcal D_S$, a random element $x \in T$ and a random $y \notin T$, and the swapped set $\hat T = (T\setminus\{x\})\cup\{y\}$. Privacy applies to one fixed pair of neighbouring inputs and one fixed event, while the reconstruction guarantee only controls $|T'\Delta T|$, not whether a particular element is recovered. The "probabilities" $\Pr[x \in T']$ of the printed proof mix the mechanism's randomness with the random choice of $T$, $x$, $y$, and they are not the probability of any single event under any single $M(z)$, so the privacy inequality cannot be applied to them as written. The reconstruction event must also be measurable, which depends on the readout, and the failure probability $\delta$ must be carried through both reconstructions. A proof that sets $\delta = 0$, as the printed one does, does not prove the stated theorem.

Formalization scope

• Databases. Inputs are Fin n → X with $n \ge 1$; the empty database is excluded because every mechanism is private on it and $Q_\varphi = 0/0$ there. In the proof, a set $T \in \mathcal D_S$ is given to the mechanism as any injective listing of its elements.
• Neighbours. The paper's "$|D\Delta D'| \le 1$" for databases of equal size is read as replacing one entry (PrivLearn.Generic.Neighbors); read literally, it would make every mechanism private and the theorem false. Under this reading $T$ and $\hat T$ are neighbours, so the paper's factor $e^{2\epsilon}$ becomes $e^{\epsilon}$.
• Mechanisms. The output space is an arbitrary measurable space and answers are read through ans. Synthetic-data mechanisms are the special case $O =$ databases, so the lower bound covers a larger class of mechanisms. The hypotheses require IsProbabilityMeasure (M z) and the measurability of o ↦ ans o φ for $\varphi \in C$. Without the first, the zero measure is private; without the second, a mechanism into a trivial $\sigma$-algebra would be private and "useful".
• Ω and the range of δ. The paper writes $\alpha \ge \Omega(1/(4+16\epsilon))$ for "$0<\delta<1$ bounded away from 1 by a constant". The Lean goal quantifies one absolute constant $c > 0$ before every other binder and assumes $0 < \delta \le 1/4$. The proof gives $\alpha \ge ((1-\delta) - e^{\epsilon}\delta)/(2(1-\delta+e^{\epsilon}))$, which is positive only for $\delta < 1/(1+e^{\epsilon})$ (about $0.27$ at $\epsilon=1$). The hypotheses $\epsilon \le 1$ and $n \le \mathrm{VCDIM}(C)/2$ are the paper's, the latter written $2n \le \mathrm{VCDIM}(C)$ in $\mathbb N\cup\{\infty\}$.
• Ruled out. The statement quantifies over every mechanism satisfying the hypotheses, randomized or not, so no restriction to deterministic or constant-output mechanisms makes the bound easy. The usefulness event is weighed by a probability measure, so the zero measure cannot be "useful". The constant cannot depend on $n$, $d$, $X$ or $C$.
• Infrastructure. The development reuses the published PrivLearn.Generic.Privacy (neighbours, IsDP) and Vershynin's HighDimProb.Chaining.Shatters and vcDim. Contributions needed: subsets of shattered sets are shattered, and $2n \le \mathrm{VCDIM}(C)$ yields a shattered set of size exactly $2n$; measurability of the argmin reconstruction; the averaging/bijection argument. The first two are reusable beyond this mission.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1 (2011); J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229 , https://doi.org/10.1145/2450142.2450148
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• I. Dinur, K. Nissim, Revealing Information while Preserving Privacy, PODS 2003. https://doi.org/10.1145/773153.773173
• M. Bun, J. Ullman, S. Vadhan, Fingerprinting Codes and the Price of Approximate Differential Privacy, STOC 2014. https://arxiv.org/abs/1311.3158
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018, §8.3 (VC dimension). https://doi.org/10.1017/9781108231596

Motivation

A prophet inequality compares a gambler who sees independent random rewards one at a time, and must accept or reject each on arrival, with a prophet who sees all rewards in advance. The classical inequality of Krengel, Sucheston and Garling (1977–78, as cited in the paper) says that when only one reward may be kept, a single threshold rule earns at least half of $\mathbb E[\max_i X_i]$, and Samuel-Cahn (1984) showed that the threshold can be chosen as a median. Such statements are the analytical core of sequential posted-price mechanisms: Hajiaghayi, Kleinberg and Sandholm (2007) observed that threshold rules are truthful online auctions, and Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices approximate the optimal Bayesian revenue in many settings, with prophet inequalities for the feasibility constraint as the key technique.

When several items may be accepted subject to a combinatorial constraint, the natural constraints in this application are matroids (for example, at most $k$ items, or at most one item per group) and intersections of matroids (for example, bipartite matchings, which are intersections of two partition matroids). Kleinberg and Weinberg (STOC 2012) proved that for every matroid there is an online algorithm with expected payoff at least half of the expected maximum-weight basis, and that for the intersection of $p$ matroids the summed version of the same algorithm earns at least $\frac{1}{4p-2}$ of the expected optimum. This mission formalizes the second result.

Timeline:

• 1977–78: Krengel–Sucheston and Garling, single-choice prophet inequality with factor 2.
• 1984: Samuel-Cahn, the median threshold rule attains factor 2.
• 2007: Hajiaghayi–Kleinberg–Sandholm, threshold rules from prophet inequalities read as truthful online auction mechanisms.
• 2010: Chawla–Hartline–Malec–Sivan, sequential posted pricing; factor 2 for matroids when the algorithm may choose the order in which elements are observed.
• 2012: Kleinberg–Weinberg, factor 2 for matroids and $4p-2$ for intersections of $p$ matroids, against online weight-adaptive adversaries.

Setting

A finite ground set $\mathcal U$ carries $p \ge 1$ matroids $\mathcal M_1,\dots,\mathcal M_p$ with independent sets $\mathcal I_1,\dots,\mathcal I_p$ and closure operators $\mathrm{cl}_1,\dots,\mathrm{cl}_p$. A set is feasible if it lies in $\mathcal I = \bigcap_j \mathcal I_j$. Each element $x$ has a random weight $w(x) \ge 0$; the weights are independent and $w(x)$ has law $F_x$. For a set $S$, $w(S) = \sum_{x \in S} w(x)$, $\mathrm{OPT}(w) = \max\{w(S) : S \in \mathcal I\}$, and $\mathrm{OPT} = \mathbb E[\mathrm{OPT}(w)]$.

An online weight-adaptive adversary reveals the elements one at a time; it chooses the $i$-th element $x_i$ after learning $w(x_1),\dots,w(x_{i-1})$, but without knowing $w(x_i)$ or any other unrevealed weight. A threshold algorithm offers $x_i$ a threshold $T_i$ computed from what has been revealed and from the set $A_{i-1}$ already selected, and selects $x_i$ exactly when $A_{i-1}\cup\{x_i\}\in\mathcal I$ and $w(x_i) \ge T_i$.

The algorithm of the paper uses a ghost sample $w'$, an independent copy of $w$. Let $B$ be a $w'$-maximum feasible set. For a set $A$ and each $j$, $R_j(A) \subseteq B \setminus A$ is a set of maximum $w'$-weight with $A \cup R_j(A) \in \mathcal I_j$ and $B \subseteq \mathrm{cl}_j(A \cup R_j(A))$, and $C_j(A) = B \setminus R_j(A)$. Put $R(A) = \bigcap_j R_j(A)$ and $C(A) = \bigcup_j C_j(A)$. For a parameter $\alpha$, the summed thresholds are

$$T(A,i) = \sum_{j=1}^p \frac1\alpha\, \mathbb E_{w'}\big[w'(R_j(A)) - w'(R_j(A \cup \{x_i\}))\big],$$

and the algorithm of §4.2 uses $T_i = T(A_{i-1}, i)$. An algorithm has $\alpha$-balanced thresholds (Definition 3) if, for every input sequence with selected set $A$ and every $V$ disjoint from $A$ with $A \cup V \in \mathcal I$,

$$\sum_{x_i\in A} T_i \ge \frac1\alpha \mathbb E\Big[\sum_j w'(C_j(A))\Big], \qquad \sum_{x_i\in V} T_i \le \frac1\alpha \mathbb E\Big[\sum_j w'(R_j(A))\Big].$$

Formalization targets

Goal: the prophet inequality for $p$ matroids

For every $p \ge 1$, all matroids $\mathcal M_1,\dots,\mathcal M_p$ on $\mathcal U$, all laws $F_x$ on $[0,\infty)$ with finite means, and every online weight-adaptive adversary, the algorithm of §4.2 with $\alpha = 2p$ selects a set $A$ with

$$\mathbb E[w(A)] \ge \frac{1}{4p-2}\, \mathbb E[\mathrm{OPT}(w)].$$

For $p = 1$ this is the factor-2 matroid prophet inequality.

Proposition 3

If a threshold algorithm has $\alpha$-balanced thresholds for some $\alpha \ge 2$, then against every online weight-adaptive adversary

$$\mathbb E[w(A)] \ge \frac{\alpha - p}{\alpha(\alpha-1)}\, \mathrm{OPT}.$$

Milestones

Proposition 2 for each matroid $\mathcal M_j$; the identity between the two forms of $T(A,i,j)$; properties (13) and (14) for the summed thresholds; the identities (20)–(21); and the inequalities (23)–(24) of Appendix A. Together with Proposition 3 these give the goal.

Significance

The bound gives a posted-price style selection rule for any feasibility constraint that is an intersection of $p$ matroids, with a guarantee depending only on $p$; the paper's §5 shows that a ratio of order $p$ is necessary. Section 6 of the paper turns the result into sequential posted-price mechanisms for multi-dimensional mechanism design, and that application needs the guarantee against the online weight-adaptive adversary, not only against a fixed order. The reduction "balanced thresholds imply an approximation" (Proposition 3) is reusable for other threshold constructions.

The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a formal proof of the $\frac{1}{4p-2}$ guarantee, with the probabilistic part (the ghost-sample argument against an adaptive adversary) and the combinatorial part (the per-matroid exchange inequality) as separate milestones. The paper justifies the per-matroid use of Proposition 2 in one paragraph; because $B$ maximizes $w'$ over the intersection rather than over $\mathcal I_j$, the description of $R_j(A)$ as a maximum-weight basis of a contraction (Lemma 2 in the single-matroid case) does not apply verbatim, and the formal proof of that milestone is not a copy of the paper's single-matroid argument.

Difficulty

Two steps do not follow from routine bookkeeping. First, the inequality (23) compares the gambler's surplus, collected along an order that the adversary adapts to the realized weights, with the ghost sample's surplus on the random set $R(A)$. The index $x_i$ revealed at step $i$ is itself random, so the step "the weight of the element offered next is distributed as its ghost weight" has to be justified for an adaptively chosen index under a product measure; it fails for an adversary that may look at unrevealed weights. Second, the paper obtains (14) by applying the single-matroid Proposition 2 to each $\mathcal M_j$, but its proof of Proposition 2 describes $R(A)$ as a maximum-weight basis of a contraction, which uses that $B$ is optimal for the matroid in question. Here $B$ is optimal only for the intersection $\mathcal I$, so the obvious transfer of the single-matroid argument does not go through as written and the per-matroid statement needs its own proof.

Formalization scope

The ground set is a Fintype; the matroids are Mathlib's Matroid α, indexed by Fin p, each with ground set Set.univ; sets are Finset α. Weights are functions α → ℝ, the weight law is Measure.pi F, and every theorem assumes each F x is a probability measure with F x (Iio 0) = 0 and a finite mean. Expectations are Bochner integrals; under these assumptions every integrand is integrable. Ties in the maximizers $B$ and $R_j(A)$ are broken by a fixed rule that does not depend on the weights. $R_j(A)$ is taken disjoint from $A$. The threshold $\infty$ on infeasible steps is a feasibility test in the selection rule. Adversaries and generic threshold rules are deterministic, see only revealed weights, and are measurable in them; randomized adversaries are mixtures of deterministic ones. Generic thresholds in Proposition 3, (23) and (24) are non-negative, as in the paper's $T_i \in \mathbb R_+ \cup \{\infty\}$.

The goal fixes the thresholds to the summed thresholds of §4.2 with $\alpha = 2p$, computed from the ghost-sample objects. A version in which the thresholds are free parameters assumed to satisfy (13)–(14) would be Proposition 3 itself and is ruled out; conversely, Proposition 3 does not mention the §4.2 thresholds.

A complete development needs: elementary facts about maximizers over finite families; matroid exchange properties (a bijective exchange between equal-size independent sets, available in Schrijver's book but not in Mathlib); submodularity of weighted-rank-type functions; and the independence argument for adaptively chosen indices under a product measure. The last two are reusable beyond this mission, as is Proposition 3. Proofs of individual milestones and of these auxiliary facts are welcome.

Selected references

• R. Kleinberg, S. M. Weinberg, Matroid Prophet Inequalities, STOC 2012; arXiv:1201.4764v1. https://arxiv.org/abs/1201.4764, https://doi.org/10.1145/2213977.2213991
• U. Krengel, L. Sucheston, Semiamarts and finite values, Bull. Amer. Math. Soc. 83 (1977), 745–747.
• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12 (1984). https://doi.org/10.1214/aop/1176993150
• M. T. Hajiaghayi, R. Kleinberg, T. Sandholm, Automated online mechanism design and prophet inequalities, Proc. 22nd AAAI Conference on Artificial Intelligence, 2007, pp. 58–65.
• S. Chawla, J. Hartline, D. Malec, B. Sivan, Multi-parameter mechanism design and sequential posted pricing, STOC 2010, pp. 311–320; arXiv:0907.2435. https://arxiv.org/abs/0907.2435
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer 2003 (Corollary 39.12a).