Machine Checked Proofs and Programs in Algebraic Combinatorics

on YouTube ↗30m

" summary

A Coq/Mathematical Components library formalizes symmetric functions and character theory, delivering a proof of the Littlewood-Richardson rule by symbolically executing the Robinson–Schensted algorithm and longest-increasing-subsequence construction. The work uses Coq/MathComp library with small-scale reflection, yields a certified implementation that computes LR coefficients as positive integers (examples up to a few thousand), required about six months of effort, formalizes roughly 5% of SageMath’s symmetric-function code, and demonstrates the construction and verified execution of the algorithms.

AI-written summary · about

" chapters (10)

1. 0:00Machine checked proofs in combinatorics
2. 1:29Library overview
3. 3:37Symmetric polynomials and partitions
4. 8:20Littlewood-Richardson rule history
5. 10:26Littlewood-Richardson coefficients
6. 13:12Young tableaux and Schur functions
7. 16:04Main theorem and proof
8. 17:53Longest increasing subsequence
9. 21:34Character theory of symmetric groups
10. 22:40Conclusion and challenges