Machine Checked Proofs and Programs in Algebraic Combinatorics

Watch this 30-minute conference talk from CPP 2025 where Florent Hivert presents a library of formalized results in algebraic combinatorics. Explore how the Coq/Rocq implementation, based on the Mathematical Components library, covers graduate-level content on symmetric functions and character theory of symmetric groups. Learn about the proof of the Littlewood-Richardson rule, which computes structure constants in the algebra of symmetric functions—a result with historical significance due to previous incorrect proofs. Discover how algorithms like Robinson-Schensted are not just computational tools but essential components of definitions and proofs in this field. The presentation demonstrates how these effective results are implemented in certified computer algebra systems, bridging theoretical mathematics and practical computation. Access supplementary materials through the GitHub repository for deeper exploration of this work from University Paris-Saclay.