Coq-HoTT
cubicaltt
Coq-HoTT | cubicaltt | |
---|---|---|
4 | 3 | |
1,214 | 557 | |
0.4% | - | |
9.8 | 2.3 | |
6 days ago | 7 months ago | |
Coq | Haskell | |
GNU General Public License v3.0 or later | MIT License |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Coq-HoTT
-
What do we mean by "the foundations of mathematics"?
https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t... :
> * Today, Zermelo–Fraenkel set theory [ZFC], with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common* foundation of mathematics.
Foundation of mathematics: https://en.wikipedia.org/wiki/Foundations_of_mathematics
Implementation of mathematics in set theory:
> The implementation of a number of basic mathematical concepts is carried out in parallel in ZFC (the dominant set theory) and in NFU, the version of Quine's New Foundations shown to be consistent by R. B. Jensen in 1969 (here understood to include at least axioms of Infinity and Choice).
> What is said here applies also to two families of set theories: on the one hand, a range of theories including Zermelo set theory near the lower end of the scale and going up to ZFC extended with large cardinal hypotheses such as "there is a measurable cardinal"; and on the other hand a hierarchy of extensions of NFU which is surveyed in the New Foundations article. These correspond to different general views of what the set-theoretical universe is like
IEEE-754 specifies that float64s have ±infinity and specify ZeroDivisionError. Symbolic CAS with MPFR needn't be limited to float64s.
HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/Coq-HoTT
leanprover-community/mathlib4//
-
Will Computers Redefine the Roots of Math?
For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few:
UniMath (https://github.com/UniMath/UniMath, mentioned in the article)
Coq-HoTT (https://github.com/HoTT/Coq-HoTT)
agda-unimath (https://unimath.github.io/agda-unimath/)
cubical agda (https://github.com/agda/cubical)
All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).
-
Homotopy Type Theory
HoTT is somewhat independent of the choice of proof assistant.
Coq: https://github.com/HoTT/HoTT
Lean: 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.
-
What is the benefit of using a text editor like MikTex, Texmaker, etc. over Overleaf?
The major one for me is version control (git). Imaging having to write a book like HoTT without having revisions and easy way to work on your changes without interfering with anyone else's work and then easily merging everything together.
cubicaltt
-
Let's collect relatively new research programming languages in this thread
- cubicialtt a programming language based on cubical type theory in which univalence from homotopy type theory isn't an axiom but a theorem
-
How and where to learn the latest mathematical concepts?
If you’re interested in programming languages specifically, the current state of the art is called Cubical Type Theory. CuTT has lots of flavours and the community hasn’t coalesced around a single design. The paper I personally found easiest to digest was the “ABCFHL” paper, but I’d recommend reading it alongside the original CCHM paper. None of the publications made an ounce of sense to me until after I’d digested Favonia’s YouTube channel, Mortberg’s lecture notes and this other series of lectures from Harper (particularly the final one).
-
Plato’s Cave Found in Mathematics
I updated the blog post to include some people in academia who contributed. I've been interacting with Kent Palmer and Sylvester James Gates, Jr. The latter held lectures about the philosophy of mathematics. I've been using work inspired by Vladimir Voevodsky, e.g. cubicaltt (https://github.com/mortberg/cubicaltt), which is also performed by academics.
What are some alternatives?
lean - Lean Theorem Prover
cooltt - 😎TT
cubical - An experimental library for Cubical Agda
jasmin - Language for high-assurance and high-speed cryptography
Agda - Agda formalisation of the Introduction to Homotopy Type Theory
karamel - KaRaMeL is a tool for extracting low-level F* programs to readable C code
hott3 - HoTT in Lean 3
sml-redprl - The People's Refinement Logic
mathlib - Lean 3's obsolete mathematical components library: please use mathlib4
anders - 🧊 Модальний гомотопічний верифікатор математики
UniMath - This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
cogent - Cogent Project