zkPi: Proving Lean Theorems in Zero-Knowledge

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