{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiblxj6jxmiuoovbjkbysblgc4yro5ujk4p7poqanbqt7lgu6zuwgu",
    "uri": "at://did:plc:4rgrdigiftglskeax4wvmsev/app.bsky.feed.post/3mkmeefgxnuc2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2604.25251v1",
  "publishedAt": "2026-04-29T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Albert Atserias",
    "Moritz Müller"
  ],
  "textContent": "**Authors:** Albert Atserias, Moritz Müller\n\nWe prove that the bounded arithmetic theory $S^1_2$ is consistent with EXP $\\not\\subseteq$ P/poly. More generally, we show that certain separations of $V^1_2$ from a theory $T$ imply the consistency of $T$ with EXP $\\not\\subseteq$ P/poly. For $T=S^1_2$, Takeuti (1988) established such a separation using a variant of Gödel's consistency statement. Analogous results hold for PSPACE $\\not\\subseteq$ P/poly but the required separations of theories are yet unknown. Finally, we give magnification results for the hardness of proving almost-everywhere versions of these lower bounds.",
  "title": "From Gödel incompleteness to the consistency of circuit lower bounds"
}