hott3 VS trepplein

Compare hott3 vs trepplein and see what are their differences.

hott3

HoTT in Lean 3 (by gebner)

trepplein

Lean type-checker written in Scala. (by gebner)
Our great sponsors
  • WorkOS - The modern identity platform for B2B SaaS
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • SaaSHub - Software Alternatives and Reviews
hott3 trepplein
2 2
72 26
- -
1.8 0.0
over 3 years ago about 2 years ago
Lean Scala
Apache License 2.0 Apache License 2.0
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.

hott3

Posts with mentions or reviews of hott3. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-12-11.

trepplein

Posts with mentions or reviews of trepplein. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-03-04.
  • Automated Theorem Provers?
    2 projects | /r/math | 4 Mar 2021
    The default kernel used is fairly large, since it does some optimisations for interactivity. However there are 3 independent checkers for Lean's output format, https://github.com/gebner/trepplein, https://github.com/leanprover/lean/tree/master/src/checker and https://github.com/leanprover/tc . They're all fairly small, with leanchecker being less than 1000 loc.
  • Formalising Mathematics: An Introduction
    2 projects | news.ycombinator.com | 21 Feb 2021
    Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean, e.g. [1].

    Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics, making it way more powerful than metamath.

    [1] https://github.com/gebner/trepplein/tree/master/src/main/sca...

What are some alternatives?

When comparing hott3 and trepplein you can also consider the following projects:

CoqGym - A Learning Environment for Theorem Proving with the Coq proof assistant

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

scala - Scala 2 compiler and standard library. Bugs at https://github.com/scala/bug; Scala 3 at https://github.com/scala/scala3

holbert - A graphical interactive proof assistant designed for education

template-agda - An Agda template, configured for Gitpod (www.gitpod.io) to give you pre-built, ephemeral development environments in the cloud.

Lila - ♞ lichess.org: the forever free, adless and open source chess server ♞ [Moved to: https://github.com/lichess-org/lila]

Leantime - Leantime is a goals focused project management system for non-project managers. Building with ADHD, Autism, and dyslexia in mind.

Coq-HoTT - A Coq library for Homotopy Type Theory

Play - The Community Maintained High Velocity Web Framework For Java and Scala.

cubical - An experimental library for Cubical Agda

lean4 - Lean 4 programming language and theorem prover