UniMath Alternatives

Similar projects and alternatives to UniMath

mathlib

36 1,625 8.8 Lean UniMath VS mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
Coq-HoTT

4 1,214 9.8 Coq UniMath VS Coq-HoTT

A Coq library for Homotopy Type Theory
InfluxDB

www.influxdata.com sponsored

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.
nqthm

4 43 10.0 Common Lisp UniMath VS nqthm

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

10 791 10.0 Lean UniMath VS mathlib4

The math library of Lean 4
analysis

1 180 9.4 Coq UniMath VS analysis

Mathematical Components compliant Analysis Library (by math-comp)
math-comp

1 546 9.0 Coq UniMath VS math-comp

Mathematical Components
pasv

4 44 10.0 Common Lisp UniMath VS pasv

The Pascal-F Verifier
WorkOS

workos.com sponsored

The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
TypeTopology

1 211 9.8 Agda UniMath VS TypeTopology

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

2 74 0.0 Coq UniMath VS hs-to-coq

Convert Haskell source code to Coq source code.
cubical

3 421 8.5 Agda UniMath VS cubical

An experimental library for Cubical Agda
coq-library-undecidability

2 98 6.4 Coq UniMath VS coq-library-undecidability

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

3 48 7.7 Coq UniMath VS rupicola

Gallina to Bedrock2 compilation toolkit

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better UniMath alternative or higher similarity.

Suggest an alternative to UniMath

UniMath reviews and mentions

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...