{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreih6p3wy42eq4ptgcaqvkhrugvvoz5x46derbwb5amjtghz42t6a3q",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mliagkt7vlz2"
  },
  "path": "/report/2026/070",
  "publishedAt": "2026-05-10T04:44:48.000Z",
  "site": "https://eccc.weizmann.ac.il",
  "textContent": "Since the introduction of the Ideal Proof System (IPS) by Grochow and Pitassi (J. ACM 2018), a substantial body of work has established size lower bounds for IPS and its fragments. In particular, Forbes, Shpilka, Tzameret, and Wigderson (Theory Comput. 2021) developed the main lower-bound frameworks for restricted IPS fragments, namely functional lower bounds and the hard multiples method, while Alekseev, Grigoriev, Hirsch, and Tzameret (SIAM J.Comput. 2024) gave a general template for conditional lower bounds for full IPS. Yet all these lower bounds apply only to purely algebraic formulas over a field, that is, non-Boolean formulas not directly expressible in propositional logic. Proving lower bounds for CNF formulas has therefore remained a central open problem in this line of work. The current work resolves this question for IPS over read-once oblivious algebraic branching programs (roABPs) by proving lower bounds for refutations of CNF formulas in this system. Our approach is a rank-based feasible interpolation argument, following the method of Pudlak and Sgall (Proof Complexity and Feasible Arithmetic 1996) for monotone span programs, in which decomposing a given roABP refutation along a variable partition yields a low-dimensional space of polynomials from which we construct a span-program interpolant. We extend their result from Nullstellensatz refutations measured by degree to Nullstellensatz refutations measured by roABP size (i.e., roABP-IPS$_{LIN}$).",
  "title": "TR26-070 |  Hard CNF Instances for Ideal Proof Systems | \n\n\tTuomas Hakoniemi , \n\n\tNutan Limaye, \n\n\tIddo  Tzameret"
}