math-comp.github.io/index.html at master · math-comp/math-comp.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<!-- 2025-11-13 Thu 11:09 -->
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>Mathematical Components</title>
<meta name="author" content="Reynald Affeldt" />
<meta name="generator" content="Org Mode" />
<style type="text/css">
  #content { max-width: 60em; margin: auto; }
  .title  { text-align: center;
             margin-bottom: .2em; }
  .subtitle { text-align: center;
              font-size: medium;
              font-weight: bold;
              margin-top:0; }
  .todo   { font-family: monospace; color: red; }
  .done   { font-family: monospace; color: green; }
  .priority { font-family: monospace; color: orange; }
  .tag    { background-color: #eee; font-family: monospace;
            padding: 2px; font-size: 80%; font-weight: normal; }
  .timestamp { color: #bebebe; }
  .timestamp-kwd { color: #5f9ea0; }
  .org-right  { margin-left: auto; margin-right: 0px;  text-align: right; }
  .org-left   { margin-left: 0px;  margin-right: auto; text-align: left; }
  .org-center { margin-left: auto; margin-right: auto; text-align: center; }
  .underline { text-decoration: underline; }
  #postamble p, #preamble p { font-size: 90%; margin: .2em; }
  p.verse { margin-left: 3%; }
  pre {
    border: 1px solid #e6e6e6;
    border-radius: 3px;
    background-color: #f2f2f2;
    padding: 8pt;
    font-family: monospace;
    overflow: auto;
    margin: 1.2em;
  }
  pre.src {
    position: relative;
    overflow: auto;
  }
  pre.src:before {
    display: none;
    position: absolute;
    top: -8px;
    right: 12px;
    padding: 3px;
    color: #555;
    background-color: #f2f2f299;
  }
  pre.src:hover:before { display: inline; margin-top: 14px;}
  /* Languages per Org manual */
  pre.src-asymptote:before { content: 'Asymptote'; }
  pre.src-awk:before { content: 'Awk'; }
  pre.src-authinfo::before { content: 'Authinfo'; }
  pre.src-C:before { content: 'C'; }
  /* pre.src-C++ doesn't work in CSS */
  pre.src-clojure:before { content: 'Clojure'; }
  pre.src-css:before { content: 'CSS'; }
  pre.src-D:before { content: 'D'; }
  pre.src-ditaa:before { content: 'ditaa'; }
  pre.src-dot:before { content: 'Graphviz'; }
  pre.src-calc:before { content: 'Emacs Calc'; }
  pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
  pre.src-fortran:before { content: 'Fortran'; }
  pre.src-gnuplot:before { content: 'gnuplot'; }
  pre.src-haskell:before { content: 'Haskell'; }
  pre.src-hledger:before { content: 'hledger'; }
  pre.src-java:before { content: 'Java'; }
  pre.src-js:before { content: 'Javascript'; }
  pre.src-latex:before { content: 'LaTeX'; }
  pre.src-ledger:before { content: 'Ledger'; }
  pre.src-lisp:before { content: 'Lisp'; }
  pre.src-lilypond:before { content: 'Lilypond'; }
  pre.src-lua:before { content: 'Lua'; }
  pre.src-matlab:before { content: 'MATLAB'; }
  pre.src-mscgen:before { content: 'Mscgen'; }
  pre.src-ocaml:before { content: 'Objective Caml'; }
  pre.src-octave:before { content: 'Octave'; }
  pre.src-org:before { content: 'Org mode'; }
  pre.src-oz:before { content: 'OZ'; }
  pre.src-plantuml:before { content: 'Plantuml'; }
  pre.src-processing:before { content: 'Processing.js'; }
  pre.src-python:before { content: 'Python'; }
  pre.src-R:before { content: 'R'; }
  pre.src-ruby:before { content: 'Ruby'; }
  pre.src-sass:before { content: 'Sass'; }
  pre.src-scheme:before { content: 'Scheme'; }
  pre.src-screen:before { content: 'Gnu Screen'; }
  pre.src-sed:before { content: 'Sed'; }
  pre.src-sh:before { content: 'shell'; }
  pre.src-sql:before { content: 'SQL'; }
  pre.src-sqlite:before { content: 'SQLite'; }
  /* additional languages in org.el's org-babel-load-languages alist */
  pre.src-forth:before { content: 'Forth'; }
  pre.src-io:before { content: 'IO'; }
  pre.src-J:before { content: 'J'; }
  pre.src-makefile:before { content: 'Makefile'; }
  pre.src-maxima:before { content: 'Maxima'; }
  pre.src-perl:before { content: 'Perl'; }
  pre.src-picolisp:before { content: 'Pico Lisp'; }
  pre.src-scala:before { content: 'Scala'; }
  pre.src-shell:before { content: 'Shell Script'; }
  pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
  /* additional language identifiers per "defun org-babel-execute"
       in ob-*.el */
  pre.src-cpp:before  { content: 'C++'; }
  pre.src-abc:before  { content: 'ABC'; }
  pre.src-coq:before  { content: 'Coq'; }
  pre.src-groovy:before  { content: 'Groovy'; }
  /* additional language identifiers from org-babel-shell-names in
     ob-shell.el: ob-shell is the only babel language using a lambda to put
     the execution function name together. */
  pre.src-bash:before  { content: 'bash'; }
  pre.src-csh:before  { content: 'csh'; }
  pre.src-ash:before  { content: 'ash'; }
  pre.src-dash:before  { content: 'dash'; }
  pre.src-ksh:before  { content: 'ksh'; }
  pre.src-mksh:before  { content: 'mksh'; }
  pre.src-posh:before  { content: 'posh'; }
  /* Additional Emacs modes also supported by the LaTeX listings package */
  pre.src-ada:before { content: 'Ada'; }
  pre.src-asm:before { content: 'Assembler'; }
  pre.src-caml:before { content: 'Caml'; }
  pre.src-delphi:before { content: 'Delphi'; }
  pre.src-html:before { content: 'HTML'; }
  pre.src-idl:before { content: 'IDL'; }
  pre.src-mercury:before { content: 'Mercury'; }
  pre.src-metapost:before { content: 'MetaPost'; }
  pre.src-modula-2:before { content: 'Modula-2'; }
  pre.src-pascal:before { content: 'Pascal'; }
  pre.src-ps:before { content: 'PostScript'; }
  pre.src-prolog:before { content: 'Prolog'; }
  pre.src-simula:before { content: 'Simula'; }
  pre.src-tcl:before { content: 'tcl'; }
  pre.src-tex:before { content: 'TeX'; }
  pre.src-plain-tex:before { content: 'Plain TeX'; }
  pre.src-verilog:before { content: 'Verilog'; }
  pre.src-vhdl:before { content: 'VHDL'; }
  pre.src-xml:before { content: 'XML'; }
  pre.src-nxml:before { content: 'XML'; }
  /* add a generic configuration mode; LaTeX export needs an additional
     (add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
  pre.src-conf:before { content: 'Configuration File'; }

  table { border-collapse:collapse; }
  caption.t-above { caption-side: top; }
  caption.t-bottom { caption-side: bottom; }
  td, th { vertical-align:top;  }
  th.org-right  { text-align: center;  }
  th.org-left   { text-align: center;   }
  th.org-center { text-align: center; }
  td.org-right  { text-align: right;  }
  td.org-left   { text-align: left;   }
  td.org-center { text-align: center; }
  dt { font-weight: bold; }
  .footpara { display: inline; }
  .footdef  { margin-bottom: 1em; }
  .figure { padding: 1em; }
  .figure p { text-align: center; }
  .equation-container {
    display: table;
    text-align: center;
    width: 100%;
  }
  .equation {
    vertical-align: middle;
  }
  .equation-label {
    display: table-cell;
    text-align: right;
    vertical-align: middle;
  }
  .inlinetask {
    padding: 10px;
    border: 2px solid gray;
    margin: 10px;
    background: #ffffcc;
  }
  #org-div-home-and-up
   { text-align: right; font-size: 70%; white-space: nowrap; }
  textarea { overflow-x: auto; }
  .linenr { font-size: smaller }
  .code-highlighted { background-color: #ffff00; }
  .org-info-js_info-navigation { border-style: none; }
  #org-info-js_console-label
    { font-size: 10px; font-weight: bold; white-space: nowrap; }
  .org-info-js_search-highlight
    { background-color: #ffff00; color: #000000; font-weight: bold; }
  .org-svg { }
</style>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css"> body {font-family: Arial, Helvetica; margin-left: 5em; font-size: large;} </style>
<style type="text/css"> h1 {margin-left: 0em; padding: 0px; text-align: center} </style>
<style type="text/css"> h2 {margin-left: 0em; padding: 0px; color: #580909} </style>
<style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
<style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px; }</style>
</head>
<body>
<div id="content" class="content">
<h1 class="title">Mathematical Components</h1>
<p>
 <div style="text-align:right"><img src="github-mark.png" height="25" style="border:0px">
<a href="https://github.com/math-comp/">View the Project on GitHub</a>
 <img src="github-mark.png" height="25" style="border:0px"></div>
</p>
<div id="outline-container-org380be2a" class="outline-2">
<h2 id="org380be2a">About</h2>
<div class="outline-text-2" id="text-org380be2a">
<p>
Welcome to Mathematical Components' web-page!
</p>

<p>
Mathematical Components are libraries of formalized mathematics
developed using the <a href="https://rocq-prover.org/">Rocq</a> prover. This project finds its roots
in the <a href="https://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf">formal proof of the Four Color Theorem</a>. It has been used for
large scale formalization projects, including a formal proof of the
<a href="https://inria.hal.science/hal-00816699/document">Odd Order (Feit-Thompson) Theorem</a>.
</p>

<p>
The libraries are written using the <a href="https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html">SSReflect proof language</a>, now part of
the standard distribution of the Rocq prover.
</p>

<p>
This is an open source project, licensed under the CeCILL-B free
software license agreement.
</p>
</div>
</div>
<div id="outline-container-orgdb0b575" class="outline-2">
<h2 id="orgdb0b575">Get the library</h2>
<div class="outline-text-2" id="text-orgdb0b575">
<ul class="org-ul">
<li><a href="installation.html">Installation instructions</a></li>
<li>The source code of the Mathematical Components library
can be <a href="https://github.com/math-comp/math-comp/releases">downloaded from github</a>.</li>
</ul>
</div>
</div>
<div id="outline-container-orgcf3c153" class="outline-2">
<h2 id="orgcf3c153">Documentation</h2>
<div class="outline-text-2" id="text-orgcf3c153">

<div style="float: right; width: 240px; margin: 5px 10px">
<a href="https://math-comp.github.io/mcb/"><img alt="Mathematical Components book" src="https://math-comp.github.io/mcb/cover-front-web.png" style="width: 240px" border="1px solid black"></a>
</div>

<ul class="org-ul">
<li>A <a href="https://math-comp.github.io/mcb/">book</a> that introduces the techniques for writing
algorithms and proofs and describes the design ideas of the
Mathematical Components library.</li>

<li>The library can be explored interactively and an HTML rendering of
the source code can be browsed online:
<ul class="org-ul">
<li>latest versions:
<ul class="org-ul">
<li>Version 2.5.0 (2025-10-13): <a href="htmldoc_2_5_0/libgraph.html">library graph</a>, <a href="htmldoc_2_5_0/index.html">coqdoc presentation</a></li>
<li>Version 2.4.0 (2025-04-14): <a href="htmldoc_2_4_0/libgraph.html">library graph</a>, <a href="htmldoc_2_4_0/index.html">coqdoc presentation</a></li>
<li>Version 2.3.0 (2024-11-28): <a href="htmldoc_2_3_0/libgraph.html">library graph</a>, <a href="htmldoc_2_3_0/index.html">coqdoc presentation</a></li>
<li>Version 2.2.0 (2024-01-17): <a href="htmldoc_2_2_0/libgraph.html">library graph</a>, <a href="htmldoc_2_2_0/index.html">coqdoc presentation</a></li>
</ul></li>
<li>See <a href="history.html">this page</a> for older versions.</li>
</ul></li>

<li>The SSReflect proof language comes with a dedicated reference
manual, as a <a href="https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html">chapter</a> of Rocq's reference manual.</li>

<li>Each file of the source code of the Mathematical Components library
features a documentation header which describes the concepts and
notations introduced in that file.</li>
</ul>
</div>
<div id="outline-container-org98859ce" class="outline-3">
<h3 id="org98859ce">More material</h3>
<div class="outline-text-3" id="text-org98859ce">
<ul class="org-ul">
<li>A selection of <a href="documentation.html">Books, lectures, videos, etc.</a></li>
<li><a href="papers.html">Research papers</a> using the Mathematical Components library.
Send <a href="mailto:mathcomp-dev@inria.fr?subject=MathComp%20related%20paper">us</a> a message or <a href="https://github.com/math-comp/math-comp.github.io">issue/PR on github</a> to add any paper or thesis not in this list!</li>
</ul>
</div>
</div>
</div>
<div id="outline-container-orgb757483" class="outline-2">
<h2 id="orgb757483">Help and contact</h2>
<div class="outline-text-2" id="text-orgb757483">
<ul class="org-ul">
<li>Chat with us on <a href="https://rocq-prover.zulipchat.com">Rocq's Zulip</a>! (in particular via the <code>math-comp</code> channels)</li>
<li>Discuss with us on Coq's <a href="https://coq.discourse.group/">Discourse</a> forum!</li>
<li><a href="mailto:sympa@inria.fr?subject=SUBSCRIBE%20ssreflect">Subscribe</a> to the SSReflect mailing list (low volume).
<ul class="org-ul">
<li>Browse the <a href="https://sympa.inria.fr/sympa/arc/ssreflect">archives</a> or consult the general <a href="https://sympa.inria.fr/sympa/info/ssreflect">information page</a> of the mailing list.</li>
</ul></li>
</ul>
</div>
</div>
<div id="outline-container-orgb498b31" class="outline-2">
<h2 id="orgb498b31">Authors and contributors</h2>
<div class="outline-text-2" id="text-orgb498b31">
<p>
The Mathematical Components library and the SSReflect proof language
were initially developed by the Mathematical Components team at the
<a href="https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/">Inria-Microsoft Research Joint Center</a>. Today, the list of members of
the Mathematical Components organization is visible <a href="https://github.com/orgs/math-comp/people">here</a>.
</p>
</div>
</div>
</div>
</body>
</html>