documentation.org

#+TITLE: Mathematical Components: Documentation
#+OPTIONS: toc:nil
#+OPTIONS: ^:nil
#+OPTIONS: html-postamble:nil
#+OPTIONS: num:nil
#+HTML_HEAD: <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
#+HTML_HEAD: <style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
#+HTML_HEAD: <style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
#+HTML_HEAD: <style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
#+HTML_HEAD: <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
#+HTML_HEAD: <style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px; }</style>

* @@html:&#128218;@@ Books
- [[https://math-comp.github.io/mcb/][Mathematical Components]] by Assia Mahboubi and Enrico Tassi
- [[https://www.morikita.co.jp/books/book/3287][Formal Proof using Coq/SSReflect/MathComp: Start Formalization of Mathematics with Free Software]] by Manabu Hagiwara and Reynald Affeldt (in Japanese, 日本語)
- [[http://ilyasergey.net/pnp/][Programs and Proofs: Mechanizing Mathematics with Dependent Types]] by Ilya Sergey
- [[https://staff.aist.go.jp/reynald.affeldt/documents/karate-rocq.pdf][Karate-Rocq, An Introduction to MathComp-Analysis]] by Reynald Affeldt
* @@html: &#128210;@@ SSReflect reference manual
- [[https://hal.inria.fr/inria-00258384/en][A Small Scale Reflection Extension for the Coq system]] by Georges Gonthier, Assia Mahboubi, and Enrico Tassi
  + the same [[https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html][htmlized as a part]] of Coq reference manual

* @@html: &#x1F3EB;@@ Lectures


** Introductions

- @@html:&#127909;@@ [[https://www.youtube.com/watch?app=desktop&v=taqk6tty8wk][Coq/Rocq tutorial: Ssreflect tactics and the MathComp library]] by Marie Kerjean and Cyril Cohen, 2024-03-26
- [[https://github.com/math-comp/math-comp/wiki/tutorial-itp2016][ITP 2016 tutorial: Mathematical Components, an Introduction]] by Yves Bertot, Cyril Cohen, Assia Mahboubi, Enrico Tassi, and Laurent Théry.
- [[https://www.jstage.jst.go.jp/article/jssst/34/2/34_2_64/_pdf][Introduction to Mathematical Components]] by Reynald Affeldt (in Japanese, 日本語), 2016
- [[http://videos.rennes.inria.fr/Conference-ITP/indexAssiaMahboubiEnricoTassi.html][ITP 2013 tutorial: The Mathematical Components library]] by Assia Mahboubi and Enrico Tassi
- [[http://jfr.unibo.it/article/view/1979][An introduction to small scale reflection in Coq]] by Georges Gonthier and Assia Mahboubi, 2010

** Class

- [[https://mathcomp-schools.gitlabpages.inria.fr/2022-12-school/school][MathComp School 2022]] by Yves Bertot, Cyril Cohen, Laurence Rideau, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry
- [[https://team.inria.fr/marelle/en/coq-winter-school-2018-2019-ssreflect-mathcomp/][Coq Winter School 2018-2019 (SSReflect & MathComp)]] by Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
- [[https://team.inria.fr/marelle/en/coq-winter-school-2017-2018-ssreflect-mathcomp/][Coq Winter School 2017-2018 (SSReflect & MathComp)]] by Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
- [[https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016/][Advanced Coq Winter School 2016 for master students]] by Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
- [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/][Coq/SSReflect/MathComp Tutorial]] by Reynald Affeldt (in Japanese, 日本語), 2014-2015
- [[http://www-sop.inria.fr/manifestations/MapSpringSchool/][International Spring School on Formalization of Mathematics (MAP 2012)]] by Yves Bertot, Assia Mahboubi, Laurence Rideau, Pierre-Yves Strub, Enrico Tassi, Laurent Théry

* @@html:&#128221;@@ Cheatsheets
- [[http://www-sop.inria.fr/marelle/math-comp-tut-16/MathCompWS/basic-cheatsheet.pdf][Basic cheat sheet]]
- [[http://www-sop.inria.fr/marelle/math-comp-tut-16/MathCompWS/cheatsheet.pdf][Advanced cheat sheet]]
- [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/ssrbool_doc.pdf][ssrbool.v]],
  [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/ssrnat_doc.pdf][ssrnat.v]],
  [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/bigop_doc.pdf][bigop.v]],
  [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/finset_doc.pdf][finset.v]],
  [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/fingroup_doc.pdf][fingroup.v]]

* @@html:&#127909;@@ Conference videos
- [[https://www.youtube.com/watch?v=v5hNHr7CF3Q][An Overview of MathComp-Analysis and Its Applications]] by Reynald Affeldt at the Rocqshop 2025
- [[https://www.youtube.com/watch?v=NJetR3C6uH8][Building Measure Theory using Hierarchy Builder]] by Cyril Cohen at the Hausdorff Center for Mathematics, 2024

** Georges Gonthier about the Mathematical Components project:
- [[https://www.youtube.com/watch?v=3ak3N31d8_g][Georges Gonthier: Computer proofs: teaching computers mathematics, and conversely]], ICM 2022, 2022-07-07
- [[https://www.youtube.com/watch?v=ZNB2ZEFw5Zw][Functional Encodings of Mathematics]], Institut des Hautes Études Scientifiques, 2022-06-15 (in French)
- [[https://www.youtube.com/watch?v=_NDD_jXGwk8][The Logic of Real Proofs]], Federated Logic Conference, 2018-07-14
- [[https://www.newton.ac.uk/seminar/17967/][Scaffolds and frames: the MathComp algebra formal library]], Isaac Newton Institute, 2017-07-13
- [[https://www.microsoft.com/en-us/research/video/proof-engineering-from-the-four-colour-to-the-odd-order-theorem/][Proof Engineering, from the Four Colour to the Odd Order Theorem]], Microsoft, 2016-07-16
- [[https://www.youtube.com/watch?v=frz6MFt36Gc][Digitizing the Group Theory of the Odd Order Theorem]], Institut Henri Poincaré, 2014-04-22
- [[https://www.youtube.com/watch?v=yBXGdJw1xBI][The four colour theorem]], RU Computer Science, 2013-01-28
- [[https://www.youtube.com/watch?v=TczaUx0B92M][Mechanizing the Odd Order Theorem: Local Analysis]], Institute for Advanced Study, 2011-01-20