Paper 2024/267
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
Metadata
- Available format(s)
-
PDF
- Category
- Applications
- Publication info
- Preprint.
- Keywords
- Zero-knowledgeLeanVerification
- Contact author(s)
-
emlaufer @ cs stanford edu
aozdemir @ cs stanford edu
dabo @ cs stanford edu - History
- 2024-02-19: approved
- 2024-02-16: 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 Zero-Knowledge}, howpublished = {Cryptology {ePrint} Archive, Paper 2024/267}, year = {2024}, url = {https://eprint.iacr.org/2024/267} }