Sam Schlesinger(they/them)
Cryptography, formalization, and the mathematics of freedom.
I’m a cryptography engineer at Google Chrome, where I lead the design of private authentication for the web: anonymous credentials that let a site tell a good-faith visitor from an abusive one without learning who anyone is. That work runs through the IETF as MoLE with collaborators at Mozilla and Cloudflare, and Anonymous Tokens with Hidden Metadata, which already filters spam between RCS and iMessage. I chair the W3C Anti-Fraud Community Group, which sets requirements for this work.
In the open, I write Lean 4: a formalization of complexity theory, statements of open conjectures, a proof of the consensus protocol I co-designed at Casper Labs, and leanlings, seventy small exercises for learning the language. I’m a maintainer of CSLib, Lean’s centralized computer science repository, focused on complexity and cryptography. I also make Computable Secrets, a YouTube channel on theoretical computer science. Recent videos cover Shannon’s 1948 paper, Kolmogorov complexity, System F, and the relativization barrier.
Before Chrome I worked on consensus research at Casper Labs and as a software engineer at SimSpace. I studied computer science and mathematics at UMass Amherst, and I’ve taught high schoolers through Google’s Code Next and independently by presenting at schools.
Selected work
Things you can open today. The rest is on the GitHub page.
Anonymous Credit Tokens
A Privacy Pass credential with a hidden balance. The issuer grants credit once; the holder spends it in unlinkable pieces. With Jonathan Katz. Rust implementation and a Privacy Pass issuance profile alongside.
Moderation of unLinkable Endorsements
With Dennis Jackson and Thibault Meunier. Stateful anonymous credentials so a site can build trust with a visitor it can't identify. Three drafts: architecture, protocols, HTTP transport.
Anonymous Tokens with Hidden Metadata
With Cathie Yun. Deployed to filter spam between RCS and iMessage.
Private Proof API
Chrome's anti-fraud primitive for a web without third-party cookies. I designed it and led the implementation.
W3C Anti-Fraud Community Group
The community group I chair. Browsers, sites, and vendors working out what private anti-fraud on the web has to guarantee.
From Weakly-terminating Binary Agreement and Reliable Broadcast to Atomic Broadcast
With Andreas Fackler and Matthew Doty. The Zug consensus protocol, shipped in the Casper 2.0 node. Safety and liveness are proved in Lean 4.
CSLib
Lean's centralized computer science repository. I'm a maintainer, focused on complexity and cryptography.
complexitylib
A formalization of complexity theory in Lean 4, with no sorry.
Open Conjecture Formalizations
Lean 4 statements of open problems in mathematics and theoretical computer science.
leanlings
Learn Lean 4 by fixing seventy small exercises, one at a time.
Computable Secrets
YouTube channel on theoretical computer science. Recent videos: Shannon's 1948 paper, Kolmogorov complexity, System F, interactive proofs, the relativization barrier.