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 .