math-comp VS UniMath

Compare math-comp vs UniMath and see what are their differences.

math-comp

Mathematical Components (by math-comp)
coq ssreflect mathcomp
Source Code
math-comp.github.io
Suggest alternative
Edit details

UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view. (by UniMath)
coq Mathematics unimath coq-library foundations
Source Code
unimath.org
Suggest alternative
Edit details
InfluxDB - Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
math-comp UniMath
1 2
548 914
1.3% 0.9%
9.1 9.5
12 days ago 8 days ago
Coq Coq
- GNU General Public License v3.0 or later
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
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.

math-comp

Posts with mentions or reviews of math-comp. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2023-06-18.

UniMath

Posts with mentions or reviews of UniMath. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2023-06-30.
  • Will Computers Redefine the Roots of Math?
    6 projects | news.ycombinator.com | 30 Jun 2023
    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).

  • Are There People Doing Formal Math In Berlin?
    3 projects | /r/berlinsocialclub | 13 Jun 2023
    I just wonder if there are any irl meetups of people involved with formalizing mathematics, I thought that it would be a cool hobby to pick up (with some background in math and programming) but the existing libraries, like MathLib, TypeTopology or UniMath look a bit intimidating...

What are some alternatives?

When comparing math-comp and UniMath you can also consider the following projects:

regexp-Brzozowski - Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

analysis - Mathematical Components compliant Analysis Library

Coq-HoTT - A Coq library for Homotopy Type Theory

coq-simple-io - IO for Gallina

nqthm - nqthm - the original Boyer-Moore theorem prover, from 1992

coq-library-undecidability - A library of mechanised undecidability proofs in the Coq proof assistant.

TypeTopology - Logical manifestations of topological concepts, and other things, via the univalent point of view.

aneris - Program logic for developing and verifying distributed systems

hs-to-coq - Convert Haskell source code to Coq source code.

rupicola - Gallina to Bedrock2 compilation toolkit

math-comp vs regexp-Brzozowski UniMath vs analysis math-comp vs analysis UniMath vs Coq-HoTT math-comp vs coq-simple-io UniMath vs nqthm math-comp vs coq-library-undecidability UniMath vs TypeTopology math-comp vs aneris UniMath vs hs-to-coq math-comp vs rupicola UniMath vs coq-library-undecidability