Papers With

← All papers
First page of Sparse Polynomial Divisibility Test over Finite Field is CoNP-hard

Sparse Polynomial Divisibility Test over Finite Field is CoNP-hard

Yichuan Cao, Ruichen Qiu, Qiao-Long Huang, Ruyong Feng, Xiao-Shan Gao

cs.SC Jun 10, 2026 · v1 cs.CC
formalization algebra mathlib ai-agents
Read PDF arXiv abstract Code
TL;DR
The algebraic core of the hardness proof, the Divisibility Bridge lemma over F_p, is formally verified in Lean 4 (v4.29.0) with a public repository.
Abstract
In this paper, we show that deciding whether a sparse polynomial does not divide another sparse polynomial exactly over finite fields is NP-hard under BPP many-one reductions. Equivalently, the sparse polynomial divisibility test over finite fields is CoNP-hard. This resolves the long-standing open problem concerning the computational complexity of the divisibility test for sparse polynomials in the setting of finite fields.
Problem

The computational complexity of testing whether one sparse polynomial divides another over a finite field was a long-standing open problem.

Approach

A reduction maps a sparse polynomial P over F_p to the pair f_P = P(x^p) - P(x) and g_P = (x^p - x)P(x). Then g_P divides f_P exactly when P has no root in F_p, and the bit-size blowup is polynomial. Combining this with known NP-hardness of root detection for sparse polynomials gives the result. The Divisibility Bridge lemma was formalized in Lean 4. The paper also mentions MMAT, an LLM-driven agent for proving theorems in natural language and in Lean.

Results

Sparse polynomial non-divisibility over finite fields is NP-hard under BPP many-one reductions, so divisibility testing is coNP-hard. The algebraic bridge lemma is machine-checked in Lean. The complexity-theoretic statement itself is not formalized, because Mathlib lacks a theory of NP and BPP.