formal-conjectures · paper · ams-5 · ams-11 · ams-94
**The Tu-Deng conjecture.** For $k \ge 2$ and a nonzero residue $t$ modulo $2^k - 1$, there
are at most $2^{k-1}$ pairs of residues $(a, b)$ with $a + b = t$ whose binary weights
(of their representatives in $0, \dots, 2^k - 2$) sum to at most $k - 1$.
Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).
Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://doi.org/10.1007/s10623-010-9413-9
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://eprint.iacr.org/2009/272
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Paper/TuDengConjecture.lean
Local target: Corpus.PaperTuDengConjecture.tu_deng_conjecture
Source SHA-256: 38617b0c53a8afbe996ef5cd98295c00680fe9c48aa55dfbcefe3ed64c053791
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
**The Tu-Deng conjecture.** For $k \ge 2$ and a nonzero residue $t$ modulo $2^k - 1$, there are at most $2^{k-1}$ pairs of residues $(a, b)$ with $a + b = t$ whose binary weights (of their representatives in $0, \dots, 2^k - 2$) sum to at most $k - 1$.
No public records on this page.
No public records on this page.