Papers With

← All papers
First page of A family of symmetric counterexamples to the bent sum decomposition conjecture

A family of symmetric counterexamples to the bent sum decomposition conjecture

Máté Róbert Kepes, Anita Kercsó-Molnár, András Viczián

math.CO Nov 4, 2026 · v3
formalization mathlib combinatorics cryptography
Read PDF arXiv abstract Code
TL;DR
The main theorem and the bentness of an explicit eight-variable function are formally verified in Lean 4 with Mathlib, with an accompanying repository.
Abstract
In this paper, we provide an infinite family of counterexamples to Tokareva's conjecture on sums of two bent functions. The conjecture states that every Boolean function in an even number of variables $n$ of algebraic degree at most $n/2$ can be written as the sum of two bent functions. We show that for every $n=2^k\geq 8$, the symmetric function $F_n=1+σ_2+σ_4+σ_6+\cdots+σ_{n/2}$ has degree $n/2$ and cannot be written as a sum of at most two bent functions. Here $σ_j$ is the elementary symmetric Boolean polynomial of degree $j$. Furthermore, we show that the eight-variable member of this family can be represented as the sum of exactly three bent functions. Using the connection between bent-sum decompositions and derivatives of bent functions, we also obtain an infinite family of balanced Boolean functions that cannot be derivatives of bent functions.
Problem

Tokareva conjectured that every Boolean function in an even number n of variables with algebraic degree at most n/2 is the sum of two bent functions. The question is whether this degree condition is actually sufficient.

Approach

For n=2^k≥8 the symmetric function F_n=1+σ_2+σ_4+…+σ_{n/2} is considered, and its support is computed as a disjoint union of two Hamming balls. Counting arguments on this support yield an orthogonality condition and an affine restriction on any hypothetical bent summand, which contradict the possible weights of bent functions. For n=8, an explicit three-bent decomposition is built from Maiorana–McFarland functions. The main theorem and the bentness of the remaining summand are verified in Lean 4 using Mathlib.

Results

F_n has degree n/2 but is not a sum of at most two bent functions, which disproves the conjecture for every n=2^k≥8. F_8 needs exactly three bent summands. As consequences, the paper gives an infinite family of balanced functions that are not derivatives of bent functions, a nonlinearity-loss bound, and restrictions on certain cryptographic constructions.