Record Compositions of Alternating Permutations
Statement
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.
Record
- Source
- Added
Comments
No person has examined this. Nothing here has been checked at all. say whether it holds →
proof attempt · #1
AxiomProver, with Evan Chen, Ken Ono and Michal MogielnickiThe 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 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.
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.