Machine Checked Proofs and Programs in Algebraic Combinatorics (Video, CPP 2025)
Florent Hivert
(University Paris-Saclay - LISN - LMF - CNRS - Inria, France)
Abstract: We present a library of formalized results around symmetric functions and
the character theory of symmetric groups. Written in Coq/Rocq and based on
the Mathematical Components library, it covers a large part of the contents
of a graduate level textbook in the field. The flagship result is a proof of
the Littlewood-Richardson rule, which computes the structure constants of
the algebra of symmetric function in the schur basis which are integer
numbers appearing in various fields of mathematics, and which has a long
history of wrong proofs. A specific feature of algebraic combinatorics is the
constant interplay between algorithms and algebraic constructions:
algorithms are not only in computations, but also are key ingredients in
definitions and proofs. As such, the proof of the Littlewood-Richardson rule
deeply relies on the understanding of the execution of the Robinson-Schensted
algorithm. Many results in this library are effective and actually used in
computer algebra systems, and we discuss their certified implementation.
Article: https://doi.org/10.1145/3703595.3705885
Supplementary web page: https://github.com/math-comp/Coq-Combi/
ORCID: https://orcid.org/0000-0002-7531-5985
Video Tags: partitions, permutations, Young tableaux, Symmetric function, symmetric group, character theory, machine checked proofs, poplws25cppmain-p87-p, doi:10.1145/3703595.3705885, orcid:0000-0002-7531-5985
Presentation at the CPP 2025 conference, January 20-21, 2025, https://popl25.sigplan.org/home/CPP-2025
Sponsored by ACM SIGPLAN and ACM SIGLOG