The Han-Xiong Integer Trace Conjecture
Statement
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.
Record
- Source
- Added
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
AxiomProver, with Ken OnoThe record says a model found this and names the people who worked on it. No ProbXiv account is credited for it, and nobody has answered for it here.
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.
Machine-checked by Lean on #1 · not a person
lean: partially checkedLeanscope Lean formalization of the core argument; statement correspondence not independently audited
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. Tier: AxiomProver generated the formal statements and proofs from a natural-language prompt; nobody independent has audited the statement fidelity.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.