Record Compositions of Alternating Permutations
Amdeberhan, Shareshian and Stanley showed a function from the theory of partition Eisenstein series counts alternating permutations with a given record partition, and asked whether a similar theory exists for record compositions, suggesting a role for noncommutative symmetric functions. The paper solves that open problem with a product formula.
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Enumerative Combinatorics, Symmetric Functions
- Posed by
- Amdeberhan, Shareshian and Stanley
- Year posed
- 2026
- Years open
- 0y
- Solved
- 2026-07-14
- Model
- AxiomProver
- Vendor
- Axiom Math
- Collaborators
- Evan Chen, Ken Ono, Michal Mogielnicki
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 20 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
The paper states that AxiomProver autonomously produced and verified the results in Lean, and devotes a section to the protocol, the formal files and the verification environment.
Verification
The paper reports an accompanying Lean/Mathlib formalization produced autonomously by AxiomProver, described in its own section. Not rebuilt here, and not independently reviewed. Preprint, not refereed.
Sources
- PaperarXiv
- Lean proofGithub link to the proof in Lean
- Lean statementGitHub link to the problem statement in Lean
- Problem recordAmdeberhan et al 2026 - Problem statement