Paper 2026/1687 Original: eprint.iacr.org/2026/1687 ↗

Theoretical Open Problems in Symmetric Cryptography: Verifiable LLM-Guided Analysis

Abstract

We present the Pilot--Sailor Framework, an LLM-guided system for studying theoretical open problems in symmetric cryptography. Pilot proposes intermediate statements and proof plans. Sailor attempts formal proofs, and the proof assistant admits only checked declarations to the verified context. We apply this methodology to Boolean-function theory and symmetric cryptanalysis through fourteen mathematical case studies, comprising complete resolutions, corrected formulations, counterexamples, and scoped quantitative advances. In particular, we prove the original pointwise Tu--Deng conjecture for all word lengths and admissible residues. We further characterize equality in this bound: if \(t\) has \(z\) zero bits, equality holds exactly when every cyclic gap between consecutive zeros is at least \(z\). This criterion also gives a closed formula for the number of equality cases for each \(z\). We also prove that, for \(n=2k\geq6\) and \(k<m<2k\), every mapping \(F:\mathbb F_2^n\to\mathbb F_2^m\) satisfies \(\operatorname{NL}(F)\leq2^{n-1}-2^{n/2-1}-2\). This improves both the covering-radius estimate and the bound obtained from Nyberg's obstruction and integrality. Using an exact computer-assisted spectral classification, we also prove that the maximum nonlinearity of a balanced Boolean function in eight variables is 116, resolving whether the value 118 can occur. Beyond the well-known long-standing problems highlighted above, we also establish new results for ten further research questions in symmetric cryptography.