Papers With

← All papers
First page of A counterexample to Tokareva's conjecture on sums of two bent functions

A counterexample to Tokareva's conjecture on sums of two bent functions

Yansong Feng, Hao Jiang, Guancheng Li, Tianyi Li, Lili Tang

math.CO Oct 23, 2026 · v1 cs.IT
formalization combinatorics cryptography
Read PDF arXiv abstract
TL;DR
The main counterexample theorems (Theorem 4.2 and Theorem 4.7) on sums of two bent functions are formally verified in Lean 4.
Abstract
It is well known that the sum of two bent functions on $\mathbb{F}^n$ has algebraic degree at most $n/2$ for even $n\ge 4$. Tokareva conjectured that the converse holds: every Boolean function with degree at most $n/2$ can be written as a sum of two bent functions. The conjecture has been verified for even $n\leq 6$ and for several special classes of Boolean functions. We disprove this conjecture by showing that $x_1x_2(x_3x_4+x_5x_6+x_7x_8)$ is not a sum of two bent functions on $\mathbb{F}^8$. We extend this construction to obtain counterexamples in every even dimension $n\ge 8$. Using Shaporenko's reduction, we also obtain explicit counterexamples to Tokareva's derivative conjecture in every even dimension $n\ge 10$.
Problem

Tokareva conjectured that for even n, every Boolean function on F_2^n of algebraic degree at most n/2 is a sum of two bent functions. The conjecture was known to hold for n ≤ 6 and for quadratic functions. A related derivative conjecture had been disproved only non-constructively.

Approach

The authors specialize the Kolomeec–Pavlov signed disagreement formula to pairs of bent functions. Combined with Parseval's identity, this gives a necessary condition: if the support of f lies in an affine subspace of dimension n−k with k < n/2, then 2^{k+1} divides wt(f). They then build degree-n/2 functions from the bent quadratic form q_3 that violate this divisibility condition. Shaporenko's reduction transfers the result to the derivative conjecture. Theorems 4.2 and 4.7 are formally verified in Lean 4.

Results

f_8 = x1x2(x3x4+x5x6+x7x8) is not a sum of two bent functions on F_2^8. The construction extends to counterexamples in every even dimension n ≥ 8, so n = 8 is the smallest dimension where the conjecture fails. Explicit counterexamples to Tokareva's derivative conjecture are also given for every even n ≥ 10.