Machine Checked Proofs and Programs in Algebraic Combinatorics

TL;DR

This paper introduces a formalized library in Coq for algebraic combinatorics, including a machine-verified proof of the Littlewood-Richardson rule, integrating algorithms and algebraic proofs with certified implementations.

Contribution

It provides a comprehensive formalization of symmetric functions and character theory, with a verified proof of the Littlewood-Richardson rule, bridging algorithms and algebraic proofs.

Findings

Verified proof of Littlewood-Richardson rule

Formalization of symmetric functions in Coq

Effective algorithms used in computer algebra systems

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.