Machine Checked Proofs and Programs in Algebraic Combinatorics
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912147118751744 |
|---|---|
| author | Hivert, Florent |
| author_facet | Hivert, Florent |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_04864 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Machine Checked Proofs and Programs in Algebraic Combinatorics Hivert, Florent Combinatorics Group Theory Representation Theory 05E05, 05E10, 68V15, 68W30 F.3.1; G.2.1; G.4; I.1.2 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. |
| title | Machine Checked Proofs and Programs in Algebraic Combinatorics |
| topic | Combinatorics Group Theory Representation Theory 05E05, 05E10, 68V15, 68W30 F.3.1; G.2.1; G.4; I.1.2 |
| url | https://arxiv.org/abs/2412.04864 |