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 ? . 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, zero knowledge, non-interactive argument of knowledge (zkSNARK) to prove that she has a Lean proof for the statement ? . 

In this work we build zkPi, the first zkSNARK for 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 zkSNARK for dependent typing. We evaluate zkPi on theorems from two core Lean libraries: stdlib and mathlib. zkPi successfully proves 57.9% of the theorems in stdlib, and 14.1% of the theorems in mathlib, within 4.5 minutes per theorem. A zkPi proof 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 zkSNARK for ITP theorems generalizes practical zero-knowledge’s interface beyond the status quo: circuit satisfiability and program execution.

BIOS

Evan Laufer is a 5th year Ph.D. student at Stanford University advised by Prof. Dan Boneh. He primarily works on new zkSNARKs and how they can be used for novel applications. His past work includes private and verifiable explanations of inference for machine learning models, privacy-preserving energy systems, and efficient RAM abstractions for SNARKs.

Professor Boneh heads the applied cryptography group and co-direct the computer security lab. Professor Boneh's research focuses on applications of cryptography to computer security. His work includes cryptosystems with novel properties, web security, security for mobile devices, and cryptanalysis. He is the author of over a hundred publications in the field and is a Packard and Alfred P. Sloan fellow. He is a recipient of the 2014 ACM prize and the 2013 Godel prize. In 2011 Dr. Boneh received the Ishii award for industry education innovation. Professor Boneh received his Ph.D from Princeton University and joined Stanford in 1997.

Alex Ozdemir is an incoming assistant professor at Georgia Tech in the School of Cybersecurity and Privacy and a postdoctoral researcher at the Max Planck Institute for Security and Privacy. He works at the intersection of cryptography, programming languages, and formal verification. He is especially interested in cryptosystems that take a computation as an input, such zero knowledge proofs and multiparty computation. His past work includes collaborative zero-knowledge proofs, the CirC (SIR-see) compiler for programmable cryptosystems, and SMT solvers for finite fields. He got his PhD from Stanford under Clark Barrett and Dan Boneh and his undergraduate degree at Harvey Mudd.