ForMath in nLab

+-- {: .rightHandSide}
+-- {: .toc .clickDown tabindex="0"}
### Context
#### Type theory
+-- {: .hide}
[[!include type theory - contents]]
=--
#### Foundations
+-- {: .hide}
[[!include foundations - contents]]
=--
#### Constructivism, Realizability, Computability
+-- {: .hide}
[[!include constructivism - contents]]
=--
=--
=--

#Contents#
* table of contents
{:toc}

## Idea

A project for formalization of parts of [[mathematics]] ([[formal proof]]) in formal languages supported by [[proof assistants]] (particularly in [[Coq]]).

## Related projects

* [[UniMath project]]

* [[Xena project]]

* [[The QED Project]]

* [[Archive of Formal Proofs]]


## Related entries

* [[MathScheme]]

* [[formal proof]]

## References

* [ForMath Website](http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath)

* {#ForMath} [[Thierry Coquand]], _ForMath: Formalisation of Mathematics_ research project ([web](http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath))
  
* {#MathClasses} Eelis van der Weegen, [[Bas Spitters]], Robbert Krebbers, Matthieu Sozeau, Tom Prince, [[Jelle Herold]], 

  _Math Classes_, Coq Library for basic mathematical structures ([web](http://math-classes.org/))


[[!redirects ForMath project]]