{"id":"arxiv/2604.25251","url":"https://arxiv.org/abs/2604.25251","tags":["math.LO","cs.CC"],"score":0,"title":"From Gödel incompleteness to the consistency of circuit lower bounds","domain":"math.LO","source":"arxiv","authors":["Albert Atserias","Moritz Müller"],"reviews":0,"subject":"math.LO","summary":"We 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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-28","reactions":{}}