AIProofWatch
← Archive
Importance: notable
VerificationAuthor claimAccessible artifact / proof
improved boundai assisted

AI-assisted lower bound for resolution over parities

Braun reports more than exp(n/(32768ℓ²)) clauses for DAG-like Res(⊕) refutations of the bit pigeonhole principle, for n=2^ℓ and ℓ≥32, without depth or regularity restrictions.

Sources for this record

What was already known

Earlier superpolynomial lower bounds addressed restricted refutations.

What changed and why it matters

Advances the stated target relative to the recorded baseline.

The AI contribution

The paper explicitly describes substantial AI assistance in proof development and a linked Lean formalization.

Limitations

Preprint. The author states limits to his ability to check the mathematics; formal-to-informal correspondence and literature claims remain outside the reported Lean checking. This does not resolve P versus NP.

Verification evidence

Evidence labels show what supports the claim. Importance rates its impact if correct.

Author claim

The original source reports this scoped result; AIProofWatch reviewed its statement, not the full proof.

Accessible artifact / proof

A research manuscript or proof artifact is publicly accessible; availability is not independent checking.

Correction and publication history