# Mathematical Components: Documentation

## Books

- Programs and Proofs: Mechanizing Mathematics with Dependent Types by Ilya Sergey
- 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, 日本語)

## Introductions

- An introduction to small scale reflection in Coq by Georges Gonthier and Assia Mahboubi
- ITP 2013 tutorial: The Mathematical Components library by Assia Mahboubi and Enrico Tassi
- 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, 日本語)

## Lectures

- International Spring School on Formalization of Mathematics (MAP 2012) by Yves Bertot, Assia Mahboubi, Laurence Rideau, Pierre-Yves Strub, Enrico Tassi, Laurent Théry
- Coq/SSReflect/MathComp Tutorial by Reynald Affeldt (in Japanese, 日本語)
- Advanced Coq Winter School 2016 for master students by 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 and Laurent Théry
- Coq Winter School 2018-2019 (SSReflect & MathComp) by Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi and Laurent Théry

## Cheatsheets

## 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

## Conference videos

Georges Gonthier about the Mathematical Components project:

- Mechanizing the Odd Order Theorem: Local Analysis, Institute for Advanced Study, 2011-01-20
- the four colour theorem, RU Computer Science, 2013-01-28
- Digitizing the Group Theory of the Odd Order Theorem, Institut Henri Poincaré, 2014-04-22
- Proof Engineering, from the Four Colour to the Odd Order Theorem, Microsoft, 2016-07-16
- Scaffolds and frames: the MathComp algebra formal library, Isaac Newton Institute, 2017-07-13
- The Logic of Real Proofs, Federated Logic Conference, 2018-07-14