VibeMathedMath problems solved by AI

The Tu-Deng Conjecture

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

Result
Proved
Status
Resolved
AI contribution
AI-assisted
Method
Argument
Field
Boolean functions; combinatorial number theory
Posed by
Ziran Tu, Yingpu Deng
Year posed
2011
Years open
15y
Solved
2026-07-30
Model
ChatGPT 5.6 Pro
Vendor
OpenAI
Collaborators
Renzhang Liu, Hengyi Luo, Tianyuan Xie
Verification
Lean-checked, statement unaudited
Publication
Preprint
Significance
15 / 100
Disclosed cost
Wikipedia
No dedicated article

What the AI did

"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.

Verification

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.

Sources

arXiv

Discussion