(2026-08) Theoretical Open Problems in Symmetric Cryptography; Verifiable LLM-Guided Analysis
2026-08-14
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