Mathematical Components: Documentation
Mathematical Components: Documentation
📒 SSReflect reference manual
🏫 Lectures
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
🎥 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
