Gaia

Implementation of books from N. Bourbaki's Elements of Mathematics in Coq using the Mathematical Components library, including set theory and number theory.

Meta

• Author(s):
  • José Grimm
  • Alban Quadrat
  • Carlos Simpson
• Coq-community maintainer(s):
  • Laurent Théry (@thery)
• License: MIT License
• Compatible Coq versions: 8.10 or later
• Additional dependencies:
  • MathComp ssreflect 1.12 or later
  • MathComp algebra
• Coq namespace: gaia
• Related publication(s):
  • Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets doi:10.6092/issn.1972-5787/1899
  • Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers doi:10.6092/issn.1972-5787/4771
  • Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets
  • Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers
  • Implementation of Bourbaki's Elements of Mathematics in Coq: Part Three Structures
  • Fibonacci numbers and the Stern-Brocot tree in Coq
  • Implementation of three types of ordinals in Coq

Building and installation instructions

The easiest way to install the latest released version of Gaia is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-gaia

To instead build and install manually, do:

git clone https://github.com/coq-community/gaia.git
cd gaia
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

Gaia stands for: Geometry, Algebra, Informatics and Applications. More information about the project is available at the project website.