Mathematical Components: Documentation
📚 Books
- 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
📒 SSReflect reference manual
- 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
🏫 Lectures
Introductions
- 🎥 Coq/Rocq tutorial: Ssreflect tactics and the MathComp library by Marie Kerjean and Cyril Cohen, 2024-03-26
- ITP 2016 tutorial: Mathematical Components, an Introduction by Yves Bertot, Cyril Cohen, Assia Mahboubi, Enrico Tassi, and Laurent Théry.
- Introduction to Mathematical Components by Reynald Affeldt (in Japanese, 日本語), 2016
- ITP 2013 tutorial: The Mathematical Components library by Assia Mahboubi and Enrico Tassi
- An introduction to small scale reflection in Coq by Georges Gonthier and Assia Mahboubi, 2010
Class
- 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, 日本語), 2014-2015
- International Spring School on Formalization of Mathematics (MAP 2012) by Yves Bertot, Assia Mahboubi, Laurence Rideau, Pierre-Yves Strub, Enrico Tassi, Laurent Théry
📝 Cheatsheets
🎥 Conference videos
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