Exponential lower bound for the bit pigeonhole principle in unrestricted resolution over parities
Any refutation of the bit pigeonhole principle in resolution over parities, a proof system whose lines are disjunctions of linear equations mod 2, must be exponentially long even with no restriction on its depth or regularity; the mathematics was produced by AI models and the main theorem is checked in Lean.
- Lab
- Independent
- Model
- GPT-6 Astra (mathematics, version 1 formalization and drafting); Claude Fable 5.1 and Claude Opus 5 (revision 1 formalization)
- Field
- Computer science
- Date
- 2026-09-15
- Human collaborators
- Kamil Braun
What was found
Resolution over parities, Res(⊕), extends resolution by letting clauses be disjunctions of affine equations over F2. Superpolynomial size lower bounds were previously known only for restricted refutations: tree-like, regular, or of bounded depth. The paper claims that every DAG-like Res(⊕) refutation of the bit pigeonhole principle with n+1 pigeons and n = 2^l holes has more than exp(n/(32768 l^2)) clauses for every l of at least 32. The argument translates a refutation into a low-degree polynomial calculus refutation over extension variables in the style of Buss, Impagliazzo, Krajicek, Pudlak, Razborov and Sgall, removes the extension variables with one substitution, and closes with a Razborov-style degree lower bound proved through the homology of chessboard complexes. The main theorem, a general sufficient condition for Res(⊕) size lower bounds, and their dependencies are formalized in Lean 4 in the author's repository.
Novelty check
The 2026-09-28 watch run surfaced this through vibemathed; this check read the paper's related-work section and searched arXiv and the web. The closest prior results found keep a restriction: Byramji and Impagliazzo (arXiv:2511.20023, November 2025) prove exponential bounds for bit pigeonhole principles only in bounded-depth Res(⊕), and the paper itself surveys regular and bounded-depth results by Efremenko, Garlík, Itsykson, Alekseev and others, each with a regularity or depth restriction. No earlier superpolynomial lower bound for unrestricted DAG-like Res(⊕) was found, which matches the abstract's framing. The year the question was first posed is not stated in the paper and is left unrecorded rather than guessed: Raz and Tzameret introduced the integer version in 2008 and Itsykson and Sokolov studied the F2 version from 2014. This was not a systematic review of the proof-complexity literature.
Caveats and known objections
The author states that he does not have the expertise to check the mathematics and did not check it, and that his confidence rests on the Lean formalization. The paper also says what that formalization does not cover: the prose, the claims about the literature, and the fidelity of the formal definitions to the standard proof system. That last point decides what the Lean is worth, and no third party has audited the Lean definitions of Res(⊕) or of the bit pigeonhole principle; there is no Palomar registration. The review rounds recorded in the repository were conversations with Claude and ChatGPT, which the author labels as not independent. Autonomy is ai-led rather than autonomous on the strictest defensible reading: the author chose the problem and steered the research loop, while his disclosure attributes all mathematical derivations to the models, with GPT-6 Astra the main contributor to version 1. A self-published claim on a well-studied problem, unrefereed and under two weeks old at entry.
Also recorded at
vibemathedsuperpolynomial-lower-bounds-for-bit-php-in-unrestricted-resolution-over-paritie
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Exponential lower bound for the bit pigeonhole principle in unrestricted resolution over parities. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-15-bit-php-resolution-over-paritiesBibTeX
@misc{whataifound-independent-2026-parities,
title = {Exponential lower bound for the bit pigeonhole principle in unrestricted resolution over parities},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Claimed. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-09-15-bit-php-resolution-over-parities}
}