TOPICS
Search

Bit Pigeonhole Principle

The bit pigeonhole principle is a family of sentential formulas in propositional calculus encoding the assertion that m>n pigeons cannot be injected into n holes. When n=2^l, each pigeon is represented by l Boolean variables, and the clauses assert that every pair of pigeons differs in at least one bit.

The resolution principle extended to parities, denoted Res( direct sum ), permits clauses that are disjunctions of affine equations over the finite field F_2. Braun (2026) reported that, for l>=32 and n=2^l, the bit pigeonhole formula BPHP_(n+1)^n requires more than

exp(n/(32768l^2))

nodes in every unrestricted acyclic digraph (DAG)-like Res( direct sum ) refutation. In particular, this gives the lower bound 2^(Omega(n/ln^2n)), which is superpolynomial in n.

Braun (2026) credits GPT-6 Astra and Claude Fable 5.1 with the principal mathematical and formalization work. The paper supplies pinned Lean sources and reports fresh-kernel replays of the aggregate formalization. Braun states that he lacks the expertise to check the mathematics himself. The fidelity of the formal definitions to the standard proof system and the novelty claims lie outside the Lean verification. Independent specialist review had not been reported as of Sep. 23, 2026.

See also

Dirichlet's Box Principle, Finite Field, Resolution Principle

Explore with Wolfram|Alpha

References

Braun, K. "An Exponential Lower Bound for the Bit Pigeonhole Principle in Resolution over Parities." 19 Sep 2026. https://arxiv.org/abs/2609.23015.Itsykson, D. and Sokolov, D. "Resolution over Linear Equations Modulo Two." Ann. Pure Appl. Logic 171, 102722, 2020. https://doi.org/10.1016/j.apal.2019.102722.

Cite this as:

Weisstein, Eric W. "Bit Pigeonhole Principle." From MathWorld--A Wolfram Resource. https://mathworld.wolfram.com/BitPigeonholePrinciple.html

Subject classifications