Skip to content
@theorem-labs

Theorem

Popular repositories Loading

  1. lf-lean lf-lean Public

    Benchmark based on the Logical Foundations volume of [Software Foundations](https://softwarefoundations.cis.upenn.edu/)

    Rocq Prover 10 1

  2. rocq rocq Public

    Forked from rocq-prover/rocq

    The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…

    OCaml 2

  3. rocq-lean-import rocq-lean-import Public

    Forked from rocq-community/rocq-lean-import

    Lean Import for Autoformalization

    OCaml

  4. coq-elpi coq-elpi Public

    Forked from LPCIC/coq-elpi

    Coq plugin embedding elpi

    OCaml

  5. coq-dpdgraph coq-dpdgraph Public

    Forked from rocq-community/coq-dpdgraph

    Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

    OCaml

  6. univalent_parametricity univalent_parametricity Public

    Forked from CoqHott/univalent_parametricity

    Univalent Parametricity for Effective Transport

    Rocq Prover

Repositories

Showing 10 of 25 repositories
  • rocq Public Forked from rocq-prover/rocq

    The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

    theorem-labs/rocq's past year of commit activity
    OCaml 2 LGPL-2.1 785 0 1 Updated Sep 15, 2026
  • xv6-lean Public
    theorem-labs/xv6-lean's past year of commit activity
    Lean 0 0 0 0 Updated Sep 11, 2026
  • lean-sail Public Forked from rems-project/lean-sail
    theorem-labs/lean-sail's past year of commit activity
    Lean 0 8 0 0 Updated Sep 10, 2026
  • metarocq Public Forked from MetaRocq/metarocq

    Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

    theorem-labs/metarocq's past year of commit activity
    Rocq Prover 0 MIT 101 0 0 Updated Aug 31, 2026
  • rocq-lean-import Public Forked from rocq-community/rocq-lean-import

    Lean Import for Autoformalization

    theorem-labs/rocq-lean-import's past year of commit activity
    OCaml 0 LGPL-2.1 13 0 0 Updated Aug 26, 2026
  • coq-elpi Public Forked from LPCIC/coq-elpi

    Coq plugin embedding elpi

    theorem-labs/coq-elpi's past year of commit activity
    OCaml 0 LGPL-2.1 87 0 1 Updated Aug 24, 2026
  • univalent_parametricity Public Forked from CoqHott/univalent_parametricity

    Univalent Parametricity for Effective Transport

    theorem-labs/univalent_parametricity's past year of commit activity
    Rocq Prover 0 5 0 0 Updated Aug 24, 2026
  • lean-zip Public Forked from kim-em/lean-zip
    theorem-labs/lean-zip's past year of commit activity
    Lean 0 Apache-2.0 14 0 0 Updated Aug 15, 2026
  • lean-zip-common Public Forked from kim-em/lean-zip-common

    Shared utilities for lean-zip and lean-zstd: binary encoding, file handle shims, and stdlib lemmas

    theorem-labs/lean-zip-common's past year of commit activity
    Lean 0 Apache-2.0 3 0 0 Updated Aug 15, 2026
  • coq-dpdgraph Public Forked from rocq-community/coq-dpdgraph

    Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

    theorem-labs/coq-dpdgraph's past year of commit activity
    OCaml 0 LGPL-2.1 33 0 0 Updated Aug 13, 2026
View all repositories

Top languages

Loading…

Most used topics

Loading…