{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreidmlp3fvrhfcnepnv4d5q7edcm2st56lllt7lym5kwnfms4i5j6ty",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3moafg62ggov2"
  },
  "path": "/report/2026/098",
  "publishedAt": "2026-06-14T05:45:32.000Z",
  "site": "https://eccc.weizmann.ac.il",
  "textContent": "Modern cryptography relies on the intractability of computational problems. We present an approach to build cryptography from a new source of hardness: proving mathematical theorems.\n\nOur main result is a construction of succinct non-interactive arguments (SNARGs) for NP under standard derandomization (prBPP = prP) and cryptographic assumptions (LWE and SXDH), as well as a new, but natural assumption on the hardness of proving lower bounds in proof complexity. Specifically, our assumption states that it is impossible to prove, within a weak bounded arithmetic theory, the correctness of certifying hard tautologies against Extended Frege. This assumption is inspired by an informal mathematical challenge proposed by Razborov [Ann. Math. '15], and can be viewed as a generalization of an unconditional unprovability result due to Krají?ek and Pudlák [J. Symb. Log. '89].\n\nOur construction is, in fact, a simple variant of the SNARG constructed by Jin, Kalai, Lombardi, and Vaikuntanathan [STOC '24]. While the soundness of their construction was only proven for a subclass of NP, we prove its soundness for all NP under our assumption. At the heart of our result is the key observation that cryptographic reasoning is simple in a formal sense: the security proof of most cryptographic primitives can be formalized in a weak theory. In particular, we show how to formalize the scheme of Jin et al. in Je?ábek's theory APC? [J. Symb. Log. '07] -- a weak theory in bounded arithmetic.",
  "title": "TR26-098 |  SNARGs for NP from Unprovability of Mathematical Theorems | \n\n\tJiatu Li, \n\n\tYaoChing Hsieh, \n\n\tAbhishek Jain, \n\n\tSurya Mathialagan"
}