Pinned Loading

1. leanprover/lean4 leanprover/lean4 Public

   Lean 4 programming language and theorem prover

   Lean 8.4k 889

2. proost-assistant/proost proost-assistant/proost Public

   A small proof assistant written in Rust. Read-only mirror of https://gitlab.crans.org/loutr/proost.

   Rust 32 3

3. proost-assistant/ProostLean proost-assistant/ProostLean Public

   An reimplementation of the Proost proof-assistant written in Lean 4

   Lean 12 1

4. Leanduction Leanduction Public

   Generate good induction principles on nested inductive types

   Lean 7

5. agda agda Public

   Forked from agda/agda

   Agda is a dependently typed programming language / interactive theorem prover.

   Haskell

6. CoqHott/logrel-coq CoqHott/logrel-coq Public

   Logical Relation for MLTT in Coq

   Coq 33 6