John Tristan: Verified Foundations for Differential Privacy

Stream: Lean Together 2025

[Markus de Medeiros]

Discussion thread for the talk

[Johan Commelin]

Very nice talk. I had heard about this project several times. Excited to see some of the details now. Impressive project!

@David Loeffler The Jacobi $\theta$ function features around p26. This is a really cool aspect of mathlib! Really abstract stuff used in this industrial application.

[Kim Morrison]

https://www.youtube.com/watch?v=nEMaiZD3iQk&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg&index=19

[David Loeffler]

Johan Commelin said:

Very nice talk. I had heard about this project several times. Excited to see some of the details now. Impressive project!

David Loeffler The Jacobi $\theta$ function features around p26. This is a really cool aspect of mathlib! Really abstract stuff used in this industrial application.

That is indeed a really fun and unexpected application!