3 ms·

Yes, Voevodsky works in Coq. Some other people in the "univalent foundations" project that Voevodsky started have also done some developments in Agda. Apart fr

Yes, Voevodsky works in Coq. Some other people in the "univalent foundations" project that Voevodsky started have also done some developments in Agda. Apart from Voevodsky's work, there are several other big math formalization projects. Perhaps the biggest ones are the formalization of the Feit-Thompson theorem (done by Georges Gonthier and his collaborators, in Coq), and the proof of the Kepler conjecture (done by Thomas Hales and his collaborators, in Isabelle/HOL and HOL Light).

platz 11y ago
does using Coq mean that the math he is seeking to prove is based on / formulated in a Constructivist style (http://en.wikipedia.org/wiki/Constructivism_%28mathematics%29 http://en.wikipedia.org/wiki/Constructivism_%28mathematics%2...), or only that the verification program itself requires such Constructivist properties?
- vilhelm_s 11y ago
  I don't think Voevodksky himself has any constructivist leanings. The univalent foundations developments make use of various axioms that have no known constructive meaning (e.g. the law of the excluded middle, and the famous univalence axiom itself), and which are motivated because there are known models in which they hold. On the other hand, many of his collaborators are interested in the project precisely because it uses Coq and they like constructive mathematics. So the HoTT book only uses exluded middle when necessary (and carefully tracks where), and developing a computational interpretation of univalence is considered to be an important task. Edit to add: So why would someone who doesn't care about constructivism want to use Coq? Because it's based around typed objects. Apparently, homotopy theorists had for a long time been aware that instead of basing mathematics on sets, and then constructing equivalence classes on top of those, you could take homotopy types as primitive.. something like basing mathematics on blobs rather than points. This was all considered theoretical and impractical--until someone noticed that the logic provided by Intensional Type Theory (as implemented in e.g. Coq) can be considered to do exactly this!
- nmrm2 11y ago
  In principle, yes. In actuality, you can always introduce new axioms and work with them. http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalence_axiom http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalence...
zepolud 11y ago
It should also be added that most of this work is being done publicly and is open to new contributors. You can check Voevodsky's github page[1], and most of the other HoTT collaborators are active members as well. The HoTT book itself is also being collaboratively written there. [1] https://github.com/vladimirias https://github.com/vladimirias

platz 11y ago

does using Coq mean that the math he is seeking to prove is based on / formulated in a Constructivist style (http://en.wikipedia.org/wiki/Constructivism_%28mathematics%29 http://en.wikipedia.org/wiki/Constructivism_%28mathematics%2...), or only that the verification program itself requires such Constructivist properties?

vilhelm_s 11y ago
I don't think Voevodksky himself has any constructivist leanings. The univalent foundations developments make use of various axioms that have no known constructive meaning (e.g. the law of the excluded middle, and the famous univalence axiom itself), and which are motivated because there are known models in which they hold. On the other hand, many of his collaborators are interested in the project precisely because it uses Coq and they like constructive mathematics. So the HoTT book only uses exluded middle when necessary (and carefully tracks where), and developing a computational interpretation of univalence is considered to be an important task. Edit to add: So why would someone who doesn't care about constructivism want to use Coq? Because it's based around typed objects. Apparently, homotopy theorists had for a long time been aware that instead of basing mathematics on sets, and then constructing equivalence classes on top of those, you could take homotopy types as primitive.. something like basing mathematics on blobs rather than points. This was all considered theoretical and impractical--until someone noticed that the logic provided by Intensional Type Theory (as implemented in e.g. Coq) can be considered to do exactly this!
nmrm2 11y ago
In principle, yes. In actuality, you can always introduce new axioms and work with them. http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalence_axiom http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalence...

zepolud 11y ago

It should also be added that most of this work is being done publicly and is open to new contributors. You can check Voevodsky's github page[1], and most of the other HoTT collaborators are active members as well. The HoTT book itself is also being collaboratively written there. [1] https://github.com/vladimirias https://github.com/vladimirias