-
Notifications
You must be signed in to change notification settings - Fork 11
Expand file tree
/
Copy pathindex.org
More file actions
96 lines (71 loc) · 5.19 KB
/
Copy pathindex.org
File metadata and controls
96 lines (71 loc) · 5.19 KB
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
#+TITLE: Mathematical Components
#+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: <div style="text-align:right"><img src="github-mark.png" height="25" style="border:0px">@@
[[https://github.com/math-comp/][View the Project on GitHub]]
@@html: <img src="github-mark.png" height="25" style="border:0px"></div>@@
* About
#+BEGIN_EXPORT html
<div style="float: right; width: 240px; margin: 5px 10px">
<img alt="rocqy" src="rocqy-mathcomp.png" style="width: 240px">
</div>
#+END_EXPORT
Welcome to Mathematical Components' web-page!
Mathematical Components are libraries of formalized mathematics
developed using the [[https://rocq-prover.org/][Rocq]] prover. This project finds its roots
in the [[https://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf][formal proof of the Four Color Theorem]]. It has been used for
large scale formalization projects, including a formal proof of the
[[https://inria.hal.science/hal-00816699/document][Odd Order (Feit-Thompson) Theorem]], and extended to [[https://github.com/math-comp/analysis][mathematical analysis]].
The libraries are written using the [[https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html][SSReflect proof language]], now part of the
standard distribution of the Rocq prover. They are built thanks to
[[https://github.com/math-comp/hierarchy-builder][Hierarchy-Builder]], a Rocq plugin.
This is an open source project, licensed under the CeCILL-B free
software license agreement.
* Get the library
- [[file:installation.html][Installation instructions]]
- The source code of the Mathematical Components library
can be [[https://github.com/math-comp/math-comp/releases][downloaded from github]].
* Documentation
#+BEGIN_EXPORT html
<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>
#+END_EXPORT
- A [[https://math-comp.github.io/mcb/][book]] that introduces the techniques for writing
algorithms and proofs and describes the design ideas of the
Mathematical Components library.
- The library can be explored interactively and an HTML rendering of
the source code can be browsed online:
+ latest versions:
* Version 2.6.0 (2026-07-10): [[file:htmldoc_2_6_0/index.html][library graph]], [[file:htmldoc_2_6_0/index.html][coqdoc presentation]]
* Version 2.5.0 (2025-10-13): [[file:htmldoc_2_5_0/libgraph.html][library graph]], [[file:htmldoc_2_5_0/index.html][coqdoc presentation]]
* Version 2.4.0 (2025-04-14): [[file:htmldoc_2_4_0/libgraph.html][library graph]], [[file:htmldoc_2_4_0/index.html][coqdoc presentation]]
* Version 2.3.0 (2024-11-28): [[file:htmldoc_2_3_0/libgraph.html][library graph]], [[file:htmldoc_2_3_0/index.html][coqdoc presentation]]
+ See [[file:history.html][this page]] for older versions.
- The SSReflect proof language comes with a dedicated reference
manual, as a [[https://rocq-prover.org/doc/V9.1.0/refman/proof-engine/ssreflect-proof-language.html][chapter]] of Rocq's reference manual.
- 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.
** More material
- A selection of [[file:documentation.html][Books, lectures, videos, etc.]]
- [[file:papers.html][Research papers]] using the Mathematical Components library.
Send [[mailto:mathcomp-dev@inria.fr?subject=MathComp related paper][us]] a message or [[https://github.com/math-comp/math-comp.github.io][issue/PR on github]] to add any paper or thesis not in this list!
* Help and contact
- Chat with us on [[https://rocq-prover.zulipchat.com][Rocq's Zulip]]! (in particular via the ~math-comp~ channels)
- Discuss with us on Coq's [[https://coq.discourse.group/][Discourse]] forum!
- [[mailto:sympa@inria.fr?subject=SUBSCRIBE%20ssreflect][Subscribe]] to the SSReflect mailing list (low volume).
+ Browse the [[https://sympa.inria.fr/sympa/arc/ssreflect][archives]] or consult the general [[https://sympa.inria.fr/sympa/info/ssreflect][information page]] of the mailing list.
* Authors and contributors
The Mathematical Components library and the SSReflect proof language
were initially developed by the Mathematical Components team at the
[[https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/][Inria-Microsoft Research Joint Center]]. Today, the list of members of
the Mathematical Components organization is visible [[https://github.com/orgs/math-comp/people][here]].