Awesome
<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->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.16 or later
- Additional dependencies:
- 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
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
Documentation
Gaia stands for: Geometry, Algebra, Informatics and Applications. More information about the project is available at the project website.