Welcome to the resource topic for 2024/267
Title:
zkPi: Proving Lean Theorems in Zero-Knowledge
Authors: Evan Laufer, Alex Ozdemir, Dan Boneh
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.
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 zero-knowledge’s interface beyond the status quo:
circuit satisfiability and program execution.
ePrint: https://eprint.iacr.org/2024/267
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .