Theoretical Computer Science

Motivation

A constraint satisfaction problem (CSP) asks whether variables can be assigned values from a finite domain so that every constraint, drawn from a fixed list of allowed relations, is satisfied. A promise CSP (PCSP) relaxes the question: given two templates $\mathbf A$ and $\mathbf B$ with a homomorphism $\mathbf A\to\mathbf B$, distinguish instances satisfiable in $\mathbf A$ from instances not even satisfiable in the weaker $\mathbf B$. Approximate graph colouring (colour a graph with more colours than its chromatic number) is the standard example. For CSPs, the resolution of the Feder–Vardi dichotomy conjecture by Bulatov and Zhuk (FOCS 2017) ties tractability to the existence of polymorphisms satisfying non-trivial identities; for PCSPs no such dichotomy is known, and the question of which polymorphism families yield algorithms is open in general.

A polymorphism of a PCSP is a function $f:A^L\to B$ mapping tuples of rows satisfying the strict constraints to columns satisfying the weak ones. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383v3, SIAM J. Comput. 2020) give a single algorithm, BLP+Affine, that decides every PCSP with infinitely many symmetric polymorphisms, and extend it to block-symmetric polymorphisms. As a corollary the same algorithm solves all tractable Boolean CSPs of Schaefer's dichotomy (2-SAT, Horn-SAT and its dual, linear equations mod 2).

Timeline, as recorded in the paper's introduction:

• 2012: Kun, O'Donnell, Tamaki, Yoshida and Zhou (ITCS 2012): with symmetric polymorphisms of all arities, the Basic LP alone decides the CSP; with only some arities (e.g. odd majorities) it does not.
• 2017: Austrin, Guruswami and Håstad classify $(2+\epsilon)$-SAT and introduce polymorphisms for PCSPs (SIAM J. Comput. 46(5), 2017).
• 2018–2019: Brakensiek and Guruswami study PCSPs through polymorphisms; their SODA 2019 algorithm (arXiv:1807.05194) solves the search version for PCSPs with structured symmetric polymorphisms (threshold, threshold-periodic, regional), combining an LP over $\mathbb Z[\sqrt2]$ with an affine relaxation over a finite ring.
• 2019: Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970) show that the identities satisfied by polymorphisms, captured by minion homomorphisms, determine the complexity of a PCSP.
• 2019–2020: the present paper. Theorem 2 needs only that $f$ be symmetric, with no structure beyond that; Theorem 3 handles any number of blocks; Theorem 4 characterizes exactly the PCSPs that BLP+Affine solves.

Setting

A signature $\tau$ is a set of symbols $R$ with arities $\mathrm{ar}(R)$. A relational structure $\mathbf A$ on a finite domain $A$ gives, for each $R$, a relation $R^{\mathbf A}\subseteq A^{\mathrm{ar}(R)}$. A homomorphism $\mathbf A\to\mathbf B$ is a map $\sigma:A\to B$ sending every tuple of $R^{\mathbf A}$, componentwise, into $R^{\mathbf B}$; $(\mathbf A,\mathbf B)$ is a promise template when one exists.

An instance $X$ has variables $x_1,\dots,x_n$ and constraints $c_j=(R_j,\bar x_j)$, $j\in[m]$, where $\bar x_j$ is a tuple of $\mathrm{ar}(R_j)$ variables. $X$ is satisfiable in $\mathbf A$ if some assignment sends every $\bar x_j$ into $R_j^{\mathbf A}$.

A polymorphism of $(\mathbf A,\mathbf B)$ of arity $L$ is $f:A^L\to B$ such that for every $R$ and every $L\times\mathrm{ar}(R)$ matrix whose rows lie in $R^{\mathbf A}$, applying $f$ to each column gives a tuple in $R^{\mathbf B}$. It is symmetric if it is invariant under all permutations of its $L$ arguments.

The Basic LP $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has rational unknowns $w_i(a)\ge0$, a distribution on $A$ for each variable, and $p_j(y)\ge0$, a distribution on $R_j^{\mathbf A}$ for each constraint, linked by the marginal conditions $\sum_{y:\,y_k=a}p_j(y)=w_i(a)$ when $x_i$ is the $k$-th variable of $\bar x_j$. The affine relaxation $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ is the same system of equations in integer unknowns $r_i(a)$, $q_j(y)$, with no sign constraints.

The BLP+Affine algorithm (Figure 1) finds a relative interior point $(w,p)$ of $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$, rejecting if there is none; restricts the affine system to $\mathrm{Aff}'_{\mathbb Z}(X,\mathbf A)$ by forcing $r_i(a)=0$ wherever $w_i(a)=0$ and $q_j(y)=0$ wherever $p_j(y)=0$; and accepts if and only if the restricted system has an integer solution. It correctly solves $\mathrm{PCSP\text{-}Decision}(\mathbf A,\mathbf B)$ (Definition 1) if it accepts every instance satisfiable in $\mathbf A$ and rejects every instance unsatisfiable in $\mathbf B$.

Formalization targets

Goal: Theorem 2 (p. 6)

$$\Bigl(\forall N\ \exists L\ge N\ \exists f:A^L\to B \text{ symmetric polymorphism of } (\mathbf A,\mathbf B)\Bigr)\ \Longrightarrow\ \text{BLP+Affine correctly solves } \mathrm{PCSP\text{-}Decision}(\mathbf A,\mathbf B).$$

The hypothesis is a property of the template alone; the conclusion quantifies over all instances.

Milestones, in attack order

1. Footnote 1 (p. 5): a feasible $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has a solution of maximal support.
2. Completeness (p. 6): an instance satisfiable in $\mathbf A$ is accepted.
3. Rounding of variables (pp. 6–7): $W_i(a)=u\ell w_i(a)+v r_i(a)$ are non-negative integers with $\sum_a W_i(a)=L$, for $L=u\ell+v\ge M\ell^2$, $0\le v<\ell$.
4. Rounding of constraints (p. 7): $P_j(y)=u\ell p_j(y)+v q_j(y)$ are non-negative integers with $\sum_y P_j(y)=L$.
5. Eq. (9) (p. 7): $W_i(a)=\sum_{y:\,y|i=a}P_j(y)$.
6. Satisfying assignment (p. 7): $X_i:=f(a,\dots,a\ [W_i(a)\text{ times}])$ satisfies $X$ in $\mathbf B$.

Companion: Theorem 3 (p. 8)

The same conclusion when $\mathrm{Pol}(\mathbf A,\mathbf B)$ contains block-symmetric polymorphisms of arbitrarily large width: $[L]$ is split into blocks, each of size at least $N$, within which $f$ is invariant.

Significance

Theorem 2 gives one algorithm that decides every PCSP with an infinite family of symmetric polymorphisms, without knowing or evaluating the polymorphisms; it subsumes the BLP-then-AIP algorithm of Brakensiek and Guruswami for Boolean templates and applies over any finite domain. Theorem 3 extends this to block-symmetric families, which covers nearly all known tractable Boolean PCSPs, including 1-in-3-SAT versus NAE-SAT, whose alternating threshold polymorphisms are block-symmetric but not symmetric.

The results are proved in the paper. No machine-checked formalization of PCSPs, polymorphisms or the Basic LP is known to exist; Mathlib has no theory of constraint satisfaction. This mission produces a formal model of promise templates, instances, polymorphisms, the two relaxations and the algorithm's acceptance condition, together with a formal proof of the correctness theorem. The same model is the starting point for the characterization theorem (Theorem 4) treated in the companion mission.

Difficulty

Completeness is routine. Soundness is the substance: from a rational LP solution and an integer solution of the refined affine system one must produce an actual assignment in $\mathbf B$, using a polymorphism whose arity is chosen only after the instance is known. The natural first idea, clearing denominators of the LP solution and feeding the resulting multiplicities to a polymorphism, needs a polymorphism of exactly the arity the denominators dictate; with polymorphisms of only some arities it fails, and the paper's introduction notes that the LP alone does not suffice there. An integer affine solution, on the other hand, may have negative entries, which are not multiplicities. The paper stresses that the affine system must be the one refined by the support of a relative interior point: an arbitrary solution of the unrefined lattice gives no control on where the negative entries sit. In the formalization, the counting step (the columns of the matrix built from the constraint multiplicities have the variable multiplicities) and the passage from equal multiplicities to equal values of a symmetric function require explicit combinatorics on finite tuples, and the existence of a maximal-support LP solution requires an averaging argument over the finite set of coordinates.

Formalization scope

All declarations are in the namespace PCSPBLPAff.Symmetric. Conventions:

• Domains are Lean types with Fintype and DecidableEq; variables are Fin n, constraints Fin m, and a constraint's scope is a function Fin (ar R_j) → Fin n, possibly repeating variables.
• Arities are any natural numbers (the page asks for positive arities; every statement remains true for arity 0).
• The LP is over $\mathbb Q$ and the affine system over $\mathbb Z$. The weights $p_j$, $q_j$ are total functions on $A^{\mathrm{ar}(R_j)}$ required to vanish off $R_j^{\mathbf A}$.
• The marginal conditions (5) and (8) are imposed per position of the scope.
• The relative interior point is encoded by its only property the algorithm uses (footnote 1): a solution whose support contains the support of every solution. Acceptance requires such a solution and an affine solution vanishing outside its support.
• A block-symmetric function of width at least $N$ has at least one block, each block of size at least $N$.
• The polynomial-time claims of the paper, and the Remark on $\mathbb Z[\sqrt2]$, are out of scope: the algorithm is formalized by its acceptance condition.

The acceptance condition must not be replaced by "the LP is feasible and $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ has a solution", nor by an affine solution vanishing outside the support of an arbitrary LP solution; the first is a different algorithm and the second bypasses footnote 1.

Contributions welcome: proofs of the milestones, in particular the combinatorial lemma that a symmetric function takes the same value on tuples with the same multiplicities, and the averaging argument for maximal-support solutions; the block-wise version for Theorem 3.

Selected references

• J. Brakensiek, V. Guruswami, M. Wrochna, S. Živný, The Power of the Combined Basic Linear Programming and Affine Relaxation for Promise Constraint Satisfaction Problems, SIAM J. Comput. 49(6), 2020; arXiv:1907.04383v3. https://arxiv.org/abs/1907.04383v3
• J. Brakensiek, V. Guruswami, An Algorithmic Blend of LPs and Ring Equations for Promise CSPs, SODA 2019. https://arxiv.org/abs/1807.05194
• J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Structure Theory and a Symmetric Boolean Dichotomy, SODA 2018. https://arxiv.org/abs/1704.01937
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic Approach to Promise Constraint Satisfaction, J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970

Motivation

A snark is a cubic graph that cannot be properly edge-coloured with three colours and that does not reduce to a smaller such graph. Snarks are the smallest possible counterexamples to several central conjectures about cubic graphs, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture, so structural statements about snarks narrow the search for counterexamples to those conjectures.

Permutation graphs are cubic graphs built from two disjoint cycles of equal length joined by a perfect matching, so that the two cycles are induced. The Petersen graph is the classical example: its outer 5-cycle and inner pentagram are joined by five spokes. In his monograph Integer Flows and Cycle Covers of Graphs (1997), C.-Q. Zhang conjectured that the Petersen graph is the only permutation snark that is also cyclically 5-edge connected.

Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, J. Combin. Theory Ser. B 103, 2013) built a generator for snarks and enumerated all snarks up to 36 vertices. Among them they found twelve cyclically 5-edge-connected permutation snarks on 34 vertices, which refute Zhang's conjecture (Observation 4.2), and they printed all twelve in Appendix 8.6 of the paper. This mission formalizes the refutation using the first of those graphs.

Setting

All graphs are finite and simple. A cycle is a 2-regular connected graph. A graph is cubic if every vertex has degree 3. A 2-factor of $G$ is a spanning 2-regular subgraph. The girth $g(G)$ is the number of vertices in a shortest cycle of $G$.

A cubic graph is colourable if it has a proper 3-edge-colouring: a map $c : E(G) \to \{1,2,3\}$ giving distinct colours to distinct edges with a common endpoint. Otherwise it is uncolourable.

A graph $G$ is cyclically $k$-edge connected if deleting fewer than $k$ edges from $G$ never leaves two distinct components that both contain a cycle.

A snark is an uncolourable, cyclically 4-edge connected cubic graph with $g(G) \ge 5$.

A cubic graph is a permutation graph if it has a 2-factor consisting of two induced cycles. Equivalently, its vertex set splits as $A \cup (V \setminus A)$ with both induced subgraphs $G[A]$ and $G[V \setminus A]$ cycles. A permutation snark is a snark that is a permutation graph.

The Petersen graph $P$ is the graph on $\{0,\dots,9\}$ with the outer cycle $i \sim i+1 \pmod 5$, the spokes $i \sim i+5$, and the inner pentagram $5+i \sim 5+((i+2) \bmod 5)$.

Zhang's Conjecture 4.1. Let $G$ be a cubic cyclically 5-edge-connected permutation graph. If $G$ is a snark, then $G$ must be the Petersen graph.

The witness $G_1$ is the first graph in Appendix 8.6 (p. 36). It is given as a list of higher-numbered neighbours of the vertices $1,\dots,34$; decoded, it has 51 edges. In the Lean development the paper's vertex $i$ is i - 1 : Fin 34.

Formalization targets

Goal: Observation 4.2, first sentence

$$\neg\,\mathrm{ZhangConjecture},$$

that is, there is a finite cubic, cyclically 5-edge connected permutation snark that is not isomorphic to the Petersen graph. This is SnarkGen.Zhang.observation_4_2.

Milestones: the properties of $G_1$

Each milestone is a property of $G_1$ asserted by the heading of Appendix 8.6, "The 12 cyclically 5-edge connected permutation snarks on 34 vertices":

1. $G_1$ is cubic;
2. $g(G_1) \ge 5$;
3. $G_1$ is cyclically 5-edge connected;
4. $G_1$ is a permutation graph;
5. $G_1$ is uncolourable;
6. $G_1$ is a snark;
7. $G_1$ satisfies all hypotheses of Conjecture 4.1 and $G_1 \not\cong P$.

The goal follows from milestone 7 directly. Two supporting theorems are included: cyclic $k$-edge connectivity is monotone in $k$, and the paper's remark (p. 9) that every permutation snark has order $\equiv 2 \pmod 4$.

Significance

Zhang's conjecture predicted that the Petersen graph is isolated among highly connected permutation snarks. Its refutation shows that this is false, and the twelve 34-vertex graphs went on to serve as counterexamples to further conjectures in the same paper (Conjectures 5.17, 5.20 and 5.21, about cycle double covers containing a prescribed 2-factor). They are also listed in the House of Graphs database.

The refutation in the paper is a computer result: the graphs were found by an exhaustive search, and their properties were checked by programs. A formal proof would replace that check with a machine-verified one that is independent of the generator. It would also produce reusable certified tools for finite cubic graphs: a kernel-checked test for uncolourability, cyclic edge connectivity, and girth. No machine-checked proof of any of these properties of $G_1$ is known to exist.

Difficulty

The statements are short, but none of the properties of $G_1$ follows from a general theorem; each must be checked on the specific graph. The obvious approach, to unfold the definitions and let a decision procedure enumerate, does not scale:

• Uncolourability quantifies over all $3^{51}$ edge colourings.
• Cyclic 5-edge connectivity quantifies over all edge sets of size at most 4 (about 270,000 of them among 51 edges), and for each one over the components of the remaining graph and the cycles inside them.
• The permutation structure requires exhibiting the two induced 17-cycles and proving that each induced subgraph is connected and 2-regular.
• Girth requires ruling out all cycles of length 3 and 4.

The definitions are stated in terms of Mathlib's general notions (line graphs, walks, connected components), not in terms of a computable representation. Connecting them to an efficient computation is the main work.

Formalization scope

Graphs are SimpleGraph V with [Fintype V]. The conventions are as follows.

• "Colourable" is G.lineGraph.Colorable 3, a proper 3-colouring of the line graph. It is not a vertex colouring of $G$.
• Cyclic $k$-edge connectivity quantifies over finite edge sets S ⊆ G.edgeSet with S.card < k. Components and cycles are taken in G.deleteEdges S.
• Girth is 5 ≤ G.egirth, the extended girth, which is $\infty$ for acyclic graphs.
• Degrees in the general predicates use classical decidability. Any other decidability instance gives the same degrees.
• The conjecture quantifies over all finite vertex types in Type and reads "must be the Petersen graph" as Nonempty (H ≃g petersen).

The conjecture keeps every printed hypothesis, including the redundant "cubic". Dropping "permutation graph" or "cyclically 5-edge connected" would make the refutation easier, since other cyclically 5-edge-connected snarks are known. The cyclic connectivity must be computed in the graph after deletion and must require both components to contain a cycle; otherwise it degenerates into ordinary edge connectivity, which is at most 3 for cubic graphs and would make the conjecture vacuous.

Proofs should be checked by the Lean kernel. The decision procedures for colourability and cyclic connectivity are the reusable part of this mission, and contributions that build them for arbitrary finite cubic graphs are welcome.

Out of scope.

• The second and third sentences of Observation 4.2 ("The smallest counterexamples have 34 vertices, and there are exactly 12 counterexamples of that order"). They rest on an exhaustive enumeration of all snarks up to 36 vertices.
• The other eleven graphs of Appendix 8.6.
• Conjectures 5.17, 5.20 and 5.21. Their refutation needs the "no cycle double cover contains this 2-factor" certificate of Observation 5.18.
• The counts in Table 3.

Selected references

• G. Brinkmann, J. Goedgebeur, J. Hägglund, K. Markström, Generation and properties of snarks, arXiv:1206.6690v3, 2013; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1206.6690v3
• C.-Q. Zhang, Integer Flows and Cycle Covers of Graphs, Monographs and Textbooks in Pure and Applied Mathematics 205, Marcel Dekker, 1997.
• G. Brinkmann, K. Coolsaet, J. Goedgebeur, H. Mélot, House of Graphs: a database of interesting graphs, Discrete Appl. Math. 161 (2013), 311–314. https://doi.org/10.1016/j.dam.2012.07.018

Motivation

For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form $\mathbf x^\top A\mathbf x$ on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form $\mathcal A(\mathbf x,\mathbf x,\mathbf x)$ on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.

Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$. A set of vertices is stable if no two of its members are adjacent; the stability number $\alpha(G)$ is the size of a largest stable set, so $1\le\alpha(G)\le v$.

Put $n=v+v(v-1)/2$ and write a vector of $\mathbb R^n$ as $\mathbf z=(\mathbf x,\mathbf y)$, with $\mathbf x=(x_1,\dots,x_v)$ indexed by vertices and $\mathbf y=(y_{ij})_{i<j}$ indexed by pairs of vertices. The tensor $\mathcal S_G=[\![s_{abc}]\!]\in\mathbb R^{n\times n\times n}$ has entry $1$ at the six orderings of the triple of coordinates $(x_i,x_j,y_{ij})$ for every non-adjacent pair $i<j$, and $0$ elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.

For a real 3-tensor $\mathcal A=[\![a_{abc}]\!]$ the cubic form is $\mathcal A(\mathbf z,\mathbf z,\mathbf z)=\sum_{a,b,c}a_{abc}z_az_bz_c$, and a real $\lambda$ is a unit $\ell^2$-eigenvalue of $\mathcal A$ if

$$\sum_{a,b}a_{abc}z_az_b=\lambda z_c\quad\text{for all }c,\qquad\text{for some }\mathbf z\text{ with }\|\mathbf z\|_2=1 .$$

Finally, $\lambda_l=2\sqrt{\tfrac23\left(1-\tfrac1l\right)}$ for $l\ge1$. In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and $\alpha(G)$ is Mathlib's SimpleGraph.indepNum.

Formalization targets

Goal: Theorem 9.3, core

$$\alpha(G)=\max\{\,l\in\{1,\dots,v\}:\ \lambda_l\text{ is a unit }\ell^2\text{-eigenvalue of }\mathcal S_G\,\}.$$

That is, $\lambda_{\alpha(G)}$ is an eigenvalue of $\mathcal S_G$, and no $\lambda_l$ with $\alpha(G)<l\le v$ is. This is the statement on which the paper's $v$-query reduction rests; nothing is claimed about $l<\alpha(G)$.

Milestones, in the paper's order

1. Theorem 9.2 (Nesterov). With $\mathbb S^{n-1}=\{(\mathbf x,\mathbf y):\|\mathbf x\|_2^2+\|\mathbf y\|_2^2=1\}$,

$$\sqrt{1-\frac1{\alpha(G)}}=3\sqrt{\frac32}\cdot\max_{(\mathbf x,\mathbf y)\in\mathbb S^{n-1}}\ \sum_{i<j,\ \{i,j\}\notin E}x_ix_jy_{ij}.$$

2. The tensor. $\mathcal S_G$ is symmetric and $\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=6\sum_{i<j,\{i,j\}\notin E}x_ix_jy_{ij}$.
3. The maximum is an eigenvalue. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)$ is attained and is a unit $\ell^2$-eigenvalue of $\mathcal S_G$.
4. Its value. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=\lambda_{\alpha(G)}$.
5. Further result: Theorem 6.9 (Banach), (23). For every symmetric $\mathcal S\in\mathbb R^{n\times n\times n}$,

$$\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}=\sup_{\mathbf x\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf x,\mathbf x)|}{\|\mathbf x\|_2^3},$$

both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.

Significance

The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.

Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor $1/\sqrt2$ (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.

Difficulty

The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing $\mathbf x$ and maximizing over $\mathbf y$ by Cauchy–Schwarz, reduces the cubic problem to a quartic one in $\mathbf x$, whose value still has to be identified with $\alpha(G)$; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of $\mathcal S_G$ is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.

Formalization scope

• Tensors and indices. A 3-tensor is a function ι → ι → ι → ℝ on a finite index type. For $\mathcal S_G$ the index type is the disjoint union of the vertices Fin v and the pairs $\{(i,j): i<j\}$; this is $\mathbb R^n$ with coordinates labelled by name instead of by the paper's enumeration $\varphi(i,j)=(i-1)v-i(i-1)/2+j-i$. Vertices are $0,\dots,v-1$.
• Normalization. Eigenvalues are taken with a unit eigenvector. The paper's Problem 9.1 and Definition 5.1 say only $\mathbf x\ne\mathbf 0$; since $(\lambda,\mathbf x)\mapsto(t\lambda,t\mathbf x)$ preserves the eigen-equation, that reading would make every nonzero real an eigenvalue of $\mathcal S_G$ and the goal false. The unit sphere (13) is where the paper derives the notion.
• Explicit readings. The paper's index range "$1\le i<j<k\le v$" in the definition of $s_{ijk}$ is read as $k\le n$ (taken literally it gives $\mathcal S_G=0$). Every "max" is stated as a greatest element, so attainment is claimed. In (23) the suprema are real suprema over nonzero vectors with boundedness part of the conclusion. $v\ge1$ is assumed wherever the paper uses $\alpha(G)\in\{1,\dots,v\}$.
• Not formalized. The oracle procedure of the proof of Theorem 9.3, the polynomial size of $\mathcal S_G$, the input model of Problem 9.1 with quadratic irrationalities (Remark 9.4), and the NP-completeness of the stability number (Karp 1972, via $\alpha(G)=\omega(\overline G)$). The goal is the mathematical core of the Turing reduction, not a complexity statement.
• Trivializations ruled out. Without the unit normalization the eigenvalue statements are trivial or false; a goal stating only (a), or only an inequality between the maximum and $\lambda_{\alpha(G)}$, would not determine $\alpha(G)$; both are excluded by the statements above.
• Infrastructure. Everything rests on Mathlib (SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, Journal of the ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5: https://arxiv.org/abs/0911.1393)
• Yu. Nesterov, Random walk in a simplex and quadratic optimization over convex polytopes, CORE Discussion Paper 2003/71, 2003. http://edoc.bib.ucl.ac.be:83/archive/00000238/01/dp2003-71.pdf
• E. de Klerk, The complexity of optimizing over a simplex, hypercube or sphere: a short survey, Central European Journal of Operations Research 16, 111–125, 2008. https://doi.org/10.1007/s10100-007-0052-9
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian Journal of Mathematics 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in ($L^2$), Studia Mathematica 7(1), 36–44, 1938 (reference [Banach 1938] of Hillar–Lim).
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 1, 129–132, 2005. https://arxiv.org/abs/math/0607648
• L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40, 1302–1324, 2005. https://doi.org/10.1016/j.jsc.2005.05.007
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

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