Lean for differential privacy

Stream: general

[Alexander Bentkamp]

The goal of differential privacy is to share information about a database without giving away information about individuals in that database. I'd like to share a collaboration with some colleagues working in that area. I helped them to verify their latest result: https://arxiv.org/pdf/2205.03470.pdf. Search the PDF for "Lean" to see the interesting bits ;-).

The formalization process revealed that the first version of the theorem was flawed and we had to fix it. All authors and all reviewers had missed that flaw before we started to formalize.

[Rémy Degenne]

Very nice!
I am very happy to read that you found the measurability tactic useful. The paper also mentions in section 3.2 that some measurability proofs had to be done by hand. I would be glad to know about any measurability goal that the tactic did not solve, but which should be simple enough for it to work. I want to work on that tactic again soon, in particular to make it prove strongly_measurable goals but also to improve it generally.

[Alexander Bentkamp]

@Rémy Degenne Here are two examples:

-- lean_version = "leanprover-community/lean:3.32.1"
-- mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "2e1e98fac6fa181ce57f9ce04914bf4cbe3120bd"}

import measure_theory.constructions.pi
import data.matrix.notation

open measure_theory

@[measurability]
lemma measurable.vec_cons {n : ℕ} {α β : Type} [measurable_space α] [measurable_space β]
  {f : β → α} {g : β → fin n → α}
  (hf : measurable f) (hg : measurable g) :
  measurable (λ x, matrix.vec_cons (f x) (g x)) :=
sorry

example (O Ω : Type*) [measurable_space O] [measurable_space Ω] (n : ℕ) :
  measurable (λ (oω : O × (fin n → Ω)),
    matrix.vec_cons oω.fst matrix.vec_empty) :=
begin
  apply measurable.vec_cons,
  measurability,
end

example (O : Type*) [measurable_space O] (s: set (O × O)) (hs: measurable_set s) :
measurable_set
    {ω : O × O | (ω.snd, ω.fst) ∈ s} :=
begin
  apply measurable.prod_mk,
  measurability
end

Note that the mathlib version is a bit old. Maybe the issues have been fixed in the meantime?

For the first example, I don't understand at all why I have to apply measurable.vec_cons manually.

In the second example, I'd understand if it is beyond the scope of the tactic to apply measurable.prod_mk automatically, but maybe it's worth considering.

[Rémy Degenne]

Thanks! I'll look into it.