Edited by ZKPunk
Highlights
A GKR Tutorial
In this tutorial, Vitalik Buterin provides a comprehensive and intuitive explanation of the GKR (Goldwasser–Kalai–Rothblum) protocol, a highly efficient interactive proof system widely used in zero-knowledge (ZK) proving systems. GKR is particularly well-suited for computations that are large in two dimensions: layered and batched, such as Poseidon hash functions and LLM inference. Its key advantage lies in avoiding commitments to intermediate layers—only the inputs and outputs need to be committed—drastically reducing computational overhead.
The article walks through the core building block of GKR: the sumcheck protocol, which recursively reduces a claim about a large computation to a claim about a single point evaluation. Using a simplified version of the Poseidon2 hash function, Vitalik demonstrates how GKR works by reversing the computation layer by layer, applying sumchecks at each step.
Several optimizations are discussed, including reducing the number of values per round from 5 to 3 using Gruen’s trick, and batching linear sumchecks. These techniques enable GKR to achieve single-digit overhead in practice, compared to ~100x overhead in traditional STARKs.
Vitalik also touches on polynomial commitment schemes and security considerations, such as Fiat–Shamir soundness. He concludes that while GKR is not zero-knowledge by itself, it is a powerful and general-purpose proving engine that can be wrapped in ZK-SNARKs or STARKs and applied to a wide range of computations beyond hashing, including machine learning inference.
本文由 Vitalik Buterin 撰写，深入浅出地介绍了 GKR（Goldwasser–Kalai–Rothblum）协议，这是一种高效的交互式证明系统，广泛应用于零知识证明（ZK）领域，尤其适用于大规模、分层、批处理的计算任务，如 Poseidon 哈希和 LLM 推理。GKR 的核心优势在于它避免了对中间层的承诺，只需对输入和输出进行承诺，从而显著降低了计算和存储开销。
文章详细讲解了 GKR 的关键构件——sumcheck 协议，并通过简化的 Poseidon2 哈希函数示例，展示了如何逐层「反向」验证计算过程。文中还介绍了多项优化技巧，如 Gruen’s trick 和批量 sumcheck，使得 GKR 在实际应用中可实现个位数的证明开销。
最后，Vitalik 强调 GKR 并非零知识协议本身，但可作为高效的证明引擎嵌入到 ZK-SNARK/STARK 中，适用于哈希、神经网络推理等多种计算场景。
Kevin Lacker on AI-Assisted Theorem Proving and Acorn
In this episode, Anna Rose and Guillermo Angeris talk with Kevin Lacker, creator of Acorn, a theorem prover utilising AI. They explore what theorem provers are, their history, and how they’re used today. Kevin shares how Acorn brings in AI to simplify the proving process, letting users naturally write mathematical statements while the system checks the correctness of those statements. It’s built to feel more like natural math, unlike tools like Lean that demand every step.
They also explore the benefits of including AI in math, and also the challenges that come with it such as hallucinations, and how Acorn could speed up research in areas like zero-knowledge proofs. The dicussion also covers the history of mathematics, community building around Acorn and its open math library, acornlib.
在本期节目中，主持人 Anna Rose 和 Guillermo Angeris 与 Acorn（一款利用 AI 的定理证明器）的创始人 Kevin Lacker 进行了对话。
他们探讨了定理证明器的概念、历史以及如今的应用。Kevin 分享了 Acorn 如何引入 AI 来简化证明过程，让用户能够自然地编写数学语句，同时系统会检查这些语句的正确性。Acorn 的设计理念更接近自然数学，不像 Lean 等要求用户每一步都参与的工具。
他们还探讨了将人工智能融入数学的益处，以及随之而来的挑战（例如幻觉），以及 Acorn 如何加速 ZK 等领域的研究。讨论还涵盖了数学的历史、围绕 Acorn 及其开放数学库 acornlib 的社区建设。
Proposal: OP_STARK_VERIFY - Native STARK Proof Verification in Bitcoin Script
This post proposes adding an opcode, OP_STARK_VERIFY, to Tapscript that verifies a bounded-size STARK proof. The goal is to enable on-chain verification of a Zero Knowledge Proof with transparent, post-quantum-secure assumptions, without resorting to ad-hoc Script encodings (e.g., OP_CAT) or enshrining a large family of arithmetic opcodes. We outline the motivation, threat model, bounding/pricing approach, initial opcode semantics, and open questions. Feedback welcome on scope, parameter bounding, pricing, alternatives, and challenges.
It is clear that this proposal is far from being fully fleshed, and presents already multiple significant challenges, the main one being about credible neutrality with respect to the need of choosing a specific flavor of STARK protocol.
The main goal is to gauge the interest about enshrining native ZK verification (i.e OP_STARK_VERIFY, OP_GROTH16_VERIFY) into Bitcoin at some point.
It’s also an interesting thought experiment to start thinking about the challenges that this would imply.
本提案旨在为 Tapscript 引入一个新的操作码 OP_STARK_VERIFY，用于验证特定大小范围内的 STARK 证明。其核心目标，是实现零知识证明的链上验证——该证明需具备透明的、后量子安全的假设前提，同时避免依赖特定的脚本编码方式（例如 OP_CAT），或直接内嵌一整套复杂的算术操作码族。
本文阐述了其动机、威胁模型、范围界定与定价方法、操作码的初步语义以及尚待解决的问题。此提案远未完善，且已面临多项重大挑战。其中最主要的，在于如何确保「可信中立性」——即，如何避免在必须选择某一具体 STARK 协议变体时，产生偏袒之嫌。
此项探讨的首要目的，是试探社区在将来某个时点，将原生零知识验证功能（例如 OP_STARK_VERIFY、OP_GROTH16_VERIFY）直接嵌入比特币协议这一构想上的兴趣程度。同时，它亦是一个引人入胜的思想实验，促使我们开始审慎思考，实现此目标所必将伴随的种种挑战。
Updates
Lecture notes for Chris Peikert's graduate-level Theory of Cryptography course
These are lecture notes from his graduate-level Theory of Cryptography course taught at Georgia Tech and University of Michigan.
Feedback (or even better, pull requests) welcome!
这是他在佐治亚理工学院和密歇根大学教授的研究生密码学理论课程的讲义。
COMS 4281: Introduction to Quantum Computing
This class is an introduction to the theory of quantum computing and quantum information. Topics covered include:
- The fundamental postulates of quantum information theory
- Entanglement and nonlocality
- The quantum circuit model
- Basic quantum protocols, such as quantum teleportation and superdense coding
- Basic quantum algorithms, such as Simons’ algorithm, the Quantum Fourier Transform, Phase Estimation, Shor’s Factoring algorithm, Grover search, amplitude amplification
- Quantum error correction and fault-tolerance
The goal of the course is to provide a rigorous foundation for future research/studies in quantum computing and quantum information, and along the way provide students with an understanding of the state of the field, and where it’s headed.
No background in quantum physics is required. However, having familiarity and comfort with abstract linear algebra is a must.
本课程旨在系统介绍量子计算与量子信息的基础理论，涵盖以下核心内容：
- 量子信息理论的基本公设
- 量子纠缠与非定域性
- 量子电路模型
- 基础量子协议，如量子隐形传态与超密编码
- 核心量子算法，包括西蒙算法、量子傅里叶变换、相位估计、肖尔质因数分解算法、格罗弗搜索及振幅放大
- 量子纠错与容错计算
课程目标是为后续的量子计算与信息研究奠定严谨的理论根基，并引导学生深入理解该领域的现状与未来发展方向。
修读本课程无需具备量子物理背景，但学生必须熟练掌握并善于运用抽象线性代数知识
CIS 7000: Succinct Arguments
In this course, we will cover the mathematical foundations, implementation aspects, and applications of zkSNARKs.
This course requires a basic background in discrete mathematics (at the level of CIS 1600), and a basic background in algorithms and complexity (at the level of CIS 3200).
本课程将系统讲解 zkSNARK 的数学基础、实现技术及其应用领域。
学生需具备离散数学（达到 CIS 1600 课程水平）及算法与复杂度（达到 CIS 3200 课程水平）的基础知识。
Papers
Q4 2025 Paper Reading List (Curated by KurtPan@ZKPunk)
- https://snark.express/25q4.pdf
If you’d like to receive updates via email, subscribe us!