The Tu-Deng Conjecture
With and the binary Hamming weight, Tu and Deng conjectured that for every at most pairs satisfy and . 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
- Lean proofLean formalization of the proof