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

• Author(s):
  • José Grimm
  • Alban Quadrat
  • Carlos Simpson
• Coq-community maintainer(s):
  • Laurent Théry (@thery)
• License: MIT License
• Compatible Coq versions: 8.16 or later
• Additional dependencies:
  • MathComp ssreflect 2.0 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

To 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

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