Mathematical Components: Documentation

• Mathematical Components by Assia Mahboubi and Enrico Tassi
• Formal Proof using Coq/SSReflect/MathComp: Start Formalization of Mathematics with Free Software by Manabu Hagiwara and Reynald Affeldt (in Japanese, 日本語)
• Programs and Proofs: Mechanizing Mathematics with Dependent Types by Ilya Sergey

• ITP 2016 tutorial: Mathematical Components, an Introduction by Yves Bertot, Cyril Cohen, Assia Mahboubi, Enrico Tassi and Laurent Théry.
• ITP 2013 tutorial: The Mathematical Components library by Assia Mahboubi and Enrico Tassi
• Introduction to Mathematical Components by Reynald Affeldt (in Japanese, 日本語)
• An introduction to small scale reflection in Coq by Georges Gonthier and Assia Mahboubi

• MathComp School 2022 by Yves Bertot, Cyril Cohen, Laurence Rideau, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry
• Coq Winter School 2018-2019 (SSReflect & MathComp) by Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
• Coq Winter School 2017-2018 (SSReflect & MathComp) by Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
• Advanced Coq Winter School 2016 for master students by Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
• Coq/SSReflect/MathComp Tutorial by Reynald Affeldt (in Japanese, 日本語)
• International Spring School on Formalization of Mathematics (MAP 2012) by Yves Bertot, Assia Mahboubi, Laurence Rideau, Pierre-Yves Strub, Enrico Tassi, Laurent Théry

• Basic cheat sheet
• Advanced cheat sheet
• ssrbool.v, ssrnat.v, bigop.v, finset.v, fingroup.v

• A Small Scale Reflection Extension for the Coq system by Georges Gonthier, Assia Mahboubi, and Enrico Tassi
  • the same htmlized as a part of Coq reference manual

Georges Gonthier about the Mathematical Components project:

• Georges Gonthier: Computer proofs: teaching computers mathematics, and conversely, ICM 2022, 2022-07-07
• Functional Encodings of Mathematics, Institut des Hautes Études Scientifiques, 2022-06-15 (in French)
• The Logic of Real Proofs, Federated Logic Conference, 2018-07-14
• Scaffolds and frames: the MathComp algebra formal library, Isaac Newton Institute, 2017-07-13
• Proof Engineering, from the Four Colour to the Odd Order Theorem, Microsoft, 2016-07-16
• Digitizing the Group Theory of the Odd Order Theorem, Institut Henri Poincaré, 2014-04-22
• the four colour theorem, RU Computer Science, 2013-01-28
• Mechanizing the Odd Order Theorem: Local Analysis, Institute for Advanced Study, 2011-01-20