Paper 2024/267
zkPi: Proving Lean Theorems in ZeroKnowledge
Abstract
Interactive theorem provers (ITPs), such as Lean and Coq, can express formal proofs for a large category of theorems, from abstract math to software correctness. Consider Alice who has a Lean proof for some public statement $T$. Alice wants to convince the world that she has such a proof, without revealing the actual proof. Perhaps the proof shows that a secret program is correct or safe, but the proof itself might leak information about the program's source code. A natural way for Alice to proceed is to construct a succinct, zeroknowledge, noninteractive argument of knowledge (zkSNARK) to prove that she has a Lean proof for the statement $T$. In this work we build zkPi, the first zkSNARKfor proofs expressed in Lean, a state of the art interactive theorem prover. With zkPi, a prover can convince a verifier that a Lean theorem is true, while revealing little else. The core problem is building an efficient zkSNARKfor dependent typing. We evaluate zkPion theorems from two core Lean libraries: stdlib and mathlib. zkPisuccessfuly proves 57.9% of the theorems in stdlib, and 14.1% of the theorems in mathlib, within 4.5 minutes per theorem. A zkPiproof is sufficiently short that Fermat could have written one in the margin of his notebook to convince the world, in zero knowledge, that he proved his famous last theorem. Interactive theorem provers (ITPs) can express virtually all systems of formal reasoning. Thus, an implemented zkSNARKfor ITP theorems generalizes practical zeroknowledge's interface beyond the status quo: circuit satisfiability and program execution.
Metadata
 Available format(s)
 Category
 Applications
 Publication info
 Preprint.
 Keywords
 ZeroknowledgeLeanVerification
 Contact author(s)

emlaufer @ cs stanford edu
aozdemir @ cs stanford edu
dabo @ cs stanford edu  History
 20240219: approved
 20240216: received
 See all versions
 Short URL
 https://ia.cr/2024/267
 License

CC BY
BibTeX
@misc{cryptoeprint:2024/267, author = {Evan Laufer and Alex Ozdemir and Dan Boneh}, title = {{zkPi}: Proving Lean Theorems in ZeroKnowledge}, howpublished = {Cryptology ePrint Archive, Paper 2024/267}, year = {2024}, note = {\url{https://eprint.iacr.org/2024/267}}, url = {https://eprint.iacr.org/2024/267} }