ProbXiv
sign in

The Tu-Deng Conjecture

Combinatorics · posed by Ziran Tu, Yingpu Deng, 2011 · solved

1 attempt · 1 machine check

Statement

With N=2k−1N = 2^k - 1 and wt(n)\mathrm{wt}(n) the binary Hamming weight, Tu and Deng conjectured that for every 1≤t≤N−11 \leq t \leq N-1 at most 2k−12^{k-1} pairs (a,b)(a,b) satisfy a+b≡t(modN)a + b \equiv t \pmod N and wt(a)+wt(b)<k\mathrm{wt}(a) + \mathrm{wt}(b) < k. Proved in full.

Context

A named conjecture from cryptographic Boolean function design, open since 2011 with a documented trail of partial results, well known inside that community and invisible outside it.

People

begin a project on this problem →

Attempts

1 attempt

No person has examined this. There is 1 attempt here and 1 machine check recorded against it. A machine check is a judgement recorded by a tool: no account is credited for it, nobody has put their name to it, and it is not verification by a person. Saying whether the mathematics holds is the most useful thing anybody can do on this page.

review this attempt →

  • #1

    Attempt 1

    proof attemptChatGPT 5.6 Pro with Renzhang Liu, Hengyi Luo, Tianyuan Xie ·
    AI involvement
    ai assisted
    — a person led the work and used a model along the way.
    models
    ChatGPT 5.6 Pro
    people
    Renzhang Liu, Hengyi Luo, Tianyuan Xie

    "The authors thank ChatGPT 5.6 Pro for assistance with some of the mathematical work presented in this paper. The authors subsequently verified the argument and take full responsibility for the final content." No individual step is attributed, so the lower tier applies.

    Reviews

    1 machine check

    No person has reviewed this attempt. 1 machine check below — a machine check is not human verification.

    • Machine check · not human verification

      machine: partially checked

      Recorded from Lean ·

      scope Lean formalization of the core argument; statement correspondence not independently audited

      The authors provide an accompanying Lean formalization described as an end-to-end machine-checked proof, including the intermediate results and the reduction to the original statement. Nobody independent has audited whether the formal statement faithfully expresses the conjecture, so this sits on the unaudited Lean rung.

      No ProbXiv account is credited for this check. Nobody has put their name to it, so it carries no personal accountability and does not count as verification by a person.

    Discussion of this attempt

    no comments

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.

Discussion

no comments

Nothing has been said about this problem yet.

Reading every thread is open to everyone. Posting needs an account with posting rights — sign in to check yours.