3 ms·
"the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types ma
by gerdesj 5y ago
"the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible)"
I'm sure Mr Hilbert would approve.
"and the formalization of each of these in computer proof assistants."
Aah, loosely IT related (hence the post) and surely Lean and co can't be far away from the discussion.
"As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux."
The WP article is quite dense for a civilian to get through so I hope something cool is on the horizon.
Is a result on the way or has Lean blue screened?
- nixpulvis 5y agoIT? WP? Lean?
- semigroupoid 5y agoIT = Information Technology WP = Wikipedia Lean -> https://leanprover.github.io https://leanprover.github.io
- darzu 5y agoHere I think IT more likely means Intuitionistic Type Theory.
- jhanschoo 5y agoHoTT is somewhat independent of the choice of proof assistant. Coq: https://github.com/HoTT/HoTT https://github.com/HoTT/HoTT Lean: https://github.com/gebner/hott3 https://github.com/gebner/hott3 idk what you mean by "blue screened", or results being on the way. afaict most of the non-foundational work present (what I assume you mean by "results") in these libraries are basic properties of basic mathematical concepts being rebuilt on HoTT.
- m_j_g 5y agocubical Agda : https://github.com/agda/cubical https://github.com/agda/cubical is also worth mentioning int this context