SNARGs for NP from Unprovability of Mathematical Theorems (Or: How to Use the Simplicity of Cryptographic Reasoning)
Published version: STOC 2026 (ACM Digital Library) · Full version: ePrint · ECCC
Abstract: Modern cryptography relies on the intractability of computational problems. This work presents an approach to build cryptography from a new source of hardness: proving mathematical theorems.
The primary contribution is a construction of succinct non-interactive arguments (SNARGs) for \(\textbf{NP}\) under standard derandomization (\(\textbf{prBPP}=\textbf{prP}\)) and cryptographic assumptions (LWE and SXDH), along with a new, but natural assumption on the hardness of proving lower bounds in proof complexity. This assumption states that proving the correctness of certifying hard tautologies against Extended Frege within a weak bounded arithmetic theory is impossible. The assumption draws inspiration from an informal mathematical challenge by Razborov and generalizes an unconditional unprovability result due to Krajíček and Pudlák.
The construction is a simple variant of the SNARG by Jin, Kalai, Lombardi, and Vaikuntanathan. While their original soundness proof applied only to a subclass of \(\textbf{NP}\), this work extends soundness to all \(\textbf{NP}\) under the stated assumption. A key observation is that cryptographic reasoning formalizes simply within weak theories, demonstrating how the scheme formalizes in Jeřábek’s theory \(\textbf{APC}_1\)—a weak bounded arithmetic theory.