AI for mathematics

Even and odd Dyck paths

Weight a Dyck path by its valley positions: even minus odd is the number of symmetric paths. Cigler's question, a combinatorial proof.

Open problem settled, formally verified in Lean 4

Even and odd Dyck paths

Weight a Dyck path by the sum of the positions of its valleys, its major index. Johann Cigler observed that among the paths of semilength n with k valleys, those of even weight outnumber those of odd weight by exactly the number of symmetric paths with k valleys. By an identity of Fürlinger and Hofbauer this says that the q-Narayana number N_{n,k}(q) at q = -1 counts symmetric Dyck paths. Cigler proved it algebraically and asked on MathOverflow (question 501839) for a direct combinatorial proof.

The note gives one (Theorem 1). Valley coordinates turn each path into a two-coloured Motzkin word in which the sign is a product of local signs (Lemmas 1 and 2). Swapping letters inside the first pair that has a partner is a sign-reversing involution whose fixed words all have sign +1 (Lemma 3). Halving the fixed words and reading off the last departures from each level matches them with the symmetric paths (Lemma 4). The survivors are not the symmetric paths themselves, and cannot be: for odd n and k every symmetric path has odd weight. For even n the value at q = -1 is also the half-turn case of a cyclic sieving theorem of Reiner, Stanton and White for noncrossing partitions, proved there by computing both sides.

Preprint v1, 10 October 2026, not peer reviewed and not yet independently reviewed. The whole argument, from Dyck paths written as lists of steps to Theorem 1, is formally verified in Lean 4 (lean/, standard axioms only); the identity of Fürlinger and Hofbauer is quoted, and checked by computer for n ≤ 8. The author used AI tools (Claude, Anthropic) in this work, as described in the paper’s acknowledgement, and is responsible for its content.