{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreicf2nclpkhnsinns24uho2igvmglnxr6repctoe4253btwsytton4",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mkrr7ntsuq62"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2604.28172v1",
  "publishedAt": "2026-05-01T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Susanna F. de Rezende",
    "David Engström",
    "Yassine Ghannane",
    "Kilian Risse"
  ],
  "textContent": "**Authors:** Susanna F. de Rezende, David Engström, Yassine Ghannane, Kilian Risse\n\nWe prove superpolynomial length lower bounds for the semantic tree-like Frege refutation system with bounded line size. Concretely, for any function $n^{2-\\varepsilon} \\leq s(n) \\leq 2^{n^{1-\\varepsilon}}$ we exhibit an explicit family $\\mathcal{A}$ of $n$-variate CNF formulas $A$, each of size $|A| \\le s(n)^{1+\\varepsilon}$, such that if $A$ is chosen uniformly from $\\mathcal{A}$, then asymptotically almost surely any tree-like Frege refutation of $A$ in line-size $s(n)$ is of length super-polynomial in $|A|$. Our lower bounds apply also to tree-like degree-$d$ threshold systems, for $d \\approx \\log\\bigl(s(n)\\bigr)$, that is, for $d$ up to $n^{1-\\varepsilon}$. More generally, our lower bounds apply to the semantic version of these systems and to any semantic tree-like proof system where the number of distinct lines is bounded by $\\exp\\bigl(s(n)\\bigr)$.",
  "title": "Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size"
}