The Han-Xiong Integer Trace Conjecture
Han and Xiong extended the Gaussian binomial coefficient to positive rational index and conjectured that its integer trace, the integer-exponent part of the resulting power series, is coefficientwise largest at the integer point. Ono's paper proves a support-dominance theorem settling the conjecture for a large family of rational parameters and reduces the full conjecture to unit fractions, with a finite computer verification covering every remaining case up to a fixed bound.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- q-series and partitions
- Posed by
- Guo-Niu Han, Huan Xiong
- Year posed
- —
- Years open
- —
- Solved
- 2026-07-31
- Model
- AxiomProver
- Vendor
- Axiom Math
- Collaborators
- Ken Ono
- Verification
- Lean-verified
- Publication
- Preprint
- Significance
- 5 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Settles the conjecture for a large family and reduces the rest to unit fractions; the general unit-fraction case remains open.
What the AI did
The theoretical results were autonomously produced and verified in Lean by AxiomProver: the formal statements and proofs of Theorem 1.3, Corollary 1.4 and Theorem 1.5 were generated from a natural-language statement of the problem containing no proofs, then checked by the Lean proof assistant. An appendix records precisely what was and was not supplied to the system.
Verification
The main theorems were formalized and kernel-checked in Lean by the same system that produced them; the human author wrote the paper from that formal development.